Конјунктивна нормална форма

Из Википедије, слободне енциклопедије

У буловској логици, формула је у конјунктивној нормалној форми (КНФ) ако представља конјункцију клауза, где је клауза дисјункција литерала. Као нормална форма, корисна је у аутоматском доказивању теорема.

Све конјункције литерала и све дисјункције литерала су у КНФ, јер се могу посматрати као конјункције једночланих литерала, или као дисјункције једне клаузе, редом. Као и код дисјунктивне нормалне форме (ДНФ), једини исказни везници које формула у КНФ може да садржи су И, ИЛИ, и НЕ. Оператор негације може да се користи само као део литерала, што значи да може да стоји само пре исказне променљиве.

Примери и контрапримери[уреди]

Следеће формуле су у КНФ:

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

Последња формула је у КНФ, јер се може посматрати као конјункција две једночлане клаузе A и B. Међутим, ова формула је и у дисјунктивној нормалној форми. Следеће формуле нису у КНФ:

\neg (B \vee C)
(A \wedge B) \vee C
A \wedge (B \vee (D \wedge E)).

Горње три формуле су редом еквивалентне следећим трима формулама које јесу у конјунктивној нормалној форми:

\neg B \wedge \neg C
(A \vee C) \wedge (B \vee C)
A \wedge (B \vee D) \wedge (B \vee E).

Конверзија у КНФ[уреди]

Свака исказна формула се може трансформисати у логички еквивалентну формулу, која је у КНФ. Ова трансформација користи правила логичке еквиваленције: елиминацију двоструке негације, Де Морганове законе, и закон дистрибутивности.

Како се све логичке формуле могу трансформисати у еквивалентне формуле у КНФ, докази се обично базирају на претпоставци да су све формуле у КНФ. Међутим, у неким случајевима, ова конверзија у КНФ може да доведе до експоненцијалне експлозије (раста дужине) формуле. На пример, трансформисање следеће формуле у КНФ производи формулу са 2^n клауза:

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

Добија се формула:

(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)

то јест, ова формула садржи 2^n клауза: у свакој клаузи се налази било X_i или Y_i за свако i.

Постоје трансформације формула у КНФ које чувају задовољивост али не и еквиваленцију, али и не производе експоненцијални раст формула. За ове трансформације се гарантује да формуле повећавају само линеарно, али уводе нове променљиве. На пример, горња гормула се може трансформисати у КНФ додавањем променљивих Z_1,\ldots,Z_n на следећи начин:

(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)

Нека интерпретација задовољава ову формулу само ако барем једна од нових променљивих има вредност тачно. Ако је то променљива Z_i, онда такође X_i и Y_i имају вредност тачно. Ово значи да сваки модел који задовољава добијену формулу задовољава и почетну. Са друге стране, само неки модели оригиналне формуле задовољавају ову нову, јер се Z_i не спомиње у почетној формули, па њихове вредности нису од значаја за њу, док јесу за нову формулу. Ово значи да су почетна формула и резултат трансформације еквизадовољиви, али не и еквивалентни.

Логика првог реда[уреди]

У логици првог реда, конјунктивна нормална форма се може трансформисати даље у клаузалну нормалну форму, која је од користи за метод резолуције.

Рачунска сложеност[уреди]

Важан скуп проблема у рачунској сложености подразумева налажење таквих додела променљивима буловске формуле у конјунктивној нормалној форми, да формула има вредност тачно. k-САТ проблем је проблем налажења задовољавајуће доделе буловској формули исказаној у КНФ, тако да свака дисјункција садржи највише k променљивих. 3-САТ је НП-комплетан проблем (као и сваки други k-САТ, где је k>2) осим 2-САТ, за кога је познато решење у полиномијалном времену.

Трансформисање из логике првог реда[уреди]

Трансформисање формуле предикатског рачуна у КНФ подразумева следеће кораке:

  1. Трансформисање у негацијску нормалну форму. Елиминишу се импликације: x \rightarrow  y се замени са \neg x \vee y
  2. Негације се увуку унутар заграда
  3. Стандардизују се променљиве
  4. Сколемизује се исказ
  5. Елиминишу се универзални квантификатори
  6. Примени се дистрибутивност на дисјункције и конјункције.[1]

Извори[уреди]

  1. ^ (Artificial Intelligence: A modern Approach [1995...] Russel and Norvig)

Види још[уреди]

Спољашње везе[уреди]