WikiDer > Konjunktive Normalform
In dem Logik ist eine Formel in Konjunktive Normalform (Gespenstisch. Konjunktive Normalform, CNF, auch abgekürzt als CNV) wenn es aus a . besteht Verbindung von Disjunktionen mit Literale (auch eine Konjunktion von Klauseln erwähnt). In einer konjunktiven Normalform sind nur die boolesche Operatorenund, oder und Negation denn wo die Negation nur als Teil von a . ist Atomformel kann auftreten. Da ist auch ein disjunktive Normalform, ein Disjunktion von Konjunktionen.
Jede Formel kann in a . umgewandelt werden Äquivalent Formel in konjunktiver Normalform unter Verwendung von Äquivalenzregeln (wie der Gesetze von De Morgan und Verteilungsfähigkeit), die die Formel in einer logisch äquivalenten Form in CNF beschreiben.
Beispiele
Beispiele für Formeln in normaler Konjunktivform:
Die folgenden Formeln sind jedoch nicht in normaler Konjunktivform:
Die folgenden Formeln in konjunktiver Normalform lauten jeweils logisches Äquivalent zu den vorherigen drei Formeln:
Anwendungen
CNF ist unter anderem im Feld wichtig automatische Argumentation, der Teilbereich von Informatik in denen Computer logische Denkprozesse ausführen. Anderer Klassiker Algorithmen in diesem Bereich, wie z DPLL-Algorithmus, erwarten Sie als Eingabe eine Formel in normaler Konjunktivform. Die Beschreibung zur konjunktiven Normalform kann mit Hilfe logischer Gesetze und mit dem Tseitin-Transformation; dieser Algorithmus liefert a Erfüllbarkeitsäquivalent Formel in normaler Konjunktivform at und no logisches Äquivalent Formel.
Umwandlung in konjunktive Normalform
Irgendeine Formel von klassisch Aussagenlogik kann in CNF umgewandelt werden, indem die folgenden Schritte wiederholt werden.
- beseitigen (Doppelimplikation) mit:
- beseitigen (Implikation) mit:
- Bewegung (Negation) nach innen mit:
- verteilen Über :
Für den Klassiker Prädikatslogik es gibt ein ähnliches Verfahren. In dem Modale Logik Eine Umstellung auf CNF ist nicht in allen Fällen möglich.
Erfüllbarkeit
Innerhalb der Komplexitätstheorie existiert eine Erfüllungsproblem wobei untersucht wird, ob eine Formel in konjunktiver Normalform erfüllbar ist; dieses Problem wird CNF-SAT genannt.
Es k-SAT-Problem besteht darin, eine Formel in normaler konjunktiver Form zu erfüllen, wobei jede Disjunkte k enthält Literale. Das Problem 3-SAT ist NP-vollständig (sowie alle anderen k-SAT-Problem für k > 2) während für 2-SAT eine Lösung in Polynomzeit kann gefunden werden.
Tautologie
Eintreten ist möglich Polynomzeit um zu prüfen, ob eine Formel in normaler Konjunktivform a . hat Tautologie ist (eine Formel, die immer wahr ist). Der Algorithmus in Pseudocode:
isCNFTautologie(formel f): für jedes verbinden Cimf: wennC enthält keine komplementären Literale: Rückkehrfalschtrue zurückgeben
Eine Formel in konjunktiver Normalform besteht aus einer Konjunktion von Disjunktionen, so dass die gesamte Formel wahr ist, wenn jede der Konjunkte wahr ist. Eine Disjunktion ist immer wahr, wenn sie ergänzende Literale enthält (beide p als seine Negation). Es ist also möglich, eine Formel durchzugehen und zu sehen, ob sie komplementäre Literale für jede der Konjunkte enthält. Wenn dies für jede der Konjunkte der Fall ist, ist die Formel eine Tautologie. Im Pseudocode oben nur wahr zurückgegeben, falls zutreffend; wenn für eine der Konjunktionen die gegebene Bedingung nicht gilt, dann wird schon gleich falsch ist zurückgekommen.
Wissenswertes
- EIN Verbindung ist auch in konjunktiver Normalform; jede der Disjunktionen enthält genau 1 Literal.