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 | pdf (x1, x4) | |
| 02 | 19.10 | Conflict Graphs, NP completeness | pdf (x1, x4) | |
| 03 | 21.10 & 28.10 | NP completeness of Shakashaka, MaxSAT | pdf (x1, x4) | |
| 04 | 04.11 & 09.11 | FO-Theories, SMT, DPLL(T) | pdf (x1, x4) | |
| 05 | 11.11 & 16.11 | Equality Logic, EUF | pdf (x1, x4) | |
| 06 | 18.11 & 23.11 | Difference Logic, Simplex | pdf (x1, x4) | |
| 07 | 25.11 & 30.11 | Farkas' Lemma, Complexity and Incrementality of Simplex | pdf (x1, x4) | |
| 08 | 02.12 & 07.12 | Branch-and-Bound, Small Model Property of LIA | pdf (x1, x4) | |
| 09 | 09.12 & 14.12 | Bit-Vector Arithmetic | pdf (x1, x4) | |
| 10 | 16.12 & 11.01 | Nelson-Oppen, QBF, PSPACE completeness | pdf (x1, x4) | |
| 11 | 13.01 & 18.01 | Ferrante-Rackoff, Cooper's Method | pdf (x1, x4) | |
| 12 | 20.01 & 25.02 | Arrays | pdf (x1, x4) | |
| 13 | 27.01 & 01.02 | Q&A, Repeat for exam | ||
| 14 | 03.02 | 1st exam |
Exam
The first exam will be conducted on February 3. One has to register for the exam until February 1. The exam will be a closed book exam in lecture hall SR 12 during the usual time of the lecture. To get an idea of the style of the exam, you can have a look at a test exam. It consists of a collection of earlier exam exercises and can be discussed in week 13 (lecture and / or proseminar).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.