Advanced Methods for SAT Solving

Abstract

This thesis explores SAT solving techniques that go beyond small changes to the predominant conflict-driven SAT solving approach with clause learning (CDCL). Whilst this work starts with techniques that are close to state-of-the-art CDCL solving, it goes further, and explores and evaluates some rather uncommon ideas. The general purpose is to widen the range of instances for which SAT solvers may compute a result in reasonable time.

We first present some extensions that can be incorporated into CDCL solvers. We introduce a novel improvement of the data structure to represent clauses within a CDCL solver. Moreover, we study the enhancement of simplification techniques for SAT formulae. The underlying techniques are asymmetric branching and hyper-binary resolution. We propose and evaluate an algorithm to improve the quality of both techniques.

A crucial part of conflict-driven SAT solving is the so-called Boolean constraint propagation (BCP) of assignments. Any clause that has only one literal left implies an assignment of the corresponding variable. We extend BCP to more general cases where any number of literals may be left. The technique is based on the general concept of hyper-resolution that was introduced by Robinson. Two different implementations are evaluated to study the tradeoff between speed and quality.

We further depart from the standard CDCL algorithm by exploring the alternative DMRP solving approach. Decision making with reference points (DMRP) was introduced by Goldberg. Compared to the CDCL algorithm the DMRP approach requires more information for SAT solving. Consequently, more effort has to be spent on maintaining the underlying data structures. We present an efficient implementation for the increased requirements of the DMRP algorithm. Moreover, we suggest a hybrid approach that is competitive to pure CDCL solving.

All the techniques and approaches presented in this thesis have been combined within one SAT solver. We present the implementation of our parallel solver, SArTagnan, with a high degree of information sharing among different threads. More complex techniques are justified by the benefits of having several solvers running in parallel.

In der Dissertation werden Ansätze zum Lösen von SAT Problemen präsentiert und evaluiert, die über die vorherrschende Technik des sogenannten CDCL Verfahrens (Conflict Driven Solving with Clause Learning) hinaus gehen. Dabei werden zunächst solche Ansätze betrachtet, die den CDCL Algorithmus leicht verändern oder erweitern. Es werden aber auch Techniken analysiert, die sich vom CDCL Verfahren grundlegend unterscheiden.

In der Arbeit wird eine Verbesserung der Datenstruktur zum Speichern von Klauseln vorgestellt, die in verschiedene Implementierungen des CDCL Algorithmus integriert werden kann. Darüber hinaus wird die Simplifizierung von SAT Instanzen analysiert, insbesondere die beiden Ansätze „Asymmetric Branching“ und „Hyper-Binary Resolution“. Es wird ein Algorithmus präsentiert und evaluiert, der beide Ansätze sinnvoll kombiniert.

Ein wesentlicher Bestandteil von erfolgreichen SAT Solvern ist die sogenannte Boolean Constraint Propagation (BCP): Führt eine partielle Belegung der Variablen dazu, dass eine Klausel nur noch ein freies Literal enthält, so wird die entsprechende Belegung einer weiteren Variable impliziert. In der Dissertation wird eine wesentliche Erweiterung dieses Vorgehens entwickelt, so dass weitere Belegungen von Variablen auch impliziert werden können, wenn eine Klausel mehr als nur ein freies Literal enthält. Dabei werden zwei Ansätze vorgeschlagen und deren Auswirkung auf Laufzeit und Qualität verglichen.

Ein alternativer Ansatz zum Lösen von SAT Problemen wurde von Goldberg erarbeitet. Der DMRP Algorithmus (Decision Making with Reference Points) benötigt während des Lösungsprozesses wesentlich mehr Informationen als das CDCL Verfahren. Dies führt zu einem erhöhten Verwaltungsaufwand für die zugrunde liegende Datenstruktur. In der Dissertation wird eine effiziente Datenstruktur und deren Implementierung vorgestellt, um den DMRP Algorithmus zu realisieren. Die praktische Evaluierung motiviert ein hybrides Verfahren, das sich mit gängigen CDCL Solvern messen kann.

Alle in der Dissertation vorgestellten Ansätze werden in einem parallelen SAT Solver „SarTagnan“ kombiniert. Daraus ergeben sich spezifische Anforderungen an die Implementierung, um einen möglichst hohen Grad an Parallelität erzielen zu können. Der erhöhte Rechenaufwand für komplexe alternative Ansätze wird dadurch gerechtfertigt und motiviert, dass diese Informationen sämtlichen parallel laufenden Prozessen zu Gute kommen.