Ein SAT-Lösungsmechanismus, der Konflikte während der Suche analysiert, um neue Klauseln (gelernten Klauseln) abzuleiten und zu speichern, die denselben Konflikt auf späteren Suchzweigen verhindern, typischerweise kombiniert mit nicht-chronologischem Backtracking.

Prinzip

Bei Auftreten eines Konflikts konstruiere man aus den jüngsten Zuweisungen einen Implikationsgraphen, identifiziere einen Schnitt oder Unique Implication Point (UIP), leite eine Klausel ab, die den Konflikt blockiert (logische Konsequenz der Klauselmenge), füge sie zur Datenbank hinzu und springe auf eine frühere Entscheidungsstufe zurück.

Demonstration

Während der Suche führt Unit-Propagation zu einem Klauselkonflikt. Baue den Implikationsgraphen der zugewiesenen Literale, finde den ersten UIP, resolviere Klauseln entlang des Schnitts, um eine gelernte Klausel ¬a ∨ ¬b zu erzeugen, die die Wiederholung derselben konfliktträchtigen Kombination verhindert, und springe dann zurück auf die Entscheidungsstufe, bei der diese Klausel unitär wird.

Fehlanwendung

Klauseln aufzuzeichnen, die keine logischen Konsequenzen sind (fehlerhafte Ableitung), zu spezifische oder trivial subsumierte Klauseln zu lernen ohne Löschpolitik, oder gelernte Klauseln wie bloße Heuristiken zu behandeln ohne Gewährleistung der Korrektheit untergräbt Korrektheit oder Leistung des Solvers.

Konsequenz

CDCL verhindert wiederholtes Durchlaufen gleicher Konfliktmuster, ermöglicht mächtiges nicht-chronologisches Backtracking und ist ein Hauptgrund für die drastischen praktischen Beschleunigungen moderner SAT-Solver bei vielen Problemklassen.

Umkehrung

Reines DPLL ohne Klausellernen entdeckt Konflikte wiederholt neu und ist typischerweise deutlich weniger effizient; lokale Suchmethoden verzichten ebenfalls auf Lernen und zeigen ein anderes Leistungsverhalten.

Abgrenzung

Gilt für klauselbasierte propositionale Lösung und für Erweiterungen mit Theoriebegründung bei sorgfältiger Integration; es erfordert korrekte Konfliktanalyse und Management der Learned-Clause-Datenbank (Garbage-Collection, Subsumption), um effektiv zu bleiben.

Semantische Spannung

CDCL balanciert zwischen zu vielen gelernten Klauseln (Speicher-/Zeitexplosion) und zu wenigen (ineffektives Pruning); es bewegt sich zwischen rein auf Resolution basierenden Beweissystemen und heuristischer Suche und verbindet Deduktion mit Suchsteuerung.

Synthese

Konfliktgesteuertes Klausel-Lernen ist der Prozess, Konflikte mittels Implikationsgraphen zu analysieren, daraus korrekte gelernte Klauseln zu extrahieren und Backjumping durchzuführen, wodurch eine dynamische Klauseldatenbank entsteht, die die künftige Suche eindämmt und moderne SAT-Lösungsverfahren antreibt.