en | de

Constraint Solving

master program

VO2 + PS2  SS 2024  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:


week date topics slides exercises
01 05.03 & 08.03 SAT basics pdf (x1, x4) pdf
02 12.03 & 15.03 Conflict Graphs, NP completeness pdf (x1, x4) pdf
03 19.03 & 22.04 NP completeness of Shakashaka, MaxSAT pdf (x1, x4) pdf
04 09.04 & 12.04 FO-Theories, SMT, DPLL(T) pdf (x1, x4) pdf
05 16.04 & 19.04 Equality Logic, EUF
06 23.04 & 26.04 Difference Logic, Simplex
07 30.04 & 03.05 Farkas' Lemma, Complexity and Incrementality of Simplex
08 07.05 & 10.05 Branch-and-Bound, Small Model Property of LIA
09 14.05 & 17.05 Cubes and Equalities in LIA
10 21.05 & 24.05 Bit-Vector Arithmetic
11 28.05 & 03.06(!) Nelson-Oppen, QBF, PSPACE completeness
12 04.06 & 07.06 Ferrante-Rackoff, Cooper's Method
13 11.06 & 14.06 Arrays
14 18.06 & 21.06 Q&A, Repeat for exam
15 25.06 1st exam

Literature

The course is partly based on the following books:

Slides and exercises are available from this page. Solutions to exercises will be made available via OLAT.