Als Konjunktive Normalform (kurz KNF) wird in der Aussagenlogik eine bestimmt Form von Formeln bezeichnet.
Definition
Eine Formel der Aussagenlogik ist in konjunktiver Normalform, wenn sie eine Konjunktion von Klauseln ist. Klauseln sind dabei Disjunktionen von Literalen (Volldisjunktionen). Eine Formel in KNF hat also die Form
Bildung
Jede Formel der Aussagenlogik lässt sich in konjunktive Normalform umwandeln, da sich auch jede boolesche Funktion mit einer KNF darstellen lässt. Dazu genügt es, die Zeilen ihrer Wahrheitstabelle abzulesen. Für jede Zeile, die als Resultat eine 0 liefert, wird eine Klausel gebildet, die alle Variablen der Funktion disjunktiv verknüpft. Variablen, die in der Zeile mit 0 belegt sind, werden dabei nicht negiert und Variablen, die mit 1 belegt sind, werden negiert. Diese Klauseln werden auch Maxterme genannt. Durch konjunktive Verknüpfung der Maxterme erhält man schließlich die konjunktive Normalform.
Auf diese Weise erhält man allerdings nicht immer eine minimale KNF, dass heißt eine KNF mit möglichst wenig Klauseln. Will man eine minimale KNF bilden, so kann man dies etwa mithilfe von Karnaugh-Venn-Diagrammen (kurz KV-Diagrammen) tun. (?)
Beispiel für die Bildung der KNF
Gesucht sei eine Formel in KNF für die boolesche Funktion mit drei Variablen x2, x1 und x0, die genau dann den Wahrheitswert 1 (wahr) annimmt, wenn die Dualzahl [x2x1x0]2 eine Primzahl ist.
Die Wahrheitstafel für diese Funktion hat folgende Gestalt:
| x2 | x1 | x0 | Ergebnis | Klausel |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | |
| 0 | 0 | 1 | 0 | |
| 0 | 1 | 0 | 1 | - |
| 0 | 1 | 1 | 1 | - |
| 1 | 0 | 0 | 0 | |
| 1 | 0 | 1 | 1 | - |
| 1 | 1 | 0 | 0 | |
| 1 | 1 | 1 | 1 | - |
Daraus ergibt sich die Formel
Entscheidbarkeit
Die Frage, ob die Variablen einer aussagenlogischen Formel so belegt werden können, dass die Aussage wahr wird, wird Erfüllbarkeitsproblem (kurz SAT) genannt. SAT gehört zur Klasse der NP-vollständigen Probleme und gilt damit im Allgemeinen als schwierig lösbar. Dies gilt auch für Formel, die in KNF vorliegen; eine Ausnahme bilden allerdings Horn-Formeln, die einen Spezialfall der KNF-Formeln darstellen und in Polynomialzeit auf Erfüllbarkeit getestet werden können.
Weitere Normalformen
Neben der konjunktiven Normalform gibt es in der Aussagenlogik weitere Normalformen, etwa die disjunktive Normalform oder die Negationsnormalform.