Skalierbare parallele Verfahren zur Boolean Constraint Propagation auf Multicore-Architekturen

Abstract

Beim SAT-Solving werden boolesche Formeln auf Erfüllbarkeit überprüft. Seit den frühen 1990ern gewann das SAT-Solving für Industrie und Forschung stetig an Bedeutung, da sich viele Probleme der Hard- und Softwareentwicklung auf das Erfüllbarkeitsproblem reduzieren lassen. Ein Großteil der Laufzeit eines SAT-Solvers (ca. 80%-90%) entfällt auf die Unit-Propagation. Unit-Propagation ist die iterative Anwendung von Implikationen, die aufgrund der Formel und der aktuellen Belegung gelten. Um Beschleunigungen des Solving-Prozesses zu erzielen, werden in dieser Arbeit verschiedene Parallelisierungsansätze der Unit-Propagation untersucht. Da moderne Prozessoren mit immer mehr Rechenkernen ausgestattet sind, werden Parallelisierungsansätze entwickelt, die auf Mehrkernarchitekturen basieren. In der vorliegenden Arbeit werden zunächst die von aktuellen SAT-Solvern verwendeten Algorithmen und Implementierungstechniken vorgestellt. Insbesondere wird der DPLL-Algorithmus und dessen Erweiterung um Klausellernen (CDCL-Solver) präsentiert. Danach wird mit dem Two-Watched-Literal Schema ein effizientes Verfahren zur Unit-Propagation beschrieben. Im nächsten Schritt wird untersucht, welche Teile der Unit-Propagation sich besonders für eine Parallelisierung eignen und welche Probleme dabei zu lösen sind. Darauf aufbauend wird ein sperrbasierter und ein sperrfreier Lösungsansatz sowie parametrisierbare Alternativen davon entwickelt. Die Algorithmen werden anschließend in Minisat - einem minimalistischen klausellernenden SAT-Solver - implementiert. Nach Auswahl eines geeigneten Formelsatzes werden die Algorithmen evaluiert. Dazu wird der Formelsatz für jeden Algorithmus mehrfach ausgeführt und Parallelisierungskennzahlen (Beschleunigung, parallele Effizienz) ermittelt. Abschließend werden die Ergebnisse beider Ansätze miteinander verglichen und bewertet.