Konjuktivna normalna forma

U bulovskoj logici, formula je u konjunktivnoj normalnoj formi (KNF) ako predstavlja konjunkciju klauza, gde je klauza disjunkcija literala. Kao normalna forma, korisna je u automatskom dokazivanju teorema.

Sve konjunkcije literala i sve disjunkcije literala su u KNF, jer se mogu posmatrati kao konjunkcije jednočlanih literala, ili kao disjunkcije jedne klauze, redom. Kao i kod disjunktivne normalne forme (DNF), jedini iskazni veznici koje formula u KNF može da sadrži su I, ILI, i NE. Operator negacije može da se koristi samo kao deo literala, što znači da može da stoji samo pre iskazne promenljive.

Primeri i kontraprimeri

Sledeće formule su u KNF:

$\mathrm{\neg }A\wedge (B\vee C)$

$(A\vee B)\wedge (\mathrm{\neg }B\vee C\vee \mathrm{\neg }D)\wedge (D\vee \mathrm{\neg }E)$

$(\mathrm{\neg }B\vee C)$

$A\wedge B.$

Poslednja formula je u KNF, jer se može posmatrati kao konjunkcija dve jednočlane klauze $A$ i $B$. Međutim, ova formula je i u disjunktivnoj normalnoj formi. Sledeće formule nisu u KNF:

$\mathrm{\neg }(B\vee C)$

$(A\wedge B)\vee C$

$A\wedge (B\vee (D\wedge E)).$

Gornje tri formule su redom ekvivalentne sledećim trima formulama koje jesu u konjunktivnoj normalnoj formi:

$\mathrm{\neg }B\wedge \mathrm{\neg }C$

$(A\vee C)\wedge (B\vee C)$

$A\wedge (B\vee D)\wedge (B\vee E).$

Konverzija u KNF

Svaka iskazna formula se može transformisati u logički ekvivalentnu formulu, koja je u KNF. Ova transformacija koristi pravila logičke ekvivalencije: eliminaciju dvostruke negacije, De Morganove zakone, i zakon distributivnosti.

Kako se sve logičke formule mogu transformisati u ekvivalentne formule u KNF, dokazi se obično baziraju na pretpostavci da su sve formule u KNF. Međutim, u nekim slučajevima, ova konverzija u KNF može da dovede do eksponencijalne eksplozije (rasta dužine) formule. Na primer, transformisanje sledeće formule u KNF proizvodi formulu sa $2^n$ klauza:

$(X_1\wedge Y_1)\vee (X_2\wedge Y_2)\vee \dots \vee (X_n\wedge Y_n).$

Dobija se formula:

$(X_1\vee \cdots \vee X_{n-1}\vee X_n)\wedge (X_1\vee \cdots \vee X_{n-1}\vee Y_n)\wedge \cdots \wedge (Y_1\vee \cdots \vee Y_{n-1}\vee Y_n)$

to jest, ova formula sadrži $2^n$ klauza: u svakoj klauzi se nalazi bilo $X_i$ ili $Y_i$ za svako $i$.

Postoje transformacije formula u KNF koje čuvaju zadovoljivost ali ne i ekvivalenciju, ali i ne proizvode eksponencijalni rast formula. Za ove transformacije se garantuje da formule povećavaju samo linearno, ali uvode nove promenljive. Na primer, gornja gormula se može transformisati u KNF dodavanjem promenljivih $Z_1,\dots ,Z_n$ na sledeći način:

$(Z_1\vee \cdots \vee Z_n)\wedge (\mathrm{\neg }{Z}_1\vee X_1)\wedge (\mathrm{\neg }{Z}_1\vee Y_1)\wedge \cdots \wedge (\mathrm{\neg }{Z}_n\vee X_n)\wedge (\mathrm{\neg }{Z}_n\vee Y_n)$

Neka interpretacija zadovoljava ovu formulu samo ako barem jedna od novih promenljivih ima vrednost tačno. Ako je to promenljiva $Z_i$, onda takođe $X_i$ i $Y_i$ imaju vrednost tačno. Ovo znači da svaki model koji zadovoljava dobijenu formulu zadovoljava i početnu. Sa druge strane, samo neki modeli originalne formule zadovoljavaju ovu novu, jer se $Z_i$ ne spominje u početnoj formuli, pa njihove vrednosti nisu od značaja za nju, dok jesu za novu formulu. Ovo znači da su početna formula i rezultat transformacije ekvizadovoljivi, ali ne i ekvivalentni.

Logika prvog reda

U logici prvog reda, konjunktivna normalna forma se može transformisati dalje u klauzalnu normalnu formu, koja je od koristi za metod rezolucije.

Računska složenost

Važan skup problema u računskoj složenosti podrazumeva nalaženje takvih dodela promenljivima bulovske formule u konjunktivnoj normalnoj formi, da formula ima vrednost tačno. k-SAT problem je problem nalaženja zadovoljavajuće dodele bulovskoj formuli iskazanoj u KNF, tako da svaka disjunkcija sadrži najviše k promenljivih. 3-SAT je NP-kompletan problem (kao i svaki drugi k-SAT, gde je k>2) osim 2-SAT, za koga je poznato rešenje u polinomijalnom vremenu.

Transformisanje iz logike prvog reda

Transformisanje formule predikatskog računa u KNF podrazumeva sledeće korake:

1. Transformisanje u negacijsku normalnu formu. Eliminišu se implikacije: $x\to y$ se zameni sa $\mathrm{\neg }x\vee y$
2. Negacije se uvuku unutar zagrada
3. Standardizuju se promenljive
4. Skolemizuje se iskaz
5. Eliminišu se univerzalni kvantifikatori
6. Primeni se distributivnost na disjunkcije i konjunkcije.

Povezano

• Disjunktivna normalna forma
• Algebarska normalna forma
• Preneks normalna forma
• Hornova klauza

Vanjske veze

• Scheme i Ocaml programi za konvertovanje iskaznih formula u KNF Šablon:Webarchive