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:

• propositional logic (SAT and Max-SAT)
• Boolean combination of constraints, satisfiability modulo theories (SMT)
• constraints about equality logic and uninterpreted functions (EUF)
• linear arithmetic constraints (LIA and LRA)
• constraints involving arrays
• constraints using quantifiers (QBF)

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 pdf (x1, x4) pdf
06 23.04 & 26.04 Difference Logic, Simplex pdf (x1, x4) pdf
07 30.04 & 03.05 Farkas' Lemma, Complexity and Incrementality of Simplex pdf (x1, x4) pdf
08 07.05 & 10.05 Branch-and-Bound, Small Model Property of LIA pdf (x1, x4) pdf
09 14.05 & 17.05 Cubes and Equalities in LIA pdf (x1, x4) pdf
10 21.05 & 24.05 Bit-Vector Arithmetic pdf (x1, x4) pdf
11 28.05 & 03.06(!) Nelson-Oppen, QBF, PSPACE completeness pdf (x1, x4) pdf
12 04.06 & 07.06 Ferrante-Rackoff, Cooper's Method pdf (x1, x4) pdf
13 11.06 & 14.06 Arrays pdf (x1, x4) pdf
14 18.06 & 21.06 Q&A, Repeat for exam
15 25.06 1st exam

### Exam

The first exam was offered on June 25. It is a closed book exam.
You can find old exams on this website of a previous iteration of this course. In particular, this test exam will be discussed in the PS on June 21.
A second exam is offered on July 24. A third exam can be offered on request after the second 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.