Slides Additional Material 1 Propositional Logic (propositional_logic_primer.ppt) propositional_logic.pdf (2x3) propositional-sat.ppt propositional-bdds.ppt Paper on MiniSat MiniSat SAT-Race 2006 Bryant's paper on BDDs CUDD (Documentation) 2 First-order theories First-order theories primer.ppt 3 Equalities and Uninterpreted Functions uf.pdf (2x3) 4 Decision Procedures for Equality Logic and Uninterpreted Functions equality-intro.ppt equality-transitivity-constraints.ppt equality-range-allocation.ppt equality-e-graphs.ppt 5 Linear Arithmetic linear-simplex.ppt linear-fourier_motzkin.pdf (2x3) linear-branch-and-bound.ppt linear-omega.pdf (2x3) Dutertre, de Moura: A Fast Linear-Arithmetic Solver for DPLL(T) Pugh: The Omega test 6 Bit Vectors bit-vectors.pdf (2x3) 7 Arrays Bradley, Manna, Sipma: What's Decidable About Arrays? 8 Pointer Logic 9 Quantified Formulas quantification.ppt 10 Deciding a Combination of Theories combination.ppt 11 Propositional Encodings and the DPLL(T) framework encodings.pdf A The SMT-LIB Initiative B A C++ Library for Developing Decision Procedures We are happy to provide the Latex-Sources of the .PDF-slides.