Information about the course Automated Reasoning (2IW15)

This course will be given in the fall of 2012, in the second quartile on Monday from 15.45 to 17.30 and Thursday from 10:45 to 12:30.
Lectures from 2009 are available on video

Teacher: Prof Dr H. Zantema, Metaforum 7.067, tel 2749, h.zantema@tue.nl

Goal:
Obtaining insight how various problems can be transformed to formulas, and can be solved automatically by computer programs manipulating these formulas.


Contents:
Many problems, in particular in the area of verification of computer systems, can be expressed as proving that some big formula is always true. In this course we will concentrate on various methods for treating this kind of problems. Not only correctness and completeness of these methods will be considered, also efficiency and usability. In particular we will consider:

• Satisfiability of propositions: tableaux method, resolution, and the main ingredients of modern satisfiability provers.
  
• Satisfiability modulo theories, in particular using linear inequalities, and the underlying simplex algorithm.
  
• Binary Decision Diagrams as efficient representation of boolean expressions.
  
• Unification; resolution on predicates.
  
• Reasoning modulo equations, term rewriting.

Examination:
The examination consists of two parts: a written exam and a practical assignment. The written exam is `closed book': no use of books or notes is permitted during the exam. The practical assignment is done by at most two persons. In case the practical assignment is done by two persons, each of them should be responsible for the whole work, possibly checked by an individual test. The practical assignment has two deadlines: December 10, 2012 for the first part, and January 14, 2013 for the second part.

For both the written exam and the practical assignment, the grade should be at least 5.0. In that case the final grade is the average of both parts, each having the same weight. Otherwise the final grade is the minimum of both parts.


To be downloaded:

• The slides used in the course in handout format, version January 9, 2013.
  
• For the practical assignment:
  
  
  
  • The text for the assignment in PDF format, including guidelines and the problems to be solved.
  • An example of how to present the solution of a problem for the practical assignment. Also the LaTeX source of this example is available.
    
  • The tool yices: a program for satisfiability modulo theories (SMT). It accepts SMT format, in particular it can be used as a boolean SAT solver.
  • The tool bddsolve: a program based on BDDs. It can be used for satisfiability and counting the number satisfying assignments, and for reachability.
  
  
• Some old exams.
  
  • November, 2006, with solutions
    
  • June, 2009
    
  • August, 2009
    
  • June, 2010
    
  • August, 2010
    
  • June, 2011, with solutions
    
  • August, 2011
    
  • January, 2012
  • April, 2012
  • January, 2013

Some of the material of the course is based on the books:

S. N. Burris:
Logic for Mathematics and Computer Science
Prentice Hall, 1998, ISBN 0-13-285974-2

C. Meinel and T. Theobald:
Algorithms and Data Structures in VLSI Design
Springer, 1998, ISBN 3-540-64486-5

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest and Clifford Stein:
Introduction to Algorithms
MIT Press, 2009, ISBN 978-0-262-53305-8
Third Edition, only Chapter 29


Lectures and topics:

date	topic	slides
Monday, November 12	Overview, pigeon hole formula, SAT is NP-complete, arithmetic in SAT	1 to 36
Thursday, November 15	Program correctness by SAT, resolution, Davis-Putnam	37 to 59
Monday, November 19	Completeness of resolution, DPLL	60 to 81
Thursday, November 22	Conflict driven clause learning, Tseitin transformation	82 to 105
Monday, November 26	Linear programming: Simplex method	106 to 135
Thursday, November 29	SMT solving, pseudo boolean constraints, unique representation, reachability	136 to 162
Monday, December 3	Decision trees and BDDs	163 to 183
Thursday, December 6	BDDs	184 to 202
Monday, December 10	Predicate logic, resolution, unification	203 to 227
Thursday, December 13	Unification, resolution, Prolog, prenex normal form	228 to 243
Monday, December 17	Skolemization, equational reasoning, term rewriting	244 to 256
Thursday, December 20	Term rewriting: main properties, termination undecidable, termination by monotone interpretations	257 to 271
Monday, January 7	Term rewriting: lexicographic path order, Newman's Lemma, critical pairs	272 to 285
Thursday, January 10	Term rewriting: word problem, Knuth-Bendix completion, overview course (last lecture)	286 to 300

Last change: April 10, 2013