Es besteht die Möglichkeit, eine Abbildung zu definieren, die konjunktive Normalformen auf boolesche Felder abbildet. Dies geschieht in einer Form, dass Produkte der Felder mit Erfüllbarkeitsbedingungen der konjunktiven Normalformen verträglich sind. Erfüllende Belegungen der Elementaraussagen für eine erfüllbare konjunktive Normalform können dann durch Fixpunkte von Abbildungen boolescher Vektoren ermittelt werden. Hierüber wird die Erfüllbarkeit von konjunktiven Normalformen in Polynomialzeit entscheidbar, für die dies bisher noch nicht bekannt war [3],[4]. Es gibt eine aufsteigende Klasse von k-dichten konjunktiven Normalformen, deren Erfüllbarkeit mit einem Aufwand von O(n^(3k-1)) booleschen Operationen entscheidbar ist. Sind die Werte von k im Verhältnis zu n groß, so ist diese Größenordnung mit einem exponentiellen Aufwand vergleichbar.
HIER geht es zu einer Kurzfassung.
Die ausführliche Beschreibung findet sich in der pdf-Datei.
 | Boolesche Felder - KNF Boolesche Felder-KNF.pdf (272.86KB) |
| Boolesche Felder-KNF.pdf (272.86KB) |