# Decision Procedures (WM 5)

## master program

VO2 + VO1 + PS2  SS 2016  703620 + 703621 + 703622

### Content

The module provides an introduction into the theory and practice of decision procedures. The course 703620 covers the theory of decision procedures and includes 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).

### Schedule

week date slides slides2 exercises solutions remarks
1 07.03 & 11.03 pdf (1, 4) pdf (1, 4) pdf pdf link
2 14.03 & 18.03 pdf (1, 4) pdf (1, 4) pdf pdf
3 04.04 & 08.04 pdf (1, 4) pdf pdf
4 11.04 & 15.04 pdf (1, 4) pdf (1, 4) pdf
5 18.04 & 22.04 pdf (1, 4) pdf (1, 4) pdf
6 25.04 & 29.04 pdf (1, 4) pdf (1, 4) pdf
7 02.05 & 13.05 pdf (1, 4) pdf pdf
8 09.05 & 20.05 pdf (1, 4) pdf pdf
9 23.05 & 27.05 pdf (1, 4) pdf
10 30.05 & 03.06 pdf (1, 4) pdf pdf
11 06.06 & 10.06 pdf (1, 4) pdf
12 13.06 & 17.06 pdf (1, 4) pdf (1, 4) pdf
13 20.06 & 24.06 pdf (1, 4) pdf
14 27.06 & 01.07 exams