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
02 19.10 Conflict Graphs, NP completeness
03 21.10 & 28.10 NP completeness of Shakashaka, MaxSAT
04 04.11 & 09.11 FO-Theories, SMT, DPLL(T)
05 11.11 & 16.11 Equality Logic, EUF
06 18.11 & 23.11 Difference Logic, Simplex
07 25.11 & 30.11 Farkas' Lemma, Complexity and Incrementality of Simplex
08 02.12 & 07.12 Branch-and-Bound, Small Model Property of LIA
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

Exam

The first exam (solution) was conducted on February 3. It was a closed book exam. There also has been a test exam (solution).
A second or third exam can be conducted on request.

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.