Definition des DPLL-Algorithmus

Question

Ich habe einige Probleme beim Verständnis des DPLL-Algorithmus und frage mich, ob mir jemand erklären könnte, weil ich denke, dass mein Verständnis inkorrekt ist.

Wie ich es verstehe, nehme ich eine Menge von Literalen und wenn jede Klausel wahr ist, ist das Modell wahr, aber wenn eine Klausel falsch ist, ist das Modell falsch.

Ich überprüfe das Modell rekursiv, indem ich nach einer Einheitsklausel suche. Wenn es eine gibt, setze ich den Wert für diese Einheitsklausel so, dass sie wahr wird, und aktualisiere dann das Modell. Ich entferne alle Klauseln, die jetzt wahr sind, und entferne alle Literale, die jetzt falsch sind.

Wenn keine Einheitsklauseln mehr übrig sind, wähle ich ein anderes Literal und weise Werte für dieses Literal zu, die es wahr und falsch machen, und entferne dann wieder alle Klauseln, die jetzt wahr sind und alle Literale, die jetzt falsch sind.

Answer 1

DPLL erfordert, dass ein Problem im disjunktiven Normalformzustand formuliert wird, das heißt als eine Menge von Klauseln, von denen jede erfüllt sein muss.

Jede Klausel ist eine Menge von Literalen {l1, l2, ..., ln}, die die Disjunktion dieser Literale darstellen (dh mindestens ein Literal muss wahr sein, damit die Klausel erfüllt ist).

Jedes Literal l besagt, dass eine Variable wahr (x) ist oder dass sie falsch (~x) ist.

Wenn ein Literal in einer Klausel wahr ist, wird die Klausel erfüllt.

Wenn alle Literale in einer Klausel falsch sind, ist die Klausel unlösbar und somit das Problem unlösbar.

Eine Lösung ist eine Zuweisung von Wahrheits-/Falschheitswerten an die Variablen, sodass jede Klausel erfüllt ist. Der DPLL-Algorithmus ist eine optimierte Suche nach einer solchen Lösung.

DPLL ist im Wesentlichen eine Tiefensuche, die zwischen drei Taktiken wechselt. Zu jedem Zeitpunkt in der Suche gibt es eine teilweise Zuweisung (dh eine Zuweisung von Werten an eine Teilmenge der Variablen) und eine Menge von unentschiedenen Klauseln (dh die Klauseln, die noch nicht erfüllt wurden).

(1) Die erste Taktik ist die Eliminierung reiner Literale: Wenn eine nicht zugewiesene Variable x nur in ihrer positiven Form in der Menge der unentschiedenen Klauseln erscheint (dh das Literal ~x nirgendwo erscheint), dann können wir einfach x = true zu unserer Zuweisung hinzufügen und alle Klauseln befriedigen, die das Literal x enthalten (ähnlich, wenn x nur in seiner negativen Form, ~x, erscheint, können wir einfach x = false zu unserer Zuweisung hinzufügen).

(2) Die zweite Taktik ist die Einheitspropagation: Wenn alle außer einem Literal in einer unentschiedenen Klausel falsch sind, muss das verbleibende wahr sein. Wenn das verbleibende Literal x ist, fügen wir x = true zu unserer Zuweisung hinzu; wenn das verbleibende Literal ~x ist, fügen wir x = false zu unserer Zuweisung hinzu. Diese Zuweisung kann zu weiteren Möglichkeiten für die Einheitspropagation führen.

(3) Die dritte Taktik ist einfach eine nicht zugewiesene Variable x auszuwählen und die Suche zu verzweigen: eine Seite versucht x = true, die andere versucht x = false.

Wenn wir an einem Punkt eine unlösbare Klausel erhalten, haben wir eine Sackgasse erreicht und müssen zurückverfolgen.

Es gibt allerlei clevere weitere Optimierungen, aber dies ist der Kern fast aller SAT-Löser.

Hoffentlich hilft das weiter.

Answer 2

Der Davis-Putnam-Logemann-Loveland (DPLL) -Algorithmus ist ein Backtracking-basierter Suchalgorithmus zur Entscheidung der Erfüllbarkeit von aussagenlogischen Formeln in konjunktiver Normalform, auch bekannt als Erfüllbarkeitsproblem oder SAT.

Jede boolesche Formel kann in konjunktiver Normalform (CNF) ausgedrückt werden, was eine Konjunktion von Klauseln bedeutet, d.h. (…) ^ (…) ^ (…)

