Logo

DISKRETE MATHEMATIK
Erich Prisner
Sommersemester 2000

Erfüllbarkeit

Aussagenlogisch

 Beim "Satisfyability-Problem" SAT geht es darum: Gegeben ist eine Aussageformel in (nichtkanonischer!) konjunktiver Normalform. Die Frage ist, ob diese Formel erfüllbar ist oder nicht. Natürlich läßt sich jede solche Frage entscheiden (etwa durch Ausprobieren aller 2n möglichen Modelle, falls wir n Aussagevariable haben), aber wie geht es am schnellsten?

Zur Terminologie: Ein Literal ist entweder eine Aussagevariable oder ihre Negation. Eine Klausel ist eine Menge endlich vieler Literale. Klauseln stehen für die Disjunktion der darin vorkommenden Elemente, d.h. die Klausel {P, ØQ, R} für P Ú ØQ Ú R.

Ist nun eine gegebene endliche Menge von Klausel; erfüllbar?

Resolution

Dies ist eine Inferenzregel, mit der eine erfüllbare Mengen von Klauseln erfüllbar erweitert werden kann. Seien C È {P} und D È {Ø P} zwei Klauseln aus einer erfüllbaren Klauselmenge. Ist in der Erfüllung P wahr, so muß D erfüllt sein, andernfalls C; also muß in jedem Fall die Klausel C È D auch erfüllbar sein. D.h. wir schließen aus den beiden Klauseln C È {P} und D È {Ø P} auf die Klausel C È D. Falls wir die (unerfüllbare) leere Klausel Æ ableiten können, kann also die Ausgangsmenge nicht erfüllbar gewesen sein. Umgekehrt können wir aus unerfüllbaren Klauselmengen immer auch die leere Menge ableiten (notfalls indem wir systematisch alle Ableitungen erzeugen, was aber dauern kann!).

2-SAT und 3-SAT

 Wir betrachten die Probleme 2-SAT bzw. 3-SAT, bei denen jede Klausel nur zwei bzw. drei sogenannte Literale enthält. Interessanterweise sind 2-SAT Probleme "leicht" zu lösen, während 3-SAT Probleme i.A. "schwer" zu lösen sind.

Jede Instanz des 2-SAT Problems läßt sich in polynomieller Zeit mit Hilfe von Digraphen lösen.
Beweis: Wir konstruieren einen Digraphen dessen Eckenmenge die Menge aller vorkommenden Literale und deren Negationen ist. Für jede Klausel {A,B} ziehen wir eine gerichtete Kante von A nach Ø B und genauso eine gerichtete Kante von B nach Ø A. In jeder Erfüllung der Klauselmenge impliziert Falschheit von A Wahrheit von B, also Falschheit von Ø B. D.h. die Relation ist eine Teilrelation der Relation "wenn ... falsch ist, dann auch ...".

Nun berechnen wir die starke Zusammenhangskomponenten des Digraphen.

Falls ein Literal mit seiner Negation in derselben Komponente liegt, dann müssen, da ja eins von beiden in jeder Erfüllung falsch ist, beide falsch sein, ein Widerspruch. Also gibt es in diesem Fall gar keine erfüllende Belegung; die Klauselmenge ist unerfüllbar.

Andernfalls liegt jedes Literal in einer anderen Komponente als seine Negation. Liegen die Literale P und Q in derselben starken Komponente, so liegen auch ihre Negationen ØP und ØQ in einer gemeinsamen starken Komponente (denn P ® P2 ® ... ® Q impliziert ØQ ® ... ® ØP2 ® ØP). Deshalb ist zu jeder starken Komponente die Menge der Negationen dieser Literale auch eine starke Komponente.
Nun zeigen wir, daß und wie man dann eine erfüllende Belegung finden kann---wir weisen einfach nacheinander Wahrheitswerte zu. Angenommen P und ØP haben noch keinen Wahrheitswert zugewiesen bekommen. Ist P von ØP aus nicht erreichbar, so setzen wir P="falsch", also ØP="wahr"; andernfalls ist nach Voraussetzung ØP von P aus nicht erreichbar und wir setzen P="wahr" und ØP="falsch". Alle Literale in derselben starken Komponente erhalten auch denselben Wahrheitswert wie P (und damit alle ihre Negationen, d.h. alle Literale in derselben starken Komponente wie ØP, denselben Wahrheitswert wie ØP). Wir fahren so lange fort bis alle Literale einen Wahrheitswert haben, und haben damit eine erfüllende Belegung konstruiert. Die Klauselmenge ist in dem Fall also erfüllbar.

Das 3-SAT Problem ist NP-vollständig, d.h. ...

Prädikatenlogisch

 Wie entscheidet man, ob eine gegebene Aussage in einer Sprache erster Ordnung erfüllbar ist? Die Frage läßt sich mehr oder weniger auf obiges aussagenlogische SAT-Problem zurückführen; allerdings gibt es einige praktische Schwierigkeiten, auf die wir hier nicht näher eingehen werden.

Ein Literal ist in der Prädikatenlogik eine Primformel oder ihre Negation. Wie oben ist eine Klausel eine Menge endlich vieler Literale und steht für deren Disjunktion.

Wir starten mit einer Aussage. "x "y $z "u "v [ (R(x,F(y)) Ú S(y)) Ù (Ø S(z) Ú R(z,y)) Ù (Ø S(F(x)) Ú Ø R(x,F(z))) Ù (Ø R(u,v) Ú S(F(v))) ]
Diese bringen wir (hier durch Einführung des neuen binären Verknüpfungssymbols "G") auf Skolemsche Normalform mit Matrix in konjunktiver Normalform. Sie ist erfüllungsäquivalent zur ursprünglichen Formel, d.h. genau dann erfüllbar, wenn obige es war. "x "y "u "v [ (R(x,F(y)) Ú S(y)) Ù (Ø S(G(x,y)) Ú R(G(x,y),y)) Ù (Ø S(F(x)) Ú Ø R(x,F(G(x,y)))) Ù (Ø R(u,v) Ú S(F(v))) ]
Nun betrachten wir die Menge der Klauseln der Matrix. {R(x,F(y)), S(y)}
{Ø S(G(x,y)), R(G(x,y),y)}
{Ø S(F(x)), Ø R(x,F(G(x,y)))}
{Ø R(u,v), S(F(v))}
Für Variablen können wir Terme einsetzen. Dadurch können wir die Klauselmenge beliebig vergrößern. Hier muß man im Allgemeinen intelligent vorgehen, Stichwort "Unifikation". Einsetzen ergibt unter Anderem:
{R(x,F(G(x,y))), S(G(x,y))}
{Ø S(G(x,y)), R(G(x,y),x)}
{Ø S(F(x)), Ø R(x,F(G(x,y)))}
{Ø R(G(x,y),x), S(F(x))}
Die Ausgangsformel ist genau dann unerfüllbar, wenn wir so eine endliche Klauselmenge konstruieren können, die aussagenlogisch unerfüllbar ist, d.h. aus der sich die leeren Menge mittels Resolution herleiten läßt. Aus den vier aussagenlogischen Klauseln
{P1, P2}, {ØP2, P3}, {Ø P4, Ø P1}, {ØP3, P4} ist die leere Klausel herleitbar.

Mit Vorsicht kann man so auch Folgern. Da Skolemisierung zwar Widersprüchlichkeit, nicht aber die logische Folgerungsbeziehung erhält, muß man dabei aber vorsichtig sein. Es genügt nicht, zu prüfen ob sich die Skolem-Form von B aus der Skolem-Form von A ableiten läßt.

Weiter zu ...
Erich Prisner
erstellt im Juni 2000.