This page is devoted to lectures for the course. Lecture slides and other study material can be found here.
| Date | Topic |
Slides |
| 9.10.2015 | Propositional Logic, Normal Forms of Formulae, Tseitin Encoding |
[PDF] |
| 15.10.2015 | SAT Solvers, DPLL, CDCL, 2-watched Literals |
[PDF] |
| 23.10.2015 | BDDs, GSAT, WalkSAT, Warning Propagation |
[PDF] |
| 30.10.2015 | Equality Theory and Uninterpreted Functions |
[PDF] |
| 6.11.2015 | Decision Procedures for Equality Logic Formulae |
[PDF] |
| 13.11.2015 | Small Domain Allocation |
[PDF] |
| 20.11.2015 | Bit Vector Arithmetics |
[PDF] |
| 27.11.2015 | Decision Procedures for Array and Pointer Logic Formulae |
[PDF] |
| 4.12.2015 | Combination of Theories, Nelson-Oppen Procedure |
[PDF] |
| 18.12.2015 | Satisfiability Modulo Theories (SMT) Problem |
[PDF] |
| 8.1.2016 | Linear Arithmetics |
[PDF] |