Konjunktiv Normalform

In der Booleschen Logik und im Booleschen Kalkül ist eine Formel in konjunktiver Normalform oder FNC (Englisch, konjunktive Normalform oder CNF ) eine Konjunktion von Klauseln , wobei eine Klausel eine Disjunktion von Literalen ist . Die Formeln in FNC werden im Rahmen des automatischen Beweises von Theoremen oder sogar bei der Lösung des SAT-Problems (insbesondere im DPLL-Algorithmus ) verwendet.

Definition und Beispiele

Ein logischer Ausdruck ist in FNC genau dann, wenn es sich um eine Konjunktion einer oder mehrerer Disjunktionen eines oder mehrerer Literale handelt . Genau wie in einer disjunktiven Normalform (DNF) sind die einzigen Operatoren in der FNC logisch , logisch oder und Negation . Der Operator kann nicht nur in einem Literal verwendet werden, dh er kann nur einer Variablen vorangehen. Beispielsweise sind alle folgenden Ausdrücke in FNC enthalten:

Beispiele für Formeln in FNC:

$A \ land B.$
$A \ lor B.$
$BEIM\!$
${\ displaystyle (A \ lor B) \ land C}$
${\ displaystyle (A \ lor \ neg B \ lor \ neg C) \ land (\ neg D \ lor E \ lor F)}$

Die folgenden Ausdrücke sind jedoch nicht in FNC enthalten:

Gegenbeispiele für Formeln in FNC:

${\ displaystyle \ neg (A \ land B)}$ - Die Negation steht vor der Formel, die nicht atomar ist (es ist keine Variable). $\ neg$ ${\ displaystyle (A \ land B)}$
${\ displaystyle A \ land (B \ lor (C \ land D))}$ - a und ist in einem oder verschachtelt

Umstellung auf äquivalente FNC

Jede Boolesche Formel kann in Form einer FNC-Formel umgeschrieben werden, die denselben Wahrheitswert hat und daher logisch äquivalent ist. Das Konvertieren eines Ausdrucks in einen FNC erfordert die Verwendung logischer Transformationsregeln, z. B. die Beseitigung von Doppelverneinungen, De Morgans Gesetzen und dem Gesetz der Verteilungsfähigkeit .

Umwandlung in FNC:

${\ displaystyle (\ lnot (X_ {1} \ lor X_ {2}) \ lor (X_ {3} \ land X_ {4})) \ land (\ lnot X_ {1} \ lor X_ {2})}$

$\ äquiv$

${\ displaystyle (\ lnot X_ {1} \ lor X_ {3}) \ land (\ lnot X_ {1} \ lor X_ {4}) \ land (\ lnot X_ {2} \ lor X_ {3}) \ Land (\ lnot X_ {2} \ lor X_ {4}) \ land (\ lnot X_ {1} \ lor X_ {2})}$

Die Anwendung der Verteilungsgesetze kann in einigen Fällen dazu führen, dass die Formel exponentiell wächst .

Formel, deren FNC eine exponentielle Größe hat:

die FNC eines Ausdrucks der folgenden Form in disjunktiver Normalform mit n Begriffen:

{\ displaystyle (X_ {1} \ land Y_ {1}) \ lor (X_ {2} \ land Y_ {2}) \ lor \ dots \ lor (X_ {n} \ land Y_ {n})}

Wessen FNC der Größe 2 n hat die Form:

{\ 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}).}

Gleichwertige lineare Umwandlung

Um exponentielle Transformationen zu vermeiden, können Transformationen durch Einführung zusätzlicher Variablen angewendet werden. Daher erzeugt diese Art der Transformation nicht mehr wie die vorherige Transformation logisch äquivalente Formeln, sondern Transformationen, die die Erfüllbarkeit der ursprünglichen Formel bewahren .

Diese Transformation wird manchmal als Tseytin- Transformation (oder Tseitin-Transformation) bezeichnet.

Die Formel von Beispiel 2 kann beispielsweise durch Einführen der Variablen umgeschrieben werden . ${\ displaystyle Z_ {1}, \ ldots, Z_ {n}}$

Beispiel für eine lineare Transformation:

Eine Formel der folgenden Form:

{\ displaystyle (X_ {1} \ land Y_ {1}) \ lor (X_ {2} \ land Y_ {2}) \ lor \ dots \ lor (X_ {n} \ land Y_ {n})}

Kann in einer nicht zufriedenstellenden Formel umgeschrieben werden

{\ 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}).}

Intuitiv repräsentiert in diesem Beispiel die Variable die Wahrheit der -ten Konjunktion der ursprünglichen Formel und der Klauseln und drückt die Bedingung aus . Mit anderen Worten, wenn es wahr ist, dann und muss es auch wahr sein. Der erste Satz der Transformation erfordert, dass mindestens einer der Punkte wahr ist, damit die Formel erfüllt ist, so dass mindestens einer der Sätze der ursprünglichen Formel wahr ist . $Z_ {i}$ $ich$ ${\ displaystyle \ neg Z_ {i} \ lor X_ {i}}$ ${\ displaystyle \ neg Z_ {i} \ lor Y_ {i}}$ ${\ displaystyle Z_ {i} \ rightarrow X_ {i} \ land Y_ {i}}$ $Z_ {i}$ $X_ {i}$ $Y_ {i}$ $Z_ {i}$

Wir können Transformationen auch auf Typklauseln basieren . Diese Klauseln implizieren Äquivalenz ; Wir können in diesen Formeln die Definition als Alias für die Formel sehen . ${\ displaystyle Z_ {i} \ vee \ neg X_ {i} \ vee \ neg Y_ {i}}$ ${\ displaystyle Z_ {i} \ equiv X_ {i} \ wedge Y_ {i}}$ $Z_ {i}$ ${\ displaystyle X_ {i} \ wedge Y_ {i}}$

Solche Transformationen ermöglichen es, eine FNC-Formel zu erhalten, deren Größe in Bezug auf die Größe der ursprünglichen Formel linear ist .

SAT-Problem

Das SAT-Problem ist das algorithmische Problem, das aus einer Formel besteht, mit der in FNC entschieden werden kann, ob es gültig ist oder nicht. Das Problem ist NP-vollständig , selbst für den speziellen 3-SAT-Fall, in dem nur Klauseln mit höchstens drei Literalen zulässig sind. Andererseits kann das Problem mit Klauseln der Größe 2, 2-SAT in Polynomzeit gelöst werden.

Siehe auch

Anmerkungen und Referenzen

(en) Jean Betrema, „ Computermodelle “ , Kapitel 9: NP-vollständige Probleme> SAT ist NP-vollständig> CNF ist NP-vollständig.
Beweis und lineare Umwandlung einer SAT-Formel in einen nicht zufriedenstellenden CNF.
GS Tseitin, Zur Komplexität der Ableitung in der Aussagenrechnung , (akademisches Kapitel),1970, [ online lesen ]