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 pdf
03 22.10 & 04.11 NP completeness, Unsat Cores pdf pdf pdf
04 29.10 Models, MaxSAT pdf
05 05.11 & 11.11 FO-Theories, SMT pdf pdf pdf
06 12.11 & 18.11 DPLL(T), EUF pdf pdf
07 19.11 & 25.11 Nelson-Oppen, QBF pdf 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

Literature

The course is partly based on the following books: Slides and exercises are available from this page.