Konjunktive Normalform

aus Wikipedia, der freien Enzyklopädie

Du hast neue Nachrichten (Unterschied zur vorletzten Version).

Als konjunktive Normalform (kurz KNF) wird in der Aussagenlogik eine bestimmte Form von Formeln bezeichnet.

Inhaltsverzeichnis

1 Definition
2 Bildung
3 Beispiel für die Bildung der KNF
4 Entscheidbarkeit
5 Weitere Normalformen
6 Weblinks

[Bearbeiten] Definition

Eine Formel der Aussagenlogik ist in konjunktiver Normalform, wenn sie eine Konjunktion von Disjunktionstermen ist. Disjunktionsterme sind dabei Disjunktionen von Literalen. Literale sind nichtnegierte oder negierte Variablen. Eine Formel in KNF hat also die Form

$\bigwedge_i \bigvee_j (\neg)x_{ij}.$

[Bearbeiten] 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 mit der invertierten Belegung verknüpft. 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 in der Regel keine minimale Formel, das heißt eine Formel mit möglichst wenig Klauseln. Will man eine minimale Formel bilden, so kann man dies etwa mit Hilfe von Karnaugh-Veitch-Diagrammen (kurz KV-Diagrammen) tun.

[Bearbeiten] Beispiel für die Bildung der KNF

Gesucht sei eine Formel in KNF für die boolesche Funktion mit drei Variablen x₂, x₁ und x₀, die genau dann den Wahrheitswert 1 (wahr) annimmt, wenn die Dualzahl [x₂x₁x₀]₂ eine Primzahl ist.

Die Wahrheitstafel für diese Funktion hat folgende Gestalt:

x₂	x₁	x₀	Ergebnis	Klausel*
0	0	0	0	$x_2 \vee x_1 \vee x_0$
0	0	1	0	$x_2 \vee x_1 \vee \bar{x_0}$
0	1	0	1	-
0	1	1	1	-
1	0	0	0	$\bar{x_2} \vee x_1 \vee x_0$
1	0	1	1	-
1	1	0	0	$\bar{x_2} \vee \bar{x_1} \vee x_0$
1	1	1	1	-

*Maxterme.

Daraus ergibt sich die Funktion:

$y = (x_2 \vee x_1 \vee x_0) \wedge (x_2 \vee x_1 \vee \bar{x_0}) \wedge (\bar{x_2} \vee x_1 \vee x_0) \wedge (\bar{x_2} \vee \bar{x_1} \vee x_0)$

[Bearbeiten] 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 Formeln, 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. Es gibt im Grunde zwei Ansätze, wie ein aussagenlogischer Ausdruck auf seine Erfüllbarkeit überprüft werden kann: durch Testen aller möglichen Belegungen seiner Variablen (semantische Herangehensweise) oder durch den Resolutionskalkül (rein syntaktisch).