Parallel SAT

Das aussagenlogische Erfüllbarkeitsproblem (SAT) ist eines der am
besten untersuchten Probleme der Klasse NP. In den letzten 20 Jahren
sind SAT-Solver so leistungsfähig geworden, dass sie in vielen
Bereichen (u.a. Verifikation, Scheduling, Model Checking) angewandt
werden. Diese Leistungssteigerung beruht auf signifikanten
Fortschritten im Bereich der Kalküle, der Algorithmen und
Datenstrukturen, der Strategien und Heuristiken, der
Parametersteuerung sowie insbesondere auch auf der Anpassung der
SAT-Solver an bestehende sequentielle Architekturen.

Neue Architekturen sind jedoch parallel, verfügen über mehrere
Rechenkerne sowie häufig auch über Vektor- und SIMD-Einheiten. Um
moderne und zukünftige Rechnerarchitekturen nutzen zu können, müssen
sequentielle Algorithmen parallelisiert und an die neuen Architekturen
angepasst werden.

Die Entwicklung eines parallelen SAT-Solvers mit akzeptabler
paralleler Effizienz für eine grosse Menge von SAT-Instanzen, die
aus unterschiedlichen Anwendungen kommen, ist eine besondere
Herausforderung und das Ziel dieses Projekts.

Heutige parallele SAT-Solver beruhen meist auf einem Portfolio-Ansatz,
bei dem mehrere, unterschiedlich konfigurierte, sequentielle Solver
jeweils die gleiche SAT-Instanz lösen. Eine echte Parallelisierung der
Suche erfolgt in der Regel nicht.  Dagegen teilen Partitions-Ansätze
den Suchraum auf, wobei bei einem iterativen Partitionen-Solver (im
Gegensatz zu flachen Partitionen-Solvern) neben den Unterräumen auch
immer parallel eine gegebenen SAT-Instanz von einem sequentiellen
Solver gelöst wird. Allen parallelen Ansätzen ist gemein, dass sie
auf den einzelnen Kernen sequentielle Solver einsetzen ohne deren
Implementierung und Datenstrukturen an die Mehrkernarchitekturen
anzupassen, unerfüllbare SAT-Instanzen nur schlecht lösen,
Vereinfachungstechniken nicht parallelisieren und nicht systematisch
evaluiert wurden. Auch ist das Verhalten paralleler Solver formal
unzureichend beschrieben.

Ausgehend von der Hypothese, dass iterative Partitionen-Solver bei
ansteigender Anzahl von Kernen in einer Mehrkernarchitektur
leistungs-, wettbewerbs- und zukunftsfähiger sind als Portfolio- oder
flache Partitionen-Solver, verfolgt dieses Projekt die folgenden
Ziele: Entwicklung eines skalierbaren, pararallen, iterativen
Partitionen-Solvers; Entwicklung und Integration spezieller Verfahren,
um unerfüllbare SAT-Instanzen schneller entscheiden und Beweise
ausgeben zu können; Verbesserung der Ressourcenausnutzung durch
Optimierung von Algorithmen, die spezielle Eigenschaften der zugrunde
liegenden Architektur ausnutzen; Entwicklung und Integration von
parallelen Vereinfachungstechniken; Entwicklung einer Beweistheorie,
die das Verhalten des Solvers adäquat beschreibt; sowie die
Konfiguration und Evaluation des Solvers. Der zu entwickelnde
parallele Solver soll aktuell eingesetzte sequentielle Solver
in allen gebräuchlichen Anwendungen ersetzen.