wo eine Klausel eine Disjunktion von booleschen Variablen ist, d.h. (A v B v C' v D)

ein Beispiel für eine boolesche Formel in CNF ausgedrückt ist

(A v B v C) ^ (C' v D) ^ (D' v A)

und das Lösen des SAT-Problems bedeutet, die Kombination von Werten für die Variablen in der Formel zu finden, die sie erfüllen, wie z.B. A=1, B=0, C=0, D=0

Dies ist ein NP-vollständiges Problem. Tatsächlich ist es das erste Problem, das von Stepehn Cook und Leonid Levin als NP-vollständig nachgewiesen wurde.

Ein bestimmter Typ von SAT-Problem ist das 3-SAT, bei dem alle Klauseln drei Variablen enthalten.

Der DPLL-Algorithmus ist eine Möglichkeit, das SAT-Problem zu lösen (was praktisch von der Schwierigkeit des Inputs abhängt), der rekursiv einen Baum potenzieller Lösungen erstellt

Angenommen, Sie möchten ein 3-SAT-Problem wie dieses lösen

(A v B v C) ^ (C' v D v B) ^ (B v A' v C) ^ (C' v A' v B')

Wenn wir die Variablen nummerieren, z. B. A=1, B=2, C=3, D=4, und negative Zahlen für negierte Variablen verwenden, z. B. A' = -1, dann kann dieselbe Formel in Python wie folgt geschrieben werden

[[1,2,3],[-3,4,2],[2,-1,3],[-3,-1,-2]]

stellen Sie sich nun vor, einen Baum zu erstellen, in dem jeder Knoten aus einer Teil-Lösung besteht. In unserem Beispiel haben wir auch einen Vektor der durch die Lösung erfüllten Klauseln dargestellt

Der Wurzelknoten ist [-1,-1,-1,-1], was bedeutet, dass den Variablen noch keine Werte zugewiesen wurden, weder 0 noch 1

bei jeder Iteration:

1. wir nehmen die erste unerfüllte Klausel dann

2. wenn es keine weiteren unzugewiesenen Variablen gibt, die wir verwenden können, um diese Klausel zu erfüllen, können keine gültigen Lösungen in diesem Zweig des Suchbaums existieren und der Algorithmus gibt None zurück

3. ansonsten nehmen wir die erste unzugewiesene Variable und setzen sie so, dass sie die Klausel erfüllt und beginnen rekursiv von Schritt 1. Wenn der innere Aufruf des Algorithmus None zurückgibt, kehren wir den Wert der Variablen um, sodass sie die Klausel nicht erfüllt, und setzen die nächste unzugewiesene Variable, um die Klausel zu erfüllen. Wenn alle drei Variablen ausprobiert wurden oder keine weiteren unzugewiesenen Variablen für diese Klausel vorhanden sind, bedeutet dies, dass es keine gültigen Lösungen in diesem Zweig gibt und der Algorithmus None zurückgibt

Sehen Sie sich das folgende Beispiel an:

Vom Wurzelknoten aus wählen wir die erste Variable (A) der ersten Klausel (A v B v C) und setzen sie so, dass sie die Klausel erfüllt, dann A=1 (zweiter Knoten des Suchbaums)

fahren Sie mit der zweiten Klausel fort und wählen die erste unzugewiesene Variable (C) und setzen sie so, dass sie die Klausel erfüllt, was bedeutet, dass C=0 (dritter Knoten links)

wir tun dasselbe für die vierte Klausel (B v A' v C) und setzen B auf 1

wir versuchen dasselbe für die letzte Klausel, müssen jedoch feststellen, dass wir keine unzugewiesenen Variablen mehr haben und die Klausel immer falsch ist. Dann müssen wir in den vorherigen Teil des Suchbaums zurückgehen. Wir ändern den Wert, den wir B zugewiesen haben, und setzen B auf 0. Dann suchen wir nach einem anderen unzugewiesenen Wert, der die dritte Klausel erfüllen kann, aber es gibt keinen. Dann müssen wir wieder zum zweiten Knoten zurückkehren

Dort müssen wir die Zuweisung der ersten Variablen (C) umkehren, damit sie die Klausel nicht erfüllt, und die nächste unzugewiesene Variable (D) so setzen, dass sie diese erfüllt (d.h. C=1 und D=1). Dies erfüllt auch die dritte Klausel, die C enthält.

Die letzte zu erfüllende Klausel (C' v A' v B') hat eine unzugewiesene Variable B, die dann auf 0 gesetzt werden kann, um die Klausel zu erfüllen.

In diesem Link http://lowcoupling.com/post/72424308422/a-simple-3-sat-solver-using-dpll finden Sie auch den Python-Code zur Implementierung