DPLL-Algorithmus

In der Logik und Informatik ist der Davis-Putnam-Logemann-Loveland (DPLL)-Algorithmus ein vollständiger, auf Backtracking basierender Suchalgorithmus zur Bestimmung der Erfüllbarkeit von Formeln der Aussagenlogik in konjunktiver Normalform, d. h. zur Lösung des CNF-SAT-Problems.

Er wurde 1961 von Martin Davis, George Logemann und Donald W. Loveland eingeführt und ist eine Verfeinerung des früheren Davis-Putnam-Algorithmus, der ein von Davis und Hilary Putnam 1960 entwickeltes auflösungsbasiertes Verfahren ist. Vor allem in älteren Veröffentlichungen wird der Davis-Logemann-Loveland-Algorithmus oft als „Davis-Putnam-Methode“ oder „DP-Algorithmus“ bezeichnet. Andere gebräuchliche Bezeichnungen, die diese Unterscheidung beibehalten, sind DLL und DPLL.

Implementierungen und Anwendungen

Das SAT-Problem ist sowohl aus theoretischer als auch aus praktischer Sicht von Bedeutung. In der Komplexitätstheorie war es das erste Problem, das sich als NP-vollständig erwiesen hat, und es kann in einer Vielzahl von Anwendungen vorkommen, z. B. bei der Modellprüfung, der automatischen Planung und Terminierung und der Diagnose in der künstlichen Intelligenz.

Daher ist die Entwicklung effizienter SAT-Löser seit vielen Jahren ein Forschungsthema. GRASP (1996–1999) war eine frühe Implementierung unter Verwendung von DPLL. Bei den internationalen SAT-Wettbewerben belegten Implementierungen auf der Grundlage von DPLL wie zChaff und MiniSat in den Jahren 2004 und 2005 die ersten Plätze.

Eine weitere Anwendung, bei der DPLL häufig zum Einsatz kommt, ist das automatisierte Theorembeweisen oder die Satisfiability Modulo Theories (SMT), ein SAT-Problem, bei dem propositionale Variablen durch Formeln einer anderen mathematischen Theorie ersetzt werden.

Der Algorithmus

Der grundlegende Backtracking-Algorithmus läuft so ab, dass ein Literal ausgewählt, diesem ein Wahrheitswert zugewiesen, die Formel vereinfacht und dann rekursiv geprüft wird, ob die vereinfachte Formel erfüllbar ist. Ist dies der Fall, so ist die ursprüngliche Formel erfüllbar; andernfalls wird dieselbe rekursive Prüfung unter Annahme des entgegengesetzten Wahrheitswertes durchgeführt. Dies wird als Splitting-Regel bezeichnet, da sie das Problem in zwei einfachere Teilprobleme aufteilt. Durch den Vereinfachungsschritt werden im Wesentlichen alle Klauseln, die durch die Zuweisung wahr werden, aus der Formel entfernt, und alle Literale, die falsch werden, aus den verbleibenden Klauseln.

Der DPLL-Algorithmus verbessert sich gegenüber dem Backtracking-Algorithmus durch die gezielte Anwendung der folgenden Regeln bei jedem Schritt:

Weitergabe von Einheiten

• Wenn eine Klausel eine Einheitsklausel ist, d. h. sie enthält nur ein einziges nicht zugewiesenes Literal, kann diese Klausel nur durch Zuweisung des erforderlichen Wertes erfüllt werden, um dieses Literal wahr zu machen. Es ist also keine Auswahl erforderlich. Die Einheitspropagierung besteht darin, jede Klausel zu entfernen, die das Literal einer Einheitsklausel enthält, und das Komplement des Literales einer Einheitsklausel aus jeder Klausel zu verwerfen, die dieses Komplement enthält. In der Praxis führt dies oft zu deterministischen Kaskaden von Einheiten, wodurch ein großer Teil des naiven Suchraums vermieden wird.

Reine Literaleliminierung

