SAT and SMT Solving
- Definition of SAT
- NP-completeness
- Usual reductions from SAT to 3CNF-SAT etc.
- Davis–Putnam–Logemann–Loveland (DPLL) algorithm, Conflict Driven Clause Learning (CDCL)
- Explosion of CDCL on pigeons
- SMT
- DPLL(T)
- Optimisation of SMT solutions
- Explosion of DPLL(T) on interesting cases
