date 
topic 
slides 
Monday, November 13 
Overview, pigeon hole formula, SAT is NPcomplete, arithmetic (addition)
in SAT 
1 to 33 
Thursday, November 16 
Multiplication, program correctness by SAT, resolution, DavisPutnam procedure 
33 to 59 
Monday, November 20 
Completeness of resolution, DPLL, conflict driven clause learning 
60 to 83 
Thursday, November 23 
Conflict driven clause learning, Tseitin transformation 
84 to 109 
Monday, November 27 
Linear programming: Simplex method, SMT solving 
110 to 137,
slides for mooc

Thursday, November 30 
SMT solving, ILP is NPhard, unique representation, reachability 
138 to 167 
Monday, December 4 
NuSMV, Decision trees and BDDs 
168 to 194 
Thursday, December 7 
BDDs, predicate logic 
195 to 227 
Monday, December 11 
Predicate logic, resolution, unification 
228 to 249 
Thursday, December 14 
Prolog, prenex normal form, Skolemization, Prover9, equational
reasoning 
250 to 270 
Monday, December 18 
Term rewriting: main properties, termination undecidable,
termination by monotone interpretations 
271 to 288 
Thursday, December 21 
Termination by monotone interpretations and lexicographic path order,
wellfounded induction, Newman's Lemma, critical pairs 
289 to 304 
Monday, January 8 
Term rewriting: critical pairs, word problem, KnuthBendix completion 
305 to 315 
Thursday, January 11 
Critical pairs, overview course, old exam
(last lecture) 
316 to 321 