Diploma Thesis DIP-3094

BibliographyThomaß, Bertram: SAT solving modulo nichtlinearer Theorien.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Diploma Thesis No. 3094 (2010).
76 pages, german.
CR-SchemaD.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
Abstract

Diplomarbeit: SAT solving modulo nichtlinearer Theorien

Um komplexe Kombinationen von booleschen Ausdrücken und (nicht-)linearen arithmetischen Theorien auf eine erfüllende Belegung zu untersuchen, wurde in dieser Arbeit ein Satisfiability Modulo Theories (SMT) Solver entwickelt, der im Gegensatz zum lazy SMT Ansatz eine enge Integration von SAT- und Theorie-Solver realisiert. Durch die enge Integration von Davis-Putnam-Logemann-Loveland (DPLL) Algorithmus und Interval Constraint Propagation (ICP) lassen sich alle Optimierungen vom DPLL-Algorithmus auf ICP übertragen. Eine Besonderheit bietet die Behandlung der Division, da zwei disjunkte unendliche Resultatsintervalle bei der Division durch ein Intervall entstehen, das eine enthält. Der SMT-Solver bietet viele moderne Features, wie nicht-chronologisches Backtracking, Watched Literals, Lernen von Konfliktklauseln, Neustarts und Parallelisierung. Außerdem wird eine neue Entscheidungsheuristik für den SMT-Solver vorgestellt.

Full text and
other links
PDF (1082106 Bytes)
Access to students' publications restricted to the faculty due to current privacy regulations
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Software Reliability and Security
Superviser(s)Nowotka, Dirk
Entry dateJanuary 28, 2011
   Publ. Computer Science