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.