Begriff
DPLL Algorithm
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Wie löst man ein Sudoku? Man sucht ein Feld, wo nur eine Zahl passt ("Unit Propagation"). Wenn keins da ist, rät man ("Probieren wir mal 5"). Wenn es nicht aufgeht, geht man zurück (Backtracking) und probiert eine andere Zahl. Genau das ist DPLL (Davis-Putnam-Logemann-Loveland). Der Ur-Großvater aller SAT-Solver (1962). Er ist ein intelligentes Backtracking-Verfahren für Logik-Formeln.
Merksatz: Ein vollständiger, Backtracking-basierter Algorithmus zur Entscheidung der Erfüllbarkeit von aussagenlogischen Formeln in konjunktiver Normalform (CNF), der Unit Propagation und Pure Literal Elimination nutzt.
Du implementierst ihn selten selbst (nutze MiniSat). Aber das Prinzip (Recursive Search + Pruning) ist überall in der KI. Constraint Satisfaction Problems (CSP) funktionieren ähnlich.
1. Unit Propagation
Die Superkraft.
Regel: A oder B.
Wir wissen: B ist Falsch.
Schlussfolgerung: A MUSS Wahr sein.
Das reduziert den Suchraum dramatisch. DPLL macht das so lange, bis nichts mehr geht ("Fixpunkt"), dann erst rät er.
2. Pure Literal Elimination
Wenn Variable x in der ganzen Formel immer nur positiv vorkommt (nie als NOT x).
Dann können wir x = True setzen. Das kann nichts kaputt machen.
(Wird in modernen Solvern oft weggelassen, weil zu teuer zu prüfen).
1. Von DPLL zu CDCL
Moderne SAT-Solver nutzen nicht mehr das reine DPLL, sondern CDCL (Conflict-Driven Clause Learning). Der Kern-Unterschied: Wenn DPLL in eine Sackgasse (Konflikt) gerät, springt es eine Ebene zurück und probiert weiter. CDCL hingegen analysiert den Konflikt: "Warum genau hat es nicht geklappt?". Es leitet eine neue Regel (eine Learned Clause) ab, die diesen spezifischen Fehler für die Zukunft ausschließt. Dadurch "lernt" der Algorithmus während der Suche die Struktur des Problems. Ohne dieses Lernen wäre die formale Verifikation von Mikroprozessoren heute unmöglich.
2. Zwei Beobachtete Literale (2-Watched Literals)
Wie prüft man effizient, ob eine Regel wie (A v B v C v D) durch Unit Propagation feuern muss?
Nativ müsste man bei jeder Änderung von A, B, C oder D die ganze Regel scannen.
Der Watched Literals Trick: Man beobachtet in jeder Regel nur zwei Variablen. Solange beide noch nicht "Falsch" sind, kann die Regel unmöglich feuern.
Erst wenn eine der beiden beobachteten Variablen auf "Falsch" gesetzt wird, sucht der Solver nach einer neuen Variable zum Beobachten. Das reduziert den Rechenaufwand pro Schritt von $O(N)$ auf fast $O(1)$, was bei Millionen von Regeln den entscheidenden Geschwindigkeitsvorteil bringt.
3. VSIDS Heuristik
Beim "Raten" (Decision) nutzt DPLL oft einfache Strategien. Hochleistungs-Solver nutzen VSIDS (Variable State Independent Decaying Sum). Dabei bekommt jede Variable einen Zähler, der erhöht wird, wenn die Variable an einem Konflikt beteiligt ist. Der Clou: Die Zähler werden über Zeit langsam kleiner (Decay). Dadurch bevorzugt der Solver Variablen, die in der jüngsten Vergangenheit zu Problemen geführt haben. Der Algorithmus fokussiert sich also automatisch auf die "schweren" Stellen des Puzzles, anstatt Zeit in irrelevanten Bereichen zu verschwenden.
Quick-Check
Unterschied zu CDCL?
DPLL ist "klassisches Backtracking" (Vergesslich). CDCL ist "DPLL mit Gedächtnis" (Conflict Learning). CDCL ist auf großen Problemen millionenfach schneller.Komplexität?
Im Worst Case immer noch exponentiell ($2^N$). Aber im Average Case viel besser.Namen?
Es gab erst DP (Davis-Putnam, basierend auf Resolution, 1960) -> brauchte zu viel Speicher. Dann DLL (Davis-Logemann-Loveland, 1962) -> basierend auf Suche. Wir nennen es heute DPLL.