Recognition and Exploitation of Gate Structure in SAT Solving

In der theoretischen Informatik ist das SAT-Problem der archetypische Vertreter der Klasse der NP-vollständigen Probleme, weshalb effizientes SAT-Solving im Allgemeinen als unmöglich angesehen wird.
Dennoch erzielt man in der Praxis oft erstaunliche Resultate, wo einige Anwendungen Probleme mit Millionen von Variablen erzeugen, die von neueren SAT-Solvern in angemessener Zeit gelöst werden können.
Der Erfolg von SAT-Solving in der Praxis ist auf aktuelle Implementierungen des Conflict Driven Clause-Learning (CDCL) Algorithmus zurückzuführen, dessen Leistungsfähigkeit weitgehend von den verwendeten Heuristiken abhängt, welche implizit die Struktur der in der industriellen Praxis erzeugten Instanzen ausnutzen. ... mehr

In dieser Arbeit stellen wir einen neuen generischen Algorithmus zur effizienten Erkennung der Gate-Struktur in CNF-Encodings von SAT Instanzen vor, und außerdem drei Ansätze, in denen wir diese Struktur explizit ausnutzen.
Unsere Beiträge umfassen auch die Implementierung dieser Ansätze in unserem SAT-Solver Candy und die Entwicklung eines Werkzeugs für die verteilte Verwaltung von Benchmark-Instanzen und deren Attribute, der Global Benchmark Database (GBD).

In theoretical computer science, the SAT problem is the archetypal representative of the class of NP-complete problems, and thus SAT solving is generally considered intractable.
However, exciting results can be found in practical SAT solving, where some applications generate problems with millions of variables, that can be solved in a reasonable time by recent solvers.
The success of practical SAT solving is due to state-of-the-art implementations of the Conflict Driven Clause-Learning (CDCL) algorithm, whose performance largely depends on the employed heuristics which implicitly exploit the structure of the instances generated in industrial practice. ... mehr

In this thesis, we present a new generic algorithm to efficiently recognize gate structure in CNF encodings and three approaches in which we explicitly exploit that structure.
Our contributions also include the implementation of these approaches in the new SAT solver Candy and the development of a tool for distributed management of benchmark instances and their attributes, the Global Benchmark Database (GBD).