Florian Leimgruber: BDD-unterstützes SAT-Solving

Es spricht Florian Leimgruber über:
BDD-unterstützes SAT-Solving

Abstract:
Binary Decision Diagrams (BDDs) sind eine Datenstruktur zur
Repräsentation Boolescher Funktionen, aus der sich viele
Eigenschaften der Funktion leicht ablesen lassen. Um die
Jahrtausendwende wurde die Effizienz von BDD basierten SAT-Solvern
untersucht. Mit der Einführung des CDCL Algorithmus 1996 im Solver
GRASP endeten diese Bemühungen größtenteils, da CDCL in der Praxis
besser Performance zeigte. Mittlerweile basieren die meisten modernen
SAT-Solver auf CDCL.

Meine Bachelorarbeit griff BDD-basierte Ansätze wieder auf und
untersuchte, wie hilfreich BDDs beim SAT-Solving sind. Es wurde dazu
ein parallelen SAT-Solver entwickelt, die mithilfe von BDDs einen CDCL
Solver unterstützen. Dabei werden BDD-Approximationsalgorithmen
eingesetzt um die BDD-Größen zu limitieren. Die BDDs werden
einerseits genutzt um lexikographische Suchraumeinschränkungen
herzuleiten. Andererseits wurde ein Algorithmus entwickelt, der aus
BDDs kleine Klauseln ableitet.

Der Vortrag erläutert die Theorie hinter BDDs und CDCL, bevor
erklärt wird, wie diese zu einem gemeinsam Solver kombiniert wurden.
Zudem wird darauf eingegangen, worauf bei einer effizienten
Implementierung geachtet werden muss. Zuletzt wird mit der
experimentellen Evaluation belegt, dass die Suche nach kleinen
Klauseln Vorteile bei ausgewählten kombinatorischen Problemen bringt.