Bibliography | Thomaß, 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-Schema | D.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 date | January 28, 2011 |
---|