This page is devoted to lectures for the course. Lecture slides and other study material can be found here.
| Date | Topic |
Slides | Video |
| 9.10.2013 | Propositional logic, normal forms of formulae, Tseitin encoding |
[PDF] |
|
| 16.10.2013 | SAT solvers, DPLL, CDCL, 2-watched literals |
[PDF] |
|
| 24.10.2013 | BDDs, GSAT, WalkSAT, Warning propagation |
[PDF] |
|
| 14.11.2013 | Equality logic, uninterpreted function, Ackermann's reduction |
[PDF] |
|
| 21.11.2013 | From equality logic to propositional logic |
[PDF] |
|
| 5.12.2013 | Construction of small adequate domain |
[PDF] |
|
| 12.12.2013 | Deciding bit vector arithmetic |
[PDF] |
|
| 19.12.2013 | Array and pointer logic |
[PDF] |
|
| 9.1.2014 | Deciding in combined theories |
[PDF] |
|