en | de

Constraint Solving

master program

VO2 + PS2  WS 2021/2022  703304 + 703305


Content

The elective module Constraint Solving provides an introduction into the theory and practice of constraint solving. The following topics will be discussed:


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 pdf pdf
02 21.10 & 28.10 Clingo and ASP pdf pdf
03 22.10 & 04.11 NP completeness, Unsat Cores pdf pdf
04 29.10 Models, MaxSAT pdf
05 05.11 & 11.11 FO-Theories, SMT pdf pdf
06 12.11 & 18.11 DPLL(T), EUF pdf pdf
07 19.11 & 25.11 Nelson-Oppen, QBF pdf pdf
08 26.11 & 02.12 PSPACE completeness of QBF, Cooper's Method pdf (x1, x4) pdf
09 03.12 & 09.12 Ferrante-Rackoff, Simplex pdf (x1, x4) pdf
10 10.12 & 16.12 Complexity and Incrementality of Simplex pdf (x1, x4) pdf
11 17.12 & 13.01 Branch-and-Bound, Small Model Property of LIA pdf (x1, x4) pdf
12 14.01 & 20.01 Gomory Cuts, Difference Logic pdf (x1, x4) pdf
13 21.01 & 27.02 Arrays pdf (x1, x4) pdf
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: Slides and exercises are available from this page.