Konjunktiv normalform

Konjunktiv normalform ( CNF ) i boolesk logik är en normalform där en boolesk formel har formen av en konjunktion av disjunktioner av bokstaver . Den konjunktiva normalformen är lämplig för automatisk satsbevisning . Vilken boolesk formel som helst kan konverteras till CNF. [1] För detta kan du använda: lagen om dubbel negation , de Morgans lag , distributionskraft .

Exempel och motexempel

Formler i CNF :

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

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

A\kil B.

Formler som inte finns i CNF :

\neg (B\vee C),

(A\kil B)\vee C,

A\kil (B\vee (D\kil E)).

Men dessa 3 formler är inte i CNF ekvivalenta med följande formler i CNF:

\neg B\kil \neg C,

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

A\kil (B\vee D)\kil (B\vee E).

Konstruktion av CNF

Algoritm för att konstruera CNF

1) Bli av med alla logiska operationer som finns i formeln, ersätt dem med de viktigaste: konjunktion, disjunktion, negation. Detta kan göras med hjälp av motsvarande formler:

A\högerpil B=\neg A\vee B,

A\vänsterhögerpil B=(\neg A\vee B)\wedge (A\vee \neg B).

2) Ersätt negationstecken, med hänvisning till hela uttrycket, med negationstecken, med hänvisning till individuella variabelsatser, baserat på formlerna:

\neg (A\vee B)=\neg A\kil \neg B,

\neg (A\kil B)=\neg A\vee \neg B.

3) Bli av med dubbla negativa tecken.

4) Tillämpa, om nödvändigt, egenskaperna för fördelnings- och absorptionsformler på operationerna av konjunktion och disjunktion .

Ett exempel på att konstruera en CNF

Låt oss reducera formeln till CNF

F=(X\högerpil Y)\kil ((\neg Y\högerpil Z)\högerpil \neg X).

Låt oss omvandla formeln till en formel som inte innehåller : $F$ $\höger pil$

F=(\neg X\vee Y)\kil (\neg (\neg Y\högerpil Z)\vee \neg X)=(\neg X\vee Y)\kil (\neg (\neg \neg Y\ vee Z)\vee \neg X).

I den resulterande formeln överför vi negationen till variablerna och reducerar de dubbla negationerna:

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

Enligt distributionslagen får vi CNF:

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

k -konjunktiv normalform

En k -konjunktiv normalform är en konjunktiv normalform där varje disjunktion innehåller exakt k literals .

Till exempel är följande formel skriven i 2-CNF:

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

Övergång från KNF till SKNF

Om någon variabel saknas i en enkel disjunktion (till exempel z), lägger vi till uttrycket till den: (detta ändrar inte själva disjunktionen), varefter vi öppnar parenteserna med hjälp av distributionslagen : $Z\kil \neg Z=0$

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

Sålunda erhålls SKNF från CNF.

Formell grammatik som beskriver CNF

Följande formella grammatik beskriver alla formler reducerade till CNF:

där <term> anger en godtycklig boolesk variabel.

Tillfredsställbarhetsproblemet för en formel i CNF

I teorin om beräkningskomplexitet spelas en viktig roll av problemet med tillfredsställelse av booleska formler i konjunktiv normal form. Enligt Cookes teorem är detta problem NP-komplett , och det reduceras till tillfredsställbarhetsproblemet för formler i 3-CNF, vilket reducerar, och till vilket andra NP-kompletta problem minskar i sin tur .

Tillfredsställbarhetsproblemet för 2-CNF-formler kan lösas i linjär tid.

Notationsfunktioner

Det bör noteras att för att underlätta uppfattningen används ofta symbolerna för aritmetisk multiplikation och addition som en beteckning för konjunktion och disjunktion, medan multiplikationssymbolen ofta utelämnas. I det här fallet ser booleska algebraformler ut som algebraiska polynom, vilket är mer bekant för ögat, men ibland kan leda till missförstånd.

Till exempel är följande poster likvärdiga:

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

Av denna anledning kallas CNF i den ryskspråkiga litteraturen ibland "produkten av summor", vilket är ett spårningspapper från den engelska termen "produkt av summor".

Se även

Anteckningar

↑ Pozdnyakov S.N., Rybin S.V. Diskret matematik. - S. 303.

Litteratur

Yu.I. Galushkina, A.N. Maryamov: Lecture Notes on Discrete Mathematics - 2nd ed., rev. - M.: Iris-press, 2008. - 176 sid. - (Högre utbildning)

Länkar

Disjunktiva och konjunktiva normala former