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

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

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

Примери и контрапримери

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

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

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

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

${\displaystyle (A\vee B).}$

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

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

${\displaystyle (A\wedge B)\vee C}$

${\displaystyle A\wedge (B\vee (D\wedge E)).}$

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

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

${\displaystyle (A\vee C)\wedge (B\vee C)}$

${\displaystyle A\wedge (B\vee D)\wedge (B\vee E).}$

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

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

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

${\displaystyle (X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n}).}$

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

${\displaystyle (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})}$

то јест, ова формула садржи ${\displaystyle 2^{n}}$ клауза: у свакој клаузи се налази било ${\displaystyle X_{i}}$ или ${\displaystyle Y_{i}}$ за свако ${\displaystyle i}$.

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

${\displaystyle (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})}$

Нека интерпретација задовољава ову формулу само ако барем једна од нових променљивих има вредност тачно. Ако је то променљива ${\displaystyle Z_{i}}$, онда такође ${\displaystyle X_{i}}$ и ${\displaystyle Y_{i}}$ имају вредност тачно. Ово значи да сваки модел који задовољава добијену формулу задовољава и почетну. Са друге стране, само неки модели оригиналне формуле задовољавају ову нову, јер се ${\displaystyle Z_{i}}$ не спомиње у почетној формули, па њихове вредности нису од значаја за њу, док јесу за нову формулу. Ово значи да су почетна формула и резултат трансформације еквизадовољиви, али не и еквивалентни.

Логика првог реда

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

Рачунска сложеност

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

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

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

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

Извори

Види још

• Канонска нормална форма
• Дисјунктивна нормална форма
• Алгебарска нормална форма
• Пренекс нормална форма
• Хорнова клауза

Спољашње везе

• и програми за конвертовање исказних формула у КНФ