Improving SAT Solvers Using State-of-the-Art Techniques

Master's thesis by Norbert Manthey

Supervisor Steffen Hölldobler
Wissensverarbeitung
15 Dezember 2010 – 15 Dezember 2010
Download

Viele Probleme lassen sich als Erfüllbarkeitsproblem (SAT) kodieren.

Innerhalb der letzten Jahre wurden dafür performante Solver entwickelt. Die Leistung von diesen SAT-Solvern übertrifft in vielen Fällen die Leistung der spezifischen Lösungsprogramme für die jeweiligen Probleme. Dadurch werden viele industrierelevante Anwendungen nach SAT kodiert und mit einem SATSolver gelöst. Dabei wächst die Größe der Probleme, wodurch die Anforderungen an SAT-Solver immer weiter steigen.
Um die Auswirkungen der letzten Entwicklung besser verstehen zu können, sollen in dieser Arbeit die einzelnen Techniken, welche in SAT-Solver Einzug erhielten, vorgestellt und analysiert werden. Durch diese Untersuchengen soll gezeigt werden, welche dieser Techniken zu dem Leistungssprung von SAT-Solvern innerhalb der letzten Jahre geführt haben. Durch die Kombination der besten Techniken soll ein SAT-Solver entstehen, der die Leistung eines state-of-the-art SAT-Solvers hat und auch für das Lösen industrieller Probleme geeignet ist. Die aktuellen Techniken sollen in einem kompontenbasierten SAT-Solver implementiert werden, um die Auswirkungen der einzelnen Veränderungen auf die Leistung des Solvers nachvollziehen zu können.
Schwerpunkte:

Analysieren der aktuellen Techniken in modernen SAT-Solvern
Implementieren der neuen Komponenten in einen SAT-Solver
Empirische Untersuchung der Auswirkungen der einzelnen Komponenten und deren Kombination