Advanced Methods for SAT Solving

DSpace Repositorium (Manakin basiert)

Zur Kurzanzeige

dc.contributor.advisor Kaufmann, Michael (Prof. Dr.) de_DE
dc.contributor.author Kottler, Stephan de_DE
dc.date.accessioned 2013-06-05 de_DE
dc.date.accessioned 2014-03-18T10:26:51Z
dc.date.available 2013-06-05 de_DE
dc.date.available 2014-03-18T10:26:51Z
dc.date.issued 2012 de_DE
dc.identifier.other 383201411 de_DE
dc.identifier.uri http://nbn-resolving.de/urn:nbn:de:bsz:21-opus-68475 de_DE
dc.identifier.uri http://hdl.handle.net/10900/49884
dc.description.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. en
dc.description.abstract 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. de_DE
dc.language.iso en de_DE
dc.publisher Universität Tübingen de_DE
dc.rights ubt-podok de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=de de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=en en
dc.subject.classification Erfüllbarkeitsproblem , Sat de_DE
dc.subject.ddc 004 de_DE
dc.subject.other Algorithm Engineering , CDCL , DMRP , BCP , Asymmetric Branching en
dc.title Advanced Methods for SAT Solving en
dc.title Alternative Ansätze für das Lösen von SAT Instanzen de_DE
dc.type PhDThesis de_DE
dcterms.dateAccepted 2013-05-08 de_DE
utue.publikation.fachbereich Informatik de_DE
utue.publikation.fakultaet 7 Mathematisch-Naturwissenschaftliche Fakultät de_DE
dcterms.DCMIType Text de_DE
utue.publikation.typ doctoralThesis de_DE
utue.opus.id 6847 de_DE
thesis.grantor 7 Mathematisch-Naturwissenschaftliche Fakultät de_DE

Dateien:

Das Dokument erscheint in:

Zur Kurzanzeige