date 
topic 
slides 
September 3 
Overview, pigeon hole formula, SAT is NPcomplete, arithmetic (addition and multiplication)
in SAT 
1 to 37 
September 10 
Program correctness by SAT, resolution, DavisPutnam procedure, completeness of resolution 
38 to 69 
September 17 
DPLL, conflict driven clause learning, dimacs format, SMT syntax 
70 to 95, 176183 
September 24 
Tseitin transformation, 8 queens, linear programming: simplex method 
96 to 152 
October 1 
Linear programming: simplex method, SMT solving, ILP is NPcomplete, model checking / transition systems 
153 to 188 
October 8 
Model checking, CTL, deadlock detection in hardware 
189 to 232 
October 15 
NuSMV, unique representation, decision trees, BDDs 
233 to 280 
November 5 
BDDs, predicate logic 
281 to 324 
November 12 
Predicate logic, resolution, unification 

November 19 
Unification, resolution, Prolog 

November 26 
Prenex normal form, Skolemization, Prover9, equational
reasoning


December 3 
Term rewriting: main properties, termination,
wellfounded induction, Newman's Lemma 

December 10 
Term rewriting: critical pairs, word problem, KnuthBendix completion 

December 17 
KnuthBendix completion, overview course, old exam
(last lecture) 
