This page is devoted to lectures for the course. Lecture slides and other study material can be found here.
| Date | Topic |
Slides |
| 8.10.2014 | Propositional Logic, Normal Forms of Formulae, Tseitin Encoding |
[PDF] |
| 15.10.2014 | SAT Solvers, DPLL, CDCL, 2-watched Literals |
[PDF] |
| 22.10.2014 | BDDs, GSAT, WalkSAT, Warning Propagation |
[PDF] |
| 29.10.2014 | Equality Theory and Uninterpreted Functions |
[PDF] |
| 5.11.2014 | Decision Procedures for Equality Logic Formulae |
[PDF] |
| 26.11.2014 | Small Domain Allocation |
[PDF] |
| 3.12.2014 | Bit Vector Arithmetics |
[PDF] |
| 10.11.2014 | Decision Procedures for Array and Pointer Logic Formulae |
[PDF] |
| 17.12.2014 | Combination of Theories, Nelson-Oppen Procedure |
[PDF] |
| 7.1.2015 | Satisfiability Modulo Theories (SMT) Problem |
[PDF] |