Paralleles SAT-Solving

• Antragsteller: Professor Dr. Steffen Hölldobler
• Fachliche Zuordnung: Theoretische Informatik ; Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2014 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 259253065

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.

• DFG-Verfahren: Sachbeihilfen