Konjunktív normál forma

A konjunktív normálforma ( CNF ) a logikai logikában egy olyan normálforma , amelyben a Boole-képlet literálok diszjunkcióinak konjunkciója . A konjunktív normálalak alkalmas az automatikus tételbizonyításra . Bármely Boole-képlet konvertálható CNF-re. [1] Ehhez használhatja: a kettős tagadás törvénye , de Morgan törvénye , disztributivitás .

Példák és ellenpéldák

Képletek a CNF-ben :

\neg A\wedge (B\vee C),

(A\vee B)\ék (\neg B\vee C\vee \neg D)\wedge (D\vee \neg E),

A\ék B.

A CNF-ben nem szereplő képletek :

\neg (B\vee C),

(A\ék B)\vee C,

A\ék (B\vee (D\ék E)).

De ez a 3 képlet nem egyenértékű a CNF-ben a következő képletekkel a CNF-ben:

\neg B\wedge \neg C,

(A\vee C)\ék (B\vee C),

A\ék (B\vee D)\ék (B\vee E).

CNF építése

Algoritmus a CNF felépítéséhez

1) Szabaduljon meg a képletben szereplő összes logikai művelettől, és cserélje le őket a főbbekre: konjunkció, diszjunkció, tagadás. Ezt egyenértékű képletekkel lehet megtenni:

A\rightarrow B=\neg A\vee B,

A\leftrightarrow B=(\neg A\vee B)\wedge (A\vee \neg B).

2) Cserélje ki a teljes kifejezésre utaló tagadójelet tagadójelekre, amelyek az egyes változók állításaira vonatkoznak, a képletek alapján:

\neg (A\vee B)=\neg A\ék \neg B,

\neg (A\ék B)=\neg A\vee \neg B.

3) Szabadulj meg a kettős negatív előjelektől.

4) Szükség esetén alkalmazza a konjunkció és a diszjunkció műveleteire az eloszlási és abszorpciós képletek tulajdonságait.

Példa egy CNF létrehozására

Csökkentsük a képletet CNF-re

F=(X\jobbra Y)\ék ((\neg Y\jobbra Z)\jobbra \neg X).

Alakítsuk át a képletet olyan képletre, amely nem tartalmazza : $F$ $\jobb nyíl$

F=(\neg X\vee Y)\wedge (\neg (\neg Y\jobbra nyíl Z)\vee \neg X)=(\neg X\vee Y)\wedge (\neg (\neg \neg Y\ vee Z)\vee \neg X).

A kapott képletben a tagadást átvisszük a változókra, és csökkentjük a kettős tagadásokat:

F=(\neg X\vee Y)\wedge ((\neg Y\wedge \neg Z)\vee \neg X).

Az elosztási törvény szerint CNF-et kapunk:

F=(\neg X\vee Y)\wedge (\neg X\vee \neg Y)\wedge (\neg X\vee \neg Z).

k -konjunktív normálforma

A k -konjunktív normálforma olyan konjunktív normálforma, amelyben minden diszjunkció pontosan k literált tartalmaz .

Például a következő képlet 2-CNF-ben van írva:

(A\vagy B)\land (\neg B\vagy C)\land (B\vagy \neg C).

Átállás KNF-ről SKNF -re

Ha egy egyszerű diszjunkcióból hiányzik valamilyen változó (például z), akkor hozzáadjuk a következő kifejezést: (ez magát a diszjunkciót nem változtatja meg), majd az eloszlási törvény segítségével megnyitjuk a zárójeleket : $Z\ék \neg Z=0$

(X\vee Y)\ék (X\vee \neg Y\vee \neg Z)=(X\vee Y\vee (Z\wedge \neg Z))\wedge (X\vee \neg Y\vee \ neg Z)=(X\vee Y\vee Z)\ék (X\vee Y\vee \neg Z)\wedge (X\vee \neg Y\vee \neg Z).

Így az SKNF-t a CNF-ből nyerik.

A CNF-et leíró formális nyelvtan

A következő formális nyelvtan leírja az összes CNF-re redukált képletet:

ahol a <term> tetszőleges logikai változót jelöl.

A CNF-beli képlet kielégíthetőségi problémája

A számítási komplexitás elméletében fontos szerepet játszik a logikai képletek konjunktív normál formában való kielégíthetőségének problémája . Cooke tétele szerint ez a probléma NP-teljes , és a 3-CNF-ben lévő képletek kielégíthetőségi problémájára redukálódik, amely redukálódik, és amelyre más NP-teljes problémák redukálódnak .

A 2-CNF képletek kielégítési problémája lineáris időben megoldható.

Jelölés jellemzői

Meg kell jegyezni, hogy az érzékelés megkönnyítése érdekében az aritmetikai szorzás és összeadás szimbólumait gyakran használják kötő- és diszjunkció jelölésére, míg a szorzás szimbólumát gyakran elhagyják. Ebben az esetben a Boole-algebrai képletek algebrai polinomoknak tűnnek, ami ismerősebb a szem számára, de néha félreértésekhez vezethet.

Például a következő bejegyzések egyenértékűek:

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

(A\vee B)\wedge ({\overline {B}}\vee C\vee {\overline {D}})\wedge (D\vee {\overline {E}});

(A\vee B)\cdot ({\overline {B}}\vee C\vee {\overline {D}})\cdot (D\vee {\overline {E}});

(A\vee B)({\overline {B}}\vee C\vee {\overline {D}})(D\vee {\overline {E}});

(A+B)({\overline {B}}+C+{\overline {D}})(D+{\overline {E}}).

Emiatt a CNF-et az orosz nyelvű irodalomban néha "összegek szorzatának" nevezik, ami az angol "product of summas" kifejezésből származó pauszpapír.

Lásd még

Jegyzetek

↑ Pozdnyakov S.N., Rybin S.V. Diszkrét matematika. - S. 303.

Irodalom

Yu.I. Galushkina, A.N. Maryamov: Lecture Notes on Discrete Mathematics - 2. ed., rev. - M.: Iris-press, 2008. - 176 p. - (Felsőoktatás)

Linkek

Disjunktív és konjunktív normálformák