Content
The module provides an introduction into the theory and practice of decision procedures.The course 703620 covers the theory of decision procedures and covers the following topics:
- propositional logic (SAT),
- equality logic with uninterpreted functions (EUF),
- linear arithmetic (LIA and LRA),
- quantified boolean formulas (QBF),
- satisfiability modulo theories (SMT).
The course 703621 shows how (real world) problems can be encoded in different logics for which sophisticated tools exist. The following logics are covered:
- propositional logic (SAT),
- pseudo boolean constraints (PBC),
- satisfiability modulo theories (SMT),
- non-linear integer arithmetic (NIA),
- answer set programming (ASP).
Schedule
week | date | slides | slides2 | exercises | solutions | remarks |
---|---|---|---|---|---|---|
1 | 03.03 & 05.03 | pdf (1, 4) | pdf (1, 2, 4) | |||
2 | 10.03 & 12.03 | pdf (1, 4) | pdf (1, 2, 4) | link | ||
3 | 17.03 & 19.03 | pdf (1, 4) | pdf (1, 2, 4) | |||
4 | 24.03 & 26.03 | pdf (1, 4) | pdf (1, 2, 4) | link | ||
5 | 31.03 & 02.04 | pdf (1, 4) | pdf (1, 2, 4) | |||
6 | 07.04 & 09.04 | pdf (1, 4) | pdf (1, 2, 4) | |||
7 | 28.04 & 30.04 | pdf (1, 4) | pdf (1, 2, 4) | |||
8 | 05.05 & 07.05 | pdf (1, 4) | pdf (1, 2, 4) | |||
9 | 12.05 & 14.05 | pdf (1, 4) | pdf (1, 2, 4) | |||
10 | 19.05 & 21.05 | pdf (1, 4) | pdf (1, 2, 4) | |||
11 | 26.05 & 28.05 | pdf (1, 4) | pdf (1, 2, 4) | |||
12 | 02.06 & 04.06 | pdf (1, 4) | pdf (1, 2, 4) | evaluation | ||
13 | pdf (1, 2, 4) | |||||
14 | 16.06 & 18.06 | pdf (1, 4) | pdf (1, 2, 4) | |||
15 | 23.06 & 25.06 | exam 1:TDP PDP | ||||
– | 03.10 & 10.10 | exam 2:PDP |
online registration is required until 10 am on October 8.