Content
The elective module Constraint Solving provides an introduction into the theory and practice of constraint solving. The following topics will be discussed:
- propositional logic (SAT and Max-SAT)
- Boolean combination of constraints, satisfiability modulo theories (SMT)
- constraints about equality logic and uninterpreted functions (EUF)
- linear arithmetic constraints (LIA and LRA)
- constraints involving arrays
- constraints using quantifiers (QBF)
| week | date | topics | slides | exercises |
|---|---|---|---|---|
| 01 | 05.03 & 08.03 | SAT basics | pdf (x1, x4) | |
| 02 | 12.03 & 15.03 | Conflict Graphs, NP completeness | pdf (x1, x4) | |
| 03 | 19.03 & 22.04 | NP completeness of Shakashaka, MaxSAT | pdf (x1, x4) | |
| 04 | 09.04 & 12.04 | FO-Theories, SMT, DPLL(T) | pdf (x1, x4) | |
| 05 | 16.04 & 19.04 | Equality Logic, EUF | pdf (x1, x4) | |
| 06 | 23.04 & 26.04 | Difference Logic, Simplex | pdf (x1, x4) | |
| 07 | 30.04 & 03.05 | Farkas' Lemma, Complexity and Incrementality of Simplex | pdf (x1, x4) | |
| 08 | 07.05 & 10.05 | Branch-and-Bound, Small Model Property of LIA | ||
| 09 | 14.05 & 17.05 | Cubes and Equalities in LIA | ||
| 10 | 21.05 & 24.05 | Bit-Vector Arithmetic | ||
| 11 | 28.05 & 03.06(!) | Nelson-Oppen, QBF, PSPACE completeness | ||
| 12 | 04.06 & 07.06 | Ferrante-Rackoff, Cooper's Method | ||
| 13 | 11.06 & 14.06 | Arrays | ||
| 14 | 18.06 & 21.06 | Q&A, Repeat for exam | ||
| 15 | 25.06 | 1st 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
Slides and exercises are available from this page. Solutions to exercises will be made available via OLAT.