Konjunktive Normalform

Grundidee und Aufbau

Die konjunktive Normalform (KNF; englisch CNF für „conjunctive normal form“) ist eine festgelegte Form für Formeln der Aussagenlogik. Sie besteht aus mehreren Oder-Verknüpfungen, die durch Und-Verknüpfungen verbunden sind.

Genauer ist eine Formel in KNF eine Konjunktion von Disjunktionstermen. Ein Disjunktionsterm ist eine Disjunktion von Literalen. Literale sind Variablen entweder ohne Negation oder negiert, also beispielsweise A oder ¬A. Allgemein hat eine KNF die Form

∧ᵢ ∨ⱼ (¬)xᵢⱼ.

Ein Beispiel ist (A ∨ B ∨ C) ∧ (Ā ∨ B ∨ C). Die geklammerten Oder-Terme werden auch Klauseln genannt.

Kanonische Form

Die kanonische konjunktive Normalform (KKNF) besteht aus paarweise verschiedenen Maxtermen. Ein Maxterm ist hier eine Oder-Verknüpfung, in der jede Variable genau einmal vorkommt, entweder negiert oder nicht negiert.

Jede Boolesche Funktion besitzt genau eine KKNF. Sie wird auch vollständige konjunktive Normalform genannt.

Bildung aus der Wahrheitstabelle

Jede Formel der Aussagenlogik und damit jede Boolesche Funktion kann als KNF dargestellt werden. Zur Bildung der KKNF liest man die Zeilen der Wahrheitstabelle ab, deren Funktionswert 0 ist.

Für jede solche Zeile bildet man eine Klausel: Alle Variablen werden mit Oder verknüpft, wobei ihre Belegung invertiert wird. Eine Variable mit Wert 1 wird also negiert, eine Variable mit Wert 0 nicht negiert. Die so gebildeten Klauseln sind Maxterme. Ihre Und-Verknüpfung ergibt die KKNF.

Eine KKNF ist meist nicht minimal, sie hat also nicht unbedingt möglichst wenige Klauseln. Eine minimale Formel kann beispielsweise mit Karnaugh-Veitch-Diagrammen (KV-Diagrammen) bestimmt werden. Auch das Verfahren nach Quine und McCluskey kann verwendet werden: Zuerst wird die Formel negiert, dann mittels dieses Verfahrens in eine disjunktive Normalform überführt und anschließend wieder negiert.

Beispiel mit Primzahlen

Gesucht ist eine KNF für eine Boolesche Funktion mit den drei Variablen A, B und C. Sie soll genau dann den Wahrheitswert 1 haben, wenn die Dualzahl [ABC]₂ eine Primzahl ist.

Für jede Belegung mit Funktionswert 0 wird ein Maxterm gebildet. Die Variablen mit Wert 1 werden dabei negiert. Im Beispiel entstehen die Disjunktionen A ∨ B ∨ C, A ∨ B ∨ ¬C, ¬A ∨ B ∨ C und ¬A ∨ ¬B ∨ C. Durch Und-Verknüpfung erhält man:

(A ∨ B ∨ C) ∧ (A ∨ B ∨ ¬C) ∧ (¬A ∨ B ∨ C) ∧ (¬A ∨ ¬B ∨ C).

Die Klauseln sind dabei als Maxterme notiert. Jede KNF besitzt außerdem eine äquivalente DNF.

Erfüllbarkeit und andere Normalformen

Das Erfüllbarkeitsproblem, kurz SAT, fragt, ob sich die Variablen einer aussagenlogischen Formel so belegen lassen, dass die Formel wahr wird. SAT gehört zu den NP-vollständigen Problemen und gilt daher im Allgemeinen als schwierig lösbar. Dies gilt auch für Formeln in KNF.

Eine Ausnahme sind Horn-Formeln, ein Spezialfall von KNF-Formeln: Ihre Erfüllbarkeit kann in Polynomialzeit getestet werden. Grundsätzlich gibt es zwei Wege, einen aussagenlogischen Ausdruck auf Erfüllbarkeit zu prüfen: Man testet alle möglichen Variablenbelegungen, was eine semantische Herangehensweise ist, oder man verwendet den rein syntaktischen Resolutionskalkül.

Weitere Normalformen der Aussagenlogik sind die disjunktive Normalform, die Negationsnormalform und die kanonische Normalform.