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), linear programming
- constraints involving arrays
- constraints using quantifiers (QBF)
Schedule
Starting from week 8, the solutions to the exercises will be made available in OLAT.| week | date | topics | slides | exercises | solutions |
|---|---|---|---|---|---|
| 01 | 08.10 & 14.10 | SAT basics | |||
| 02 | 21.10 & 28.10 | Clingo and ASP | |||
| 03 | 22.10 & 04.11 | NP completeness, Unsat Cores | |||
| 04 | 29.10 | Models, MaxSAT | |||
| 05 | 05.11 & 11.11 | FO-Theories, SMT | |||
| 06 | 12.11 & 18.11 | DPLL(T), EUF | |||
| 07 | 19.11 & 25.11 | Nelson-Oppen, QBF | |||
| 08 | 26.11 & 02.12 | PSPACE completeness of QBF, Cooper's Method | pdf (x1, x4) | ||
| 09 | 03.12 & 09.12 | Ferrante-Rackoff, Simplex | pdf (x1, x4) | ||
| 10 | 10.12 & 16.12 | Complexity and Incrementality of Simplex | pdf (x1, x4) | ||
| 11 | 17.12 & 13.01 | Branch-and-Bound, Small Model Property of LIA | pdf (x1, x4) | ||
| 12 | 14.01 & 20.01 | Gomory Cuts, Difference Logic | pdf (x1, x4) | ||
| 13 | 21.01 & 27.02 | Arrays | pdf (x1, x4) | ||
| 14 | 28.01 & 03.02 | Q&A, Repeat for exam | |||
| 15 | 04.02 | 1st exam |
Test Exam
Have a look at an earlier exam that gives you an idea about the potential content of an exam in this course. It can be discussed in the proseminar on February 3.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