en | de

# Constraint-Solving

## Masterstudium

VO2 + PS2  WS 2021/2022  703304 + 703305

### Inhalt

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), linear programming
• constraints involving arrays
• constraints using quantifiers (QBF)

### Zeitplan

Starting from week 8, the solutions to the exercises will be made available in OLAT.
Woche Datum Themen Folien Proseminar Musterlösungen
01 08.10 & 14.10 SAT basics pdf pdf
02 21.10 & 28.10 Clingo and ASP pdf pdf
03 22.10 & 04.11 NP completeness, Unsat Cores pdf pdf
04 29.10 Models, MaxSAT pdf
05 05.11 & 11.11 FO-Theories, SMT pdf pdf
06 12.11 & 18.11 DPLL(T), EUF pdf pdf
07 19.11 & 25.11 Nelson-Oppen, QBF 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

### Test Exam

Have a look at an earlier exam that gives you an idea about the potential content of an exam in this course. It can be discussed in the proseminar on February 3.

### Literatur

The course is partly based on the following books: