en | de

# Decision Procedures (WM 5)

## master program

VO3 + PS2  SS 2021  703829 + 703830

### 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) pdf pdf
02 08.03 & 12.03 NP-completeness, SAT reductions pdf (x1, x4) pdf pdf
03 15.03 & 19.03 maxSAT, binary decision diagrams, ZDDs pdf (x1, x4) pdf pdf
04 22.03 & 26.03 SMT, DPLL(T) pdf (x1, x4) pdf pdf
05 12.04 & 16.04 equality logic, EUF pdf (x1, x4) pdf pdf
06 19.04 & 23.04 bit-vector arithmetic pdf (x1, x4) pdf pdf
07 26.04 & 30.04 Nelson-Oppen combination method, quantifier elimination, QBF pdf (x1, x4) pdf pdf
08 03.05 & 07.05 PSPACE-completeness, Cooper's method pdf (x1, x4) pdf pdf
09 10.05 & 14.05 Ferrante and Rackoff's method, cardinality constraints, BMC pdf (x1, x4) pdf pdf
10 17.05 & 21.05 quantifier free linear arithmetic, simplex algorithm pdf (x1, x4) pdf pdf
11 24.05 & 28.05 pdf pdf
12 31.05 & 04.06 branch and bound, small model property of LIA pdf (x1, x4) pdf pdf
13 07.06 & 11.06 Gomory cuts, difference logic pdf (x1, x4) pdf pdf
14 14.06 & 18.06 checking array bounds, array logic, array properties pdf (x1, x4) pdf pdf
15 21.06 & 25.06 1st exam (solutions) pdf pdf
24.09 2nd exam

### Literature

The course is partly based on the following books:
Slides, exercises and solutions are available from this page. Recordings of the lectures are available from OLAT.