Zurück

Beleg der Erfüllbarkeit mittels Resolutionsverfahren

Das Resolutionsverfahren lässt sich nicht nur nutzen, um die Allgemeingültigkeit einer Formel nachzuweisen, sondern auch, um zu belegen, dass dies eben nicht der Fall ist. Das bedeutet, dass mittels Resolution in endlicher Zeit alle möglichen Resolutionsableitungen einer gegebenen Formel gebildet werden können. Besteht keine dieser Ableitungen aus einer leeren Klausel (bzw. eine Resolutionswiederlegung) bedeutet dies, dass die Negation ¬ F der Formel F erfüllbar ist. F ist damit wiederlegbar und nicht allgemeingültig.
Durch diese Eigenschaft stellt die Resolution ein Entscheidungsverfahren dar.
Nachfolgend wird an einem Beispiel die Erfüllbarkeit einer Formel mittels Resolution illustriert.

Beweise mittels Resolutionsverfahren, dass die Formel (in Klausel-Normalform)
$$ \langle [\neg{a},b,\neg{c}],[\neg{a},b,d],[a,b],[b,c],[b,\neg{d}] \rangle $$ erfüllbar ist.

1
$$ [\neg{a},b,\neg{c}] $$
2
$$ [\neg{a},b,d] $$
3
$$ [a,b] $$
4
$$ [b,c] $$
5
$$ [b,\neg{d}] $$
6
$$ - $$
res(1,2)
6
$$ [b,\neg{c}] $$
res(1,3)
7
$$ [\neg{a},b] $$
res(1,4)
8
$$ - $$
res(1,5)
8
$$ [b,d] $$
res(2,3)
9
$$ - $$
res(2,4)
9
$$ [\neg{a},b] $$
res(2,5)
9
$$ - $$
res(3,4)
9
$$ - $$
res(3,5)
9
$$ - $$
res(4,5)
9
$$ - $$
res(1,6)
9
$$ - $$
res(1,7)
9
$$ - $$
res(1,8)
9
$$ - $$
res(2,6)
9
$$ - $$
res(2,7)
9
$$ - $$
res(2,8)
9
$$ - $$
res(3,6)
9
$$ [b] $$
res(3,7)
10
$$ - $$
res(3,8)
10
$$ [b] $$
res(4,6)
10
$$ - $$
res(4,7)
10
$$ - $$
res(4,8)
10
$$ - $$
res(5,6)
10
$$ - $$
res(5,7)
10
$$ [b] $$
res(5,8)
10
$$ - $$
res(6,7)
10
$$ - $$
res(6,8)
10
$$ - $$
res(7,8)
keine weiteren Resolventen

Beleg der Erfüllbarkeit mittels Resolutionsverfahren. Die Bildung aller gültigen Resolutionsableitungen führt nicht zu einer leeren Klausel. Auf den letzten Iterationsschritt wurde an dieser Stelle verzichtet, da es keine Resolutionsableitung gibt, welche aus dem Literal [b] und einem Literal mit zwei oder mehreren aussagenlogischen Variablen zu einer leeren Klausel führt. Im jeweiligen Schritt sind immer die zur Resolventenbildung betrachteten Teilformeln (bzw. Zeilen in der Tabelle) farbig hinterlegt. Ergibt sich aus den Teilformeln eine neue Resolvente, so ist die Hinterlegung grün. Lässt sich hingegen keine Resolvente bilden oder ist diese bereits vorhanden, so ist die Hinterlegung rot.