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)
All material (slides, homework sheets, solutions, lecture recordings) are available on the OLAT sites of the lecture and proseminar.
| week | date | topics |
|---|---|---|
| 01 | 04.03 & 10.03 | SAT basics |
| 02 | 11.03 & 17.03 | Conflict Graphs, NP completeness |
| 03 | 18.03 & 24.03 | NP completeness of Shakashaka, MaxSAT |
| 04 | 25.03 & 14.04 | FO-Theories, SMT, DPLL(T) |
| 05 | 15.04 & 21.04 | Equality Logic, EUF |
| 06 | 22.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 & 09.06 | Ferrante-Rackoff, Cooper's Method |
| 13 | 10.06 & 16.06 | Arrays |
| 14 | 17.06 | Q&A, Repeat for exam |
| 15 | 24.06 | 1st exam |
Exam
The first exam will be on June 24. It will be closed book.You can find old exams on this website of a previous iteration of this course.
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