en | de

Constraint Solving

master program

VO2 + PS2  WS 2022/2023  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 07.10 & 12.10 SAT basics pdf (x1, x4) pdf
02 19.10 Conflict Graphs, NP completeness pdf (x1, x4)
03 21.10 & 28.10 NP completeness of Shakashaka, MaxSAT pdf (x1, x4) pdf
04 04.11 & 09.11 FO-Theories, SMT, DPLL(T) pdf (x1, x4) pdf
05 11.11 & 16.11 Equality Logic, EUF pdf (x1, x4) pdf
06 18.11 & 23.11 Difference Logic, Simplex pdf (x1, x4) pdf
07 25.11 & 30.11 Farkas' Lemma, Complexity and Incrementality of Simplex pdf (x1, x4) pdf
08 02.12 & 07.12 Branch-and-Bound, Small Model Property of LIA pdf (x1, x4) pdf
09 09.12 & 14.12 Bit-Vector Arithmetic
10 16.12 & 11.01 Nelson-Oppen, QBF, PSPACE completeness
11 13.01 & 18.01 Ferrante-Rackoff, Cooper's Method
12 20.01 & 25.02 Arrays
13 27.01 & 01.02 Q&A, Repeat for exam
14 03.02 1st exam

Further Material

Literature

The course is partly based on the following books:

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.