Content
The module Decision Procedures provides an introduction into the theory and practice of decision procedures. The following topics will be discussed:
- propositional logic (SAT, BDD)
- satisfiability modulo theories (SMT)
- equality logic and uninterpreted functions (EUF)
- linear arithmetic (LIA and LRA)
- bit vectors (BV) and floating points (FP)
- arrays (AX) and pointers
- quantified formulas (QBF)
Schedule
| week | date | topics | slides | exercises | solutions |
|---|---|---|---|---|---|
| 01 | 01.03 & 05.03 | propositional logic, Tseitin's transformation, DPLL | pdf (x1, x4) | ||
| 02 | 08.03 & 12.03 | NP-completeness, SAT reductions | pdf (x1, x4) | ||
| 03 | 15.03 & 19.03 | maxSAT, binary decision diagrams, ZDDs | pdf (x1, x4) | ||
| 04 | 22.03 & 26.03 | SMT, DPLL(T) | pdf (x1, x4) | ||
| 05 | 12.04 & 16.04 | equality logic, EUF | pdf (x1, x4) | ||
| 06 | 19.04 & 23.04 | bit-vector arithmetic | pdf (x1, x4) | ||
| 07 | 26.04 & 30.04 | Nelson-Oppen combination method, quantifier elimination, QBF | pdf (x1, x4) | ||
| 08 | 03.05 & 07.05 | PSPACE-completeness, Cooper's method | pdf (x1, x4) | ||
| 09 | 10.05 & 14.05 | Ferrante and Rackoff's method, cardinality constraints, BMC | pdf (x1, x4) | ||
| 10 | 17.05 & 21.05 | quantifier free linear arithmetic, simplex algorithm | pdf (x1, x4) | ||
| 11 | |||||
| 12 | 31.05 & 04.06 | branch and bound, small model property of LIA | pdf (x1, x4) | ||
| 13 | 07.06 & 11.06 | Gomory cuts, difference logic | pdf (x1, x4) | ||
| 14 | 14.06 & 18.06 | checking array bounds, array logic, array properties | pdf (x1, x4) | ||
| 15 | 21.06 & 25.06 | 1st exam (solutions) | |||
| 24.09 | 2nd exam |
Literature
The course is partly based on the following books:-
Daniel Kroenig and Ofer Strichman
Decision Procedures — An Algorithmic Point of View (second edition)
Springer, 2016 -
Aaron Bradley and Zohar Manna
The Calculus of Computation — Decision Procedures with Applications to Verification
Springer, 2007