# Decision Procedures (WM 5)

## master program

VO2 + VO1 + PS2  SS 2014  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 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),

### Schedule

week date slides slides2 exercises solutions remarks
1 03.03 & 05.03 pdf (1, 4) pdf (1, 2, 4) pdf
2 10.03 & 12.03 pdf (1, 4) pdf (1, 2, 4) pdf link
3 17.03 & 19.03 pdf (1, 4) pdf (1, 2, 4) pdf
4 24.03 & 26.03 pdf (1, 4) pdf (1, 2, 4) pdf link
5 31.03 & 02.04 pdf (1, 4) pdf (1, 2, 4) pdf
6 07.04 & 09.04 pdf (1, 4) pdf (1, 2, 4) pdf
7 28.04 & 30.04 pdf (1, 4) pdf (1, 2, 4) pdf
8 05.05 & 07.05 pdf (1, 4) pdf (1, 2, 4) pdf
9 12.05 & 14.05 pdf (1, 4) pdf (1, 2, 4) pdf
10 19.05 & 21.05 pdf (1, 4) pdf (1, 2, 4) pdf
11 26.05 & 28.05 pdf (1, 4) pdf (1, 2, 4) pdf
12 02.06 & 04.06 pdf (1, 4) pdf (1, 2, 4) pdf evaluation
13 09.06 & 11.06 pdf (1, 2, 4) pdf
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
The 2nd exam for the course 703620 takes place on October 10 (09:00 – 11:00, 3W04);
online registration is required until 10 am on October 8.