DPLL

Der DPLL-Algorithmus ist ein rekursiver Algorithmus zur Entscheidung der Erfüllbarkeit von Formeln in KNF.

Darstellung einer Formel

Eine Formel

wird als Klauselmenge

repräsentiert.

Basis-Algorithmus:

DPLL($\Phi ,\beta$)

Eingabe

• Klauselmenge $\mathrm{\Phi }$
• partielle Belegung $\beta$ mit$$\mathrm{def}(\beta )\subseteq \mathrm{var}(\mathrm{\Phi })$$

Ausgabe

• eine erweiterte Belegung ${\beta }^{\prime }\supseteq \beta$ mit$${\beta }^{\prime }\models \mathrm{\Phi }$$oder
• "unerfüllbar"

Algorithmus

1. Fall 1: $[[\mathrm{\Phi }]{]}^{\beta }=1$
   → gib $\beta$ zurück.

2. Fall 2: $[[\mathrm{\Phi }]{]}^{\beta }=0$
   → gib "unerfüllbar" zurück.

3. Fall 3: $[[\mathrm{\Phi }]{]}^{\beta }$ ist unbestimmt
   Führe nacheinander aus:

   1. (a) reduce(β, Φ)
      Reduziert die Klauselmenge, meist durch Unit Clause Propagation.
   2. (b) branch(β)
      Wähle eine unbelegte Variable $X\in var(\mathrm{\Phi })$ und einen Wahrheitswert $t\in \{0,1\}$.

   Rekursion:

   $${\beta }^{\prime }:=\mathrm{DPLL}(\mathrm{\Phi },\beta [X\mapsto t])$$
   • Wenn ${\beta }^{\prime }\ne$ unerfüllbar → gib ${\beta }^{\prime }$ zurück
   • sonst$$\mathrm{return}\mathrm{DPLL}(\mathrm{\Phi },\beta [X\mapsto 1-t])$$

Hilfsfunktion: reduce(β, Φ)

Dient der Reduktion der Formel nach jedem Schritt.

Unit Clause Propagation (Einer-Klauseln):

Enthält $\mathrm{\Phi }$ eine Klausel

in der alle bis auf ein Literal bereits durch $\beta$ belegt sind,
dann muss jede erfüllende Belegung das letzte Literal $L_i$ wahr machen.

• Falls $L_i=X$, füge $[X\mapsto 1]$ zu $\beta$ hinzu.
• Falls $L_i=\mathrm{\neg }X$, füge $[X\mapsto 0]$ zu $\beta$ hinzu.

Wiederhole, bis es keine Einer-Klauseln mehr gibt.

Hilfsfunktion: branch(β)

Wählt eine unbelegte Variable zur Fallunterscheidung.

Typische Heuristiken:

• DLIS (dynamic largest individual sum):
  Wähle Literal $L$, das am häufigsten vorkommt; setze es auf 1.
• DLCS (dynamic largest combined sum):
  Wähle Variable, die (positiv+negativ) am häufigsten vorkommt.
• MOM (maximal occurrence in minimal clauses):
  Wähle Variable, die am häufigsten in den kürzesten Klauseln vorkommt.

DPLL Optimierungen

1. Auswahlregeln (Heuristiken): Welches Literal wird beim Branching gewählt? (z.B. MOM, DLIS).
2. Conflict Analysis: Bei einer Sackgasse (Konflikt) wird analysiert, warum der Konflikt auftrat, um intelligenter zurückzuspringen (Non-chronological Backtracking).
3. Clause Learning (CDCL): Aus der Konfliktanalyse werden neue Klauseln gelernt und zur Formel hinzugefügt, um denselben Fehler in Zukunft zu vermeiden.
4. Random Restarts: Der Solver wird neu gestartet (unter Beibehaltung gelernter Klauseln), um nicht in lokalen Minima festzustecken.