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:

:\neg A \wedge (B \vee C)
:(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)
:(\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:

:\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:

:\neg B \wedge \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,\ldots,Z_n na sledeći način:

:(Z_1 \vee \cdots \vee Z_n) \wedge
(\neg Z_1 \vee X_1) \wedge (\neg Z_1 \vee Y_1) \wedge
\cdots \wedge 
(\neg Z_n \vee X_n) \wedge (\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:
# Transformisanje u negacijsku normalnu formu. Eliminišu se implikacije: x \rightarrow  y se zameni sa \neg x \vee y
# Negacije se uvuku unutar zagrada
# Standardizuju se promenljive
# Skolemizuje se iskaz
# Eliminišu se univerzalni kvantifikatori
# Primeni se distributivnost na disjunkcije i konjunkcije.

## Izvori

## Povezano
* Disjunktivna normalna forma
* Algebarska normalna forma
* Preneks normalna forma
* Hornova klauza

## Vanjske veze
* Scheme i Ocaml programi za konvertovanje iskaznih formula u KNF