Master Program - Constraint Solving

VO2 + PS2  SS 2026  703304 + 703305

Overview

Lecturer

Type Lecturer Room Consulting Hours
VO + PS Manuel Eberl 3M03 Thursday, 10:30 - 11:30

Time and Place

VO Tuesday, 13:45 - 15:15 3W04 (ICT building, 2nd floor)
PS Monday, 12:00 - 13:30 3W04 (ICT building, 2nd floor)


The lecture (VO) starts on March 4th, the first exercise session (PS) is on March 10th.

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)

All material (slides, homework sheets, solutions, lecture recordings) are available on the OLAT sites of the lecture and proseminar.

Week Date Topics
01 04.03 & 10.03 SAT basics
02 11.03 & 17.03 Conflict Graphs, NP completeness
03 18.03 & 24.03 NP completeness of Shakashaka, MaxSAT
04 25.03 & 14.04 FO-Theories, SMT, DPLL(T)
05 15.04 & 21.04 Equality Logic, EUF
06 22.04 & 28.04 Difference Logic, Simplex
07 29.04 & 05.05 Farkas' Lemma, Complexity and Incrementality of Simplex
08 06.05 & 12.05 Branch-and-Bound, Small Model Property of LIA
09 13.05 & 19.05 Cubes and Equalities in LIA
10 20.05 & 26.05 Bit-Vector Arithmetic
11 27.05 & 02.06 Nelson-Oppen, QBF, PSPACE completeness
12 03.06 & 09.06 Ferrante-Rackoff, Cooper's Method
13 10.06 & 16.06 Arrays
14 17.06 Q&A, Repeat for exam
15 24.06 1st exam

Exam

The first exam will be on June 24. It will be closed book.
You can find old exams on this website of a previous iteration of this course.

Literature

The course is partly based on the following books: