Norbert Manthey

Towards Next Generation Sequential and Parallel SAT Solvers

Dokumente und Dateien

Hinweis

Bitte nutzen Sie beim Zitieren immer folgende Url:

http://nbn-resolving.de/urn:nbn:de:bsz:14-qucosa-158672

Kurzfassung in Englisch

This thesis focuses on improving the SAT solving technology. The improvements focus on two major subjects: sequential SAT solving and parallel SAT solving.

To better understand sequential SAT algorithms, the abstract reduction system Generic CDCL is introduced. With Generic CDCL, the soundness of solving techniques can be modeled. Next, the conflict driven clause learning algorithm is extended with the three techniques local look-ahead, local probing and all UIP learning that allow more global reasoning during search. These techniques improve the performance of the sequential SAT solver Riss. Then, the formula simplification techniques bounded variable addition, covered literal elimination and an advanced cardinality constraint extraction are introduced. By using these techniques, the reasoning of the overall SAT solving tool chain becomes stronger than plain resolution. When using these three techniques in the formula simplification tool Coprocessor before using Riss to solve a formula, the performance can be improved further.

Due to the increasing number of cores in CPUs, the scalable parallel SAT solving approach iterative partitioning has been implemented in Pcasso for the multi-core architecture. Related work on parallel SAT solving has been studied to extract main ideas that can improve Pcasso. Besides parallel formula simplification with bounded variable elimination, the major extension is the extended clause sharing level based clause tagging, which builds the basis for conflict driven node killing. The latter allows to better identify unsatisfiable search space partitions. Another improvement is to combine scattering and look-ahead as a superior search space partitioning function. In combination with Coprocessor, the introduced extensions increase the performance of the parallel solver Pcasso. The implemented system turns out to be scalable for the multi-core architecture. Hence iterative partitioning is interesting for future parallel SAT solvers.

The implemented solvers participated in international SAT competitions. In 2013 and 2014 Pcasso showed a good performance. Riss in combination with Copro- cessor won several first, second and third prices, including two Kurt-Gödel-Medals. Hence, the introduced algorithms improved modern SAT solving technology.

weitere Metadaten

übersetzter Titel
(Deutsch)
Hin zur nächsten Generation Sequentieller und Paralleler SAT-Solver
Schlagwörter
(Deutsch)
Künstliche Intelligenz, Automatisches Schließen, Suche, Aussagenlogik, Erfüllbarkeitsproblem, Paralleles Rechnen, Formelvereinfachung, Reduktionssystem
Schlagwörter
(Englisch)
Artificial Intelligence, Automated Reasoning, Search, Propositional Logic, Satisfiability Testing, Parallel Computing, Constraint Programming, Formula Simplification, Pseudo Boolean, Reduction System
SWD SchlagworteErfüllbarkeitsproblem, Künstliche Intelligenz, Suche, Aussagenlogik, Reduktionssystem
DDC Klassifikation004
RVK KlassifikationST 300
Institution(en) 
HochschuleTechnische Universität Dresden
FakultätFakultät Informatik
ProfessurProfessur für Wissensverarbeitung
GutachterProf. Dr. habil. Steffen Hölldobler
Prof. Dr. Armin Biere
DokumententypDissertation
SpracheEnglisch
Tag d. Einreichung (bei der Fakultät)13.10.2014
Tag d. Verteidigung / Kolloquiums / Prüfung01.12.2014
Veröffentlichungsdatum (online)08.01.2015
persistente URNurn:nbn:de:bsz:14-qucosa-158672

Hinweis zum Urheberrecht

Diese Website ist eine Installation von Qucosa - Quality Content of Saxony!
Sächsische Landesbibliothek Staats- und Universitätsbibliothek Dresden