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:

• 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 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 pdf (x1, x4) pdf
10 16.12 & 11.01 Nelson-Oppen, QBF, PSPACE completeness pdf (x1, x4) pdf
11 13.01 & 18.01 Ferrante-Rackoff, Cooper's Method pdf (x1, x4) pdf
12 20.01 & 25.02 Arrays pdf (x1, x4) pdf
13 27.01 & 01.02 Q&A, Repeat for exam
14 03.02 1st exam

### Exam

The first exam will be conducted on February 3. One has to register for the exam until February 1. The exam will be a closed book exam in lecture hall SR 12 during the usual time of the lecture. To get an idea of the style of the exam, you can have a look at a test exam. It consists of a collection of earlier exam exercises and can be discussed in week 13 (lecture and / or proseminar).
A second or third exam can be conducted on request.

### 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.