KIT | KIT-Bibliothek | Impressum | Datenschutz

Recognition and Exploitation of Gate Structure in SAT Solving

Iser, Markus

Abstract:
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

Abstract (englisch):
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

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000118523
Veröffentlicht am 27.04.2020
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsdatum 27.04.2020
Sprache Englisch
Identifikator KITopen-ID: 1000118523
Verlag Karlsruhe
Umfang III, 78 S.
Abschlussart Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdatum 07.02.2020
Referent/Betreuer Prof. C. Sinz
Schlagwörter SAT Solving, Propositional Logic, Structure, Algorithms, NP Completeness
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page