Information about the course Automated Reasoning (NWI-IMC009)

Teacher: Prof Dr H. Zantema, h.zantema@tue.nl

This course will be given in the fall of 2021, in the first semester.

The course will be offered partly on campus, on Tuesday, 13:30, with roughly one lecture in two weeks, starting at September 7, see schedule below. In between there will be online meetings in Brightspace Virtual Classroom, also on Tuesday, 13:30. Please watch the corresponding recorded lectures before these meetings.
The full series of recorded lectures from 2020 is available and up to date. They are numbered, please follow them no later than indicated in the schedule below. The physical lectures will cover roughly two of these recorded lectures each.

You may always ask questions to h.zantema@tue.nl.

The first eight lectures are roughly covered by the MOOC available at https://www.coursera.org/learn/automated-reasoning-sat and https://www.coursera.org/learn/automated-reasoning-symbolic-model-checking, where this material has been split up into several professionally recorded lectures of around 10 minutes. After registration by entering name and email address, these MOOC lectures are accessible for free.

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: 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, as the basis of symbolic model checking.
  
• 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: November 2, 2021 for the first part, and January 5, 2022 for the second part.
The reports of the practical assignment should be handed in via Brightspace. If you do it with two people, only one of them should submit.


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 September, 2021 .
  
• For the practical assignment:
  
  
  
  • The text for the assignment in PDF format, including guidelines and the problems for both parts 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 Z3: a program for satisfiability modulo theories (SMT). It accepts SMT format.
  • The tool NuSMV: a symbolic model checker based on BDDs.
  • The tools Prover9 and Mace4: tools for predicate logic and equational reasoning, based on resolution and finding finite counterexamples.
  
  
• Some old exams (some from Eindhoven, but covering the same material)
  
  • January, 2016, with solutions
  • April, 2016
  • January, 2017
  • April, 2017
  • January, 2018
  • April, 2018
  • January, 2019
  • March, 2019
  • January, 2020
  • April, 2020
  • Presentation of examination April, 2020
  • January, 2021
  • March, 2021
  • January, 2022
  
  
  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 to be followed:
  

lecture	date	topic	slides
Nr 01	September 7 (lecture on campus)	Overview, pigeon hole formula, SAT is NP-complete, arithmetic (addition and multiplication) in SAT	1 to 40
Nr 02	September 14 (lecture online)	Program correctness by SAT, resolution, Davis-Putnam procedure, completeness of resolution	41 to 73
Nr 03	September 21 (lecture online)	DPLL, conflict driven clause learning, dimacs format, Tseitin transformation	74 to 107
Nr 04	September 28 (lecture on campus)	8 queens problem, linear programming: simplex method	108 to 150
Nr 05	October 5 (lecture online)	Linear programming: simplex method, SMT solving, ILP is NP-complete	151 to 187
Nr 06	October 12 (lecture on campus)	Model checking, NuSMV, CTL	188 to 228
Nr 07	October 19 (lecture online)	Deadlock detection in hardware, unique representation of boolean functions, decision trees	229 to 256
Nr 08	November 9 (lecture on campus)	Decision trees, BDDs	257 to 314
Nr 09	November 16 (lecture online)	BDDs, Predicate logic, resolution, unification	315 to 344
Nr 10	November 23 (lecture on campus)	Unification, resolution, Prolog, Prenex normal form, Skolemization	345 to 366
Nr 11	November 30 (lecture online)	Prover9, Equational reasoning, term rewriting, main properties, termination	367 to 387
Nr 12	December 7 (lecture on campus)	Term rewriting: monotonic interpretations, lpo, dependency pairs, well-founded induction, Newman's Lemma	388 to 414
Nr 13	December 14 (lecture online)	Critical pairs, word problem, Knuth-Bendix completion, overview course	415 to 435
	December 21 (opportunity to ask questions online)	Presentation of examination April, 2020

Last change: January 25, 2022