date 
topic 
slides 
Monday, November 12 
Overview, pigeon hole formula, SAT is NPcomplete, arithmetic (addition)
in SAT 
1 to 33 
Thursday, November 15 
Multiplication, program correctness by SAT, resolution, DavisPutnam procedure 
34 to 59 
Monday, November 19 
Completeness of resolution, DPLL, conflict driven clause learning 
60 to 91 
Thursday, November 22 
Dimacs format, Tseitin transformation, 8 queens, rectangle fitting 
92 to 110, MOOC examples 3060 
Monday, November 26 
Linear programming: Simplex method, SMT solving 
111 to 145 
Thursday, November 29 
SMT solving, examples, ILP is NPcomplete, unique representation 
146 to 162 
Monday, December 3 
Reachability, NuSMV, Decision trees 
163 to 187 
Thursday, December 6 
BDDs 
188 to 207 
Monday, December 10 
BDDs, Predicate logic, resolution, unification 
208 to 239 
Thursday, December 13 
Unification, resolution, Prolog 
240 to 259 
Monday, December 17 
Prenex normal form, Skolemization, Prover9, equational
reasoning

260 to 280 
Thursday, December 20 
Term rewriting: main properties, termination,
wellfounded induction, Newman's Lemma 
281 to 304 
Monday, January 7 
Term rewriting: critical pairs, word problem, KnuthBendix completion 
305 to 322 
Thursday, January 10 
KnuthBendix completion, overview course, old exam
(last lecture) 
323 to 325 