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)	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.