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
02	12.03 & 15.03	Conflict Graphs, NP completeness
03	19.03 & 22.04	NP completeness of Shakashaka, MaxSAT
04	09.04 & 12.04	FO-Theories, SMT, DPLL(T)
05	16.04 & 19.04	Equality Logic, EUF
06	23.04 & 26.04	Difference Logic, Simplex
07	30.04 & 03.05	Farkas' Lemma, Complexity and Incrementality of Simplex
08	07.05 & 10.05	Branch-and-Bound, Small Model Property of LIA
09	14.05 & 17.05	Cubes and Equalities in LIA
10	21.05 & 24.05	Bit-Vector Arithmetic
11	28.05 & 03.06(!)	Nelson-Oppen, QBF, PSPACE completeness
12	04.06 & 07.06	Ferrante-Rackoff, Cooper's Method
13	11.06 & 14.06	Arrays
14	18.06 & 21.06	Q&A, Repeat for exam
15	25.06	1st exam

Exam

The first exam (exam, handout, solution) was offered on June 25. It was 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:

• Daniel Kroenig and Ofer Strichman
  Decision Procedures — An Algorithmic Point of View (second edition)
  Springer, 2016
• Aaron Bradley and Zohar Manna
  The Calculus of Computation — Decision Procedures with Applications to Verification
  Springer, 2007

Slides and exercises are available from this page. Solutions to exercises will be made available via OLAT.