### 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