SlidesAdditional 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)
miniBDD
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
The small model property: How small can it be?
Boolean satisfiability with transitivity constraints
5 Linear Arithmetic
linear-simplex.ppt
linear-fourier_motzkin.pdf (2x3)
linear-branch-and-bound.ppt
linear-gomory.pdf
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
arrays.pdf (2x3) Bradley, Manna, Sipma: What's Decidable About Arrays?
8 Pointer Logic
pointers.pdf (2x3)
9 Quantified Formulas
quantification.ppt
10 Deciding a Combination of Theories
combination.ppt A New Correctness Proof of the Nelson-Oppen Combination Procedure
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 and of the sample assignment sheets.