Dieses ¨Ubungsblatt beschreibt die erste Praktikumsaufgabe. Sie sollen dabei den Davis-
Putnam-Logemann-Loveland–Algorithmus (DPLL) zur Berechnung der Modelle aussagenlogischer
Formeln in konjunktiver Normalform (engl. Conjunctive Normal Form; CNF)
in PROLOG implementieren.
Folgende Begriffe spielen im Kontext dieser Aufgabe wichtige Rollen:
Aussagenlogische Variable: Eine aussagenlogische Variable kann mit den Werten true
und false belegt werden.
Literal: F¨ur eine aussagenlogische Variable X sind X und ¬X Literale. Das positive
Literal X ist in einer Interpretation I wahr, wenn X in I den Wert true hat. Analog
ist das negative Literal ¬X in I wahr, wenn X in I den Wert false hat.
Klausel: Eine Klausel ist eine Disjunktion von Literalen. Wir repr¨asentieren eine Klausel
C = l1 _ . . . _ ln durch die Menge {l1, . . . , ln} der in C enthaltenen Literale.
Konjunktive Normalform (CNF): Eine aussagenlogische Formel ist in konjunktiver
Normalform, wenn F eine Konjunktion von Klauseln ist. Wir repr¨asentieren eine
aussagenlogische Formel F = C1 ^ . . . ^ Cm in CNF durch die Menge {C1, . . . ,Cm} der in F enthaltenen Klauseln.
Partielle Interpretation: Eine partielle Interpretation I ist eine Menge von Literalen.
Eine aussagenlogische Variable X hat in I den Wert true (false), wenn X 2 I
(¬X 2 I). Eine partielle Interpretation ist bzgl. einer aussagenlogischen Formel F
total, wenn jede in F vorkommende Variable belegt ist.
Modell: Eine totale Interpretation I einer aussagenlogischen Formel F ist ein Modell
von F, wenn F bzgl. I wahr ist. F¨ur aussagenlogische Formeln F = {C1, . . . ,Cm} in CNF heißt das: In jeder Klausel Ci = {l1, . . . , ln} 2 F gibt es ein Literal lj 2 Ci,
sodass lj 2 I.
Nachfolgend geben wir DPLL als Entscheidungsalgorithmus f¨ur aussagenlogische Erf¨ullbarkeit
an. Die Eingaben des Algorithmus sind eine partielle Interpretation I, repr¨asentiert
als Menge von Literalen, sowie eine aussagenlogische Formel F in CNF, repr¨asentiert als
Menge von Klauseln.
Die Grundidee von DPLL ist wie folgt:
1. L¨osche alle in I falschen Literale aus den Klauseln von F.
2. Sollte eine Klausel leer werden, gebe false zur¨uck.
3. F¨uge Literale, die in Klauseln der L¨ange 1 vorkommen, zu I hinzu.
4. Wenn I total ist, gebe true zur¨uck.
5. Ansonsten w¨ahle eine unbelegte Variable X aus F und belege X nacheinander mit
true und false. Wenn entweder I [ {X} oder I [ {¬X} zu einem Modell von F
erweitert werden kann, gebe true zur¨uck, sonst false.
Die obigen Schritte 1–3 werden Unit-Propagation genannt. DPLL basiert auf deterministischer
Inferenz, Unit-Propagation, und nicht-deterministischer Suche (Schritt 5):
DPLL(I, F)
UnitPropagation(I, F)
if ; 2 F then return false
if there is a variable X in F such that neither X nor ¬X is in I then
if DPLL(I [ {X}, F) then return true
else return DPLL(I [ {¬X}, F)
else return true
UnitPropagation(I, F)
do
F0 F
for every clause C 2 F do
C0 C \ ({X | ¬X 2 I} [ {¬X | X 2 I})
F (F \ {C}) [ {C0}
if |C0| = 1 then I I [ {C0}
end for
while F 6= F0
Ihre Aufgabe besteht im Folgenden darin, DPLL in PROLOG zu implementieren. Auf
derWebseite zu den ¨Ubungen finden sie als Grundger¨ust die Datei dpll.pl. In dieser Datei
werden Eingabe- und Ausgabeformate sowie einige richtig zu beantwortende Testanfragen
vorgegeben. Anstelle eines Entscheidungsalgorithmus wird DPLL dabei so aufgefasst, dass
die Modelle einer aussagenlogischen Formel F in CNF berechnet werden.
