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 | 07.10 & 12.10 | SAT basics | ||
| 02 | 19.10 | Conflict Graphs, NP completeness | ||
| 03 | 21.10 & 28.10 | NP completeness of Shakashaka, MaxSAT | ||
| 04 | 04.11 & 09.11 | FO-Theories, SMT, DPLL(T) | ||
| 05 | 11.11 & 16.11 | Equality Logic, EUF | ||
| 06 | 18.11 & 23.11 | Difference Logic, Simplex | ||
| 07 | 25.11 & 30.11 | Farkas' Lemma, Complexity and Incrementality of Simplex | ||
| 08 | 02.12 & 07.12 | Branch-and-Bound, Small Model Property of LIA | ||
| 09 | 09.12 & 14.12 | Bit-Vector Arithmetic | ||
| 10 | 16.12 & 11.01 | Nelson-Oppen, QBF, PSPACE completeness | ||
| 11 | 13.01 & 18.01 | Ferrante-Rackoff, Cooper's Method | ||
| 12 | 20.01 & 25.02 | Arrays | ||
| 13 | 27.01 & 01.02 | Q&A, Repeat for exam | ||
| 14 | 03.02 | 1st exam |
Exam
The first exam (solution) was conducted on February 3. It was a closed book exam. There also has been a test exam.A second or third exam can be conducted on request.
Further Material
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. Recordings of the lectures (if lectures turn virtual) will be available from the OLAT course of the lecture. Solutions to exercises will be made available via the OLAT course of the proseminar.