• Wenn eine Satzvariable nur mit einer Polarität in der Formel vorkommt, wird sie als rein bezeichnet. Ein reines Literal kann immer so zugewiesen werden, dass alle Klauseln, die es enthalten, wahr werden. Wenn es also auf diese Weise zugewiesen wird, schränken diese Klauseln die Suche nicht mehr ein und können gelöscht werden.

Die Unerfüllbarkeit einer gegebenen Teilzuweisung wird festgestellt, wenn eine Klausel leer wird, d. h. wenn alle Variablen so zugewiesen wurden, dass die entsprechenden Literale falsch sind. Die Erfüllbarkeit der Formel wird entweder festgestellt, wenn alle Variablen zugewiesen werden, ohne dass die leere Klausel entsteht, oder, in modernen Implementierungen, wenn alle Klauseln erfüllt sind. Die Unerfüllbarkeit der vollständigen Formel kann nur nach einer erschöpfenden Suche festgestellt werden.

Der DPLL-Algorithmus lässt sich in folgendem Pseudocode zusammenfassen, wobei Φ die CNF-Formel ist:

    Eingabe: Eine Menge von Klauseln Φ.
    Ausgabe: Ein Wahrheitswert, der angibt, ob Φ erfüllbar ist.

Funktion DPLL(Φ)
    // Weitergabe von Einheiten:
    while es gibt eine Einheitsklausel {l} in Φ do
        Φ ← unit-propagate(l, Φ);
    // reine Literaleliminierung:
    while gibt es ein Literal l, das rein in Φ do vorkommt
        Φ ← pure-literal-assign(l, Φ);
    // Haltebedingungen:
    if Φ leer ist then
        return true;
    if Φ eine leere Klausel enthält, dann
        return false;
    // DPLL-Prozedur:
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {¬l});

In diesem Pseudocode sind unit-propagate(l, Φ) und pure-literal-assign(l, Φ) Funktionen, die das Ergebnis der Anwendung der unit-propagate- bzw. der pure-literal-Regel auf das Literal l und die Formel Φ zurückgeben. Mit anderen Worten: Sie ersetzen jedes Vorkommen von l durch „wahr“ und jedes Vorkommen von nicht l durch „falsch“ in der Formel Φ und vereinfachen die resultierende Formel. Das oder in der Return-Anweisung ist ein Kurzschlussoperator. Φ ∧ {l} bezeichnet das vereinfachte Ergebnis der Ersetzung von l durch „wahr“ in Φ.

Der Algorithmus bricht in einem von zwei Fällen ab. Entweder ist die CNF-Formel Φ leer, d. h. sie enthält keine Klausel. Dann ist sie durch jede beliebige Zuweisung erfüllt, da alle ihre Klauseln leer wahr sind. Andernfalls, wenn die Formel eine leere Klausel enthält, ist die Klausel leer falsch, da eine Disjunktion mindestens ein wahres Glied erfordert, damit die Gesamtmenge wahr ist. In diesem Fall bedeutet das Vorhandensein einer solchen Klausel, dass die Formel (ausgewertet als Konjunktion aller Klauseln) nicht als wahr ausgewertet werden kann und nicht erfüllbar sein muss.

Die Pseudocode-DPLL-Funktion gibt nur zurück, ob die endgültige Zuordnung die Formel erfüllt oder nicht. In einer realen Implementierung wird bei Erfolg typischerweise auch die teilerfüllende Zuweisung zurückgegeben; dies lässt sich aus der Verfolgung von verzweigenden Literalen und den Literalzuweisungen ableiten, die während der Einheitenfortpflanzung und der reinen Literaleliminierung vorgenommen werden.

Der Davis-Logemann-Loveland-Algorithmus hängt von der Wahl des Verzweigungsliterales ab, d. h. des Literales, das im Backtracking-Schritt berücksichtigt wird. Folglich handelt es sich nicht um einen Algorithmus, sondern um eine Familie von Algorithmen, einen für jede mögliche Wahl des Verzweigungsliterales. Die Effizienz wird durch die Wahl des Verzweigungsliterales stark beeinflusst: Es gibt Fälle, bei denen die Laufzeit je nach Wahl des Verzweigungsliterales konstant oder exponentiell ist. Solche Wahlfunktionen werden auch als heuristische Funktionen oder Verzweigungsheuristiken bezeichnet[5].

Visualisierung

Davis, Logemann, Loveland (1961) hatten diesen Algorithmus entwickelt. Einige Eigenschaften dieses ursprünglichen Algorithmus sind:

• Er basiert auf der Suche.
• Er ist die Grundlage für fast alle modernen SAT-Löser.
• Er verwendet kein Lernen oder nicht-chronologisches Backtracking (eingeführt 1996).

Ein Beispiel mit Visualisierung für einen DPLL-Algorithmus mit chronologischem Backtracking:

• 
  Alle Klauseln, die eine CNF-Formel bilden
• 
  Wählen Sie eine Variable
• 
  Entscheidung treffen, Variable a = Falsch (0), damit wird grüne Klausel Wahr
• 
  Nachdem wir mehrere Entscheidungen getroffen haben, finden wir einen Implikationsgraph, der zu einem Konflikt führt.
• 
  Nun kehren wir auf die unmittelbare Ebene zurück und weisen dieser Variablen zwangsweise den entgegengesetzten Wert zu
• 
  Aber eine erzwungene Entscheidung führt immer noch zu einem weiteren Konflikt
• 
  Zurück zur vorherigen Ebene gehen und eine erzwungene Entscheidung treffen
• 
  Eine neue Entscheidung treffen, aber sie führt zu einem Konflikt
• 
  Eine erzwungene Entscheidung treffen, aber sie führt wieder zu einem Konflikt
• 
  Zurückgehen zum vorherigen Level
• 
  Weiter so und der letzte Implikationsgraph

Verwandte Algorithmen

Seit 1986 werden auch (reduzierte geordnete) binäre Entscheidungsbäume zur SAT-Lösung verwendet.

In den Jahren 1989–1990 wurde die Stålmarck-Methode zur Formelüberprüfung vorgestellt und patentiert. Sie hat einige Verwendung in industriellen Anwendungen gefunden.

DPLL wurde für das automatische Theorembeweisen für Fragmente der Logik erster Ordnung durch den DPLL(T)-Algorithmus erweitert.

In den Jahren 2010 bis 2019 wurde an der Verbesserung des Algorithmus gearbeitet und bessere Strategien für die Auswahl der Verzweigungsliterale und neue Datenstrukturen gefunden, um den Algorithmus schneller zu machen, insbesondere den Teil der unit propagation. Die wichtigste Verbesserung war jedoch ein leistungsfähigerer Algorithmus, Conflict-Driven Clause Learning (CDCL), der ähnlich wie DPLL ist, aber nach dem Erreichen eines Konflikts die Ursachen (Zuweisungen an Variablen) des Konflikts „lernt“ und diese Informationen verwendet, um nicht-chronologisches Backtracking (auch bekannt als Backjumping) durchzuführen, um ein erneutes Erreichen desselben Konflikts zu vermeiden. Die meisten modernen SAT-Solver basieren auf dem CDCL-Framework (Stand 2019).

Weiterführende Literatur

• Malay Ganai, Aarti Gupta, Dr. Aarti Gupta: SAT-based scalable formal verification solutions. Springer, 2007, ISBN 978-0-387-69166-4, S. 23–32 (englisch). 
• Carla P. Gomes, Henry Kautz, Ashish Sabharwal, Bart Selman: Handbook of knowledge representation. Hrsg.: Frank Van Harmelen, Vladimir Lifschitz, Bruce Porter (= Foundations of Artificial Intelligence. Band 3). Elsevier, 2008, ISBN 978-0-444-52211-5, Satisfiability Solvers, S. 89–134, doi:10.1016/S1574-6526(07)03002-7 (englisch). 

Weblinks

Commons: DPLL-Algorithmus – Sammlung von Bildern, Videos und Audiodateien