Forma normală conjunctivă - Conjunctive normal form

În logica booleană , o formulă este în formă normală conjunctivă ( CNF ) sau în formă normală clauzală dacă este o conjuncție a uneia sau mai multor clauze , unde o clauză este o disjuncție a literelor ; altfel spus, este un produs al sumelor sau al unui ȘI al OR . Ca formă canonică normală , este utilă în demonstrarea automatizată a teoremelor și teoria circuitelor .

Toate conjuncțiile de literali și toate disjuncțiile de literali se află în CNF, deoarece pot fi văzute ca conjuncții de clauze cu un singur literal și respectiv conjuncții ale unei singure clauze. Ca și în forma normală disjunctivă (DNF), singurele conectivități propoziționale pe care le poate conține o formulă în CNF sunt și , sau , și nu . Operatorul not poate fi folosit doar ca parte a unui literal, ceea ce înseamnă că poate preceda doar o variabilă propozițională sau un simbol predicat .

În demonstrarea automatizată a teoremelor, noțiunea „ formă normală clauzală ” este adesea utilizată într-un sens mai restrâns, ceea ce înseamnă o reprezentare particulară a unei formule CNF ca un set de seturi de literali.

Exemple și non-exemple

Toate următoarele formule din variabile și sunt în formă conjunctivă normală:

Pentru claritate, clauzele disjunctive sunt scrise în paranteze de mai sus. În formă normală disjunctivă cu propoziții conjunctive parantezate, ultimul caz este același, dar următorul la ultim este . Constantele adevărat și fals sunt notate de conjunctul gol și de o clauză constând din disjunctul gol, dar în mod normal sunt scrise explicit.

Următoarele formule nu sunt în formă conjunctivă normală:

  • , deoarece un OR este cuibărit într-un NOT
  • , deoarece un AND este imbricat într-un OR

Fiecare formulă poate fi scrisă în mod echivalent ca formulă în formă normală conjunctivă. Cele trei non-exemple din CNF sunt:

Conversia în CNF

Fiecare formulă propozițională poate fi convertită într-o formulă echivalentă care este în CNF. Această transformare se bazează pe reguli despre echivalențe logice : eliminarea dublei negații , legile lui De Morgan și legea distributivă .

Deoarece toate formulele propoziționale pot fi convertite într-o formulă echivalentă în formă conjunctivă normală, dovezile se bazează adesea pe presupunerea că toate formulele sunt CNF. Cu toate acestea, în unele cazuri, această conversie în CNF poate duce la o explozie exponențială a formulei. De exemplu, traducerea următoarei formule non-CNF în CNF produce o formulă cu clauze:

În special, formula generată este:

Această formulă conține clauze; fiecare clauză conține fie sau pentru fiecare .

Există transformări în CNF care evită o creștere exponențială a dimensiunii prin păstrarea satisfacției mai degrabă decât a echivalenței . Aceste transformări sunt garantate doar pentru a crește liniar dimensiunea formulei, dar introduc noi variabile. De exemplu, formula de mai sus poate fi transformată în CNF adăugând variabile după cum urmează:

O interpretare satisface această formulă numai dacă cel puțin una dintre noile variabile este adevărată. Dacă această variabilă este , atunci ambele și sunt adevărate. Aceasta înseamnă că fiecare model care satisface această formulă îl satisface și pe cel original. Pe de altă parte, doar unele dintre modelele formulei originale o satisfac pe aceasta: deoarece nu sunt menționate în formula originală, valorile lor sunt irelevante pentru satisfacerea acesteia, ceea ce nu este cazul în ultima formulă. Acest lucru înseamnă că formula originală și rezultatul traducerii sunt echivizabile, dar nu echivalente .

O traducere alternativă, transformarea Tseitin , include și clauze . Cu aceste clauze, formula implică ; această formulă este adesea considerată a „defini” pentru a fi un nume .

Logică de ordinul întâi

În logica de ordinul întâi, forma normală conjunctivă poate fi luată mai departe pentru a produce forma normală clauzală a unei formule logice, care poate fi apoi utilizată pentru a efectua rezoluția de ordinul întâi . În demonstrarea teoremei automatizată bazată pe rezoluție, o formulă CNF

, cu litere, este reprezentat de obicei ca un set de mulțimi
.

Vedeți mai jos un exemplu.

Complexitatea computațională

Un set important de probleme în complexitatea de calcul implică găsirea de atribuții variabilelor unei formule booleene exprimate în formă normală conjunctivă, astfel încât formula să fie adevărată. Problema k -SAT este problema găsirii unei atribuții satisfăcătoare la o formulă booleană exprimată în CNF în care fiecare disjuncție conține cel mult k variabile. 3-SAT este NP-complet (ca orice altă problemă k -SAT cu k > 2) în timp ce se știe că 2-SAT are soluții în timp polinomial . În consecință, sarcina de a converti o formulă într-un DNF , păstrând satisfacția, este NP-hard ; dual , convertirea în CNF, păstrarea validității , este, de asemenea, NP-hard; prin urmare, conversia care păstrează echivalența în DNF sau CNF este din nou NP-hard.

Problemele tipice în acest caz implică formule în „3CNF”: formă normală conjunctivă cu cel mult trei variabile pe conjunct. Exemple de astfel de formule întâlnite în practică pot fi foarte mari, de exemplu cu 100.000 de variabile și 1.000.000 de conjuncturi.

O formulă în CNF poate fi convertită într-o formulă echisatisfăcătoare în „ k CNF” (pentru k ≥3) prin înlocuirea fiecărui conjunct cu mai mult de k variabile cu două conjuncte și cu Z o nouă variabilă și repetarea ori de câte ori este necesar.

Conversia din logica de prim ordin

Pentru a converti logica de prim ordin în CNF:

  1. Convertiți în formă normală de negare .
    1. Eliminați implicațiile și echivalențele: înlocuiți în mod repetat cu ; înlocuiți cu . În cele din urmă, acest lucru va elimina toate aparițiile și .
    2. Mutați NOT-urile spre interior aplicând în mod repetat Legea lui De Morgan . Mai exact, înlocuiți cu ; înlocuiți cu ; și înlocuiți cu ; înlocuiți cu ; cu . După aceea, a poate apărea doar imediat înainte de simbolul predicat.
  2. Standardizați variabilele
    1. Pentru propoziții precum cele care folosesc același nume de variabilă de două ori, schimbați numele uneia dintre variabile. Acest lucru evită confuzia ulterior atunci când renunțați la cuantificatori. De exemplu, este redenumit în .
  3. Skolemize afirmația
    1. Mutați cuantificatoarele spre exterior: înlocuiți în mod repetat cu ; înlocuiți cu ; înlocuiți cu ; înlocuiți cu . Aceste înlocuiri păstrează echivalența, deoarece etapa anterioară a standardizării variabilei a asigurat că nu are loc în . După aceste înlocuiri, un cuantificator poate avea loc numai în prefixul inițial al formulei, dar niciodată în interiorul , sau .
    2. Înlocuiți în mod repetat cu , unde este un nou simbol funcțional -ary, așa-numita „ funcție Skolem ”. Acesta este singurul pas care păstrează mai degrabă satisfacția decât echivalența. Elimină toți cuantificatorii existențiali.
  4. Elimină toate cuantificatoarele universale.
  5. Distribuiți OR-urile spre interior peste AND-uri: înlocuiți în mod repetat cu .

De exemplu, formula care spune „Oricine iubește toate animalele, este la rândul său iubită de cineva” este convertită în CNF (și ulterior în formă de clauză în ultima linie) după cum urmează (evidențierea regulii de înlocuire redexează în ):

de 1.1
de 1.1
de 1.2
de 1.2
de 1.2
de 2
de 3.1
de 3.1
de 3.2
de 4
de 5
( reprezentarea clauzei )

În mod informal, funcția Skolem poate fi considerată ca cedând persoana de care este iubit, în timp ce cedează animalul (dacă există) care nu iubește. Al treilea ultim rând de jos citește apoi nu iubește animalul sau altfel este iubit de .

A doua ultimă linie de sus ,, este CNF.

Note

  1. ^ Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory , 2013, ISBN  9401599343 , p. 48
  2. ^ a b Inteligență artificială: o abordare modernă Archived 2017-08-31 la Wayback Machine [1995 ...] Russell și Norvig
  3. ^ Tseitin (1968)
  4. ^ Jackson și Sheridan (2004)
  5. ^ întrucât o modalitate de a verifica satisfacția unui CNF este de a-l converti într-un DNF , a cărui satisfacție poate fi verificată în timp liniar

Vezi si

Referințe

linkuri externe