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 | 04.03 & 10.03 | SAT basics | pdf (x1, x4) | |
| 02 | 11.03 & 17.03 | Conflict Graphs, NP completeness | pdf (x1, x4) | |
| 03 | 18.03 & 24.03 | NP completeness of Shakashaka, MaxSAT | pdf (x1, x4) | |
| 04 | 25.03 & 31.03 | FO-Theories, SMT, DPLL(T) | ||
| 05 | 01.04 & 07.04 | Equality Logic, EUF | ||
| 06 | 08.04 & 28.04 | Difference Logic, Simplex | ||
| 07 | 29.04 & 05.05 | Farkas' Lemma, Complexity and Incrementality of Simplex | ||
| 08 | 06.05 & 12.05 | Branch-and-Bound, Small Model Property of LIA | ||
| 09 | 13.05 & 19.05 | Cubes and Equalities in LIA | ||
| 10 | 20.05 & 26.05 | Bit-Vector Arithmetic | ||
| 11 | 27.05 & 02.06 | Nelson-Oppen, QBF, PSPACE completeness | ||
| 12 | 03.06 & 16.06 | Ferrante-Rackoff, Cooper's Method | ||
| 13 | 10.06 & 23.06 | Arrays | ||
| 14 | 17.06 | Q&A, Repeat for exam | ||
| 15 | 24.06 | 1st exam |
Exam
The first exam is offered on June 24. It is a closed book exam.You can find old exams on this website of a previous iteration of this course.
A second and third exam is offered offered on request after the first 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.