Information about the course Automated Reasoning (2IMF25)

This course will be given in the fall of 2021, in the first quartile. The lectures will be partly on campus, with the restriction of maximal 75 people in the lecture room. More precisely, the Monday lectures at 15:30 will be on-campus, and the Wednesday slot will at 10:45 will be replaced by an online meeting in Canvas conference. The full series of lectures recorded in 2020, is available and is up to date. Please watch them no later than the dates indicated in the schedule below. In the Monday lectures the same material will be presented in a somewhat condensed form; in the Wednesday online meetings apart from giving a survey of highlights, there will be the opportunity to ask questions. You are asked to indicate in a quiz on Canvas whether you intend to show up at the first lecture on September 6, in order to decide whether extra regulations are required to stay below the border 75 people in a room.

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

Students from the Radboud University in Nijmegen that (want to) follow this course should go to special information for Radboud University

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:



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; these groups of at most two persons should be registered in Canvas by yourselves as 'groups practical assignment'. 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: September 29, 2021 for the first part, and October 27, 2021 for the second part.
The reports of the practical assignment should be handed in via Canvas.


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:


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

Lectures to be followed.


lecture date topic slides
Nr 01 Monday, September 6 Overview, pigeon hole formula, SAT is NP-complete, arithmetic (addition and multiplication) in SAT 1 to 40
Nr 02 Wednesday, September 8 Program correctness by SAT, resolution, Davis-Putnam procedure, completeness of resolution 41 to 73
Nr 03 Monday, September 13 DPLL, conflict driven clause learning, dimacs format, Tseitin transformation 74 to 107
Nr 04 Wednesday, September 15 tool syntax, 8 queens problem, linear programming: Simplex method 108 to 150
Nr 05 Monday, September 20 Linear programming: Simplex method, SMT solving: rectangle fitting, ILP is NP-complete 151 to 187
Nr 06 Wednesday, September 22 Model checking, NuSMV, CTL 188 to 228
Nr 07 Monday, September 27 Deadlock detection in hardware, unique representation of boolean functions, decision trees 229 to 256
Nr 08 Wednesday, September 29 Decision trees, BDDs 257 to 314
Nr 09 Monday, October 4 BDDs, predicate logic, resolution, unification 315 to 344
Nr 10 Wednesday, October 6 Unification, resolution, Prolog, Prenex normal form, Skolemization 345 to 366
Nr 11 Monday, October 11 Example prenex normal form and skolemization, Prover9, equational reasoning, term rewriting 367 to 387
Nr 12 Wednesday, October 13 Term rewriting: monotonic interpretations, lpo, dependency pairs, well-founded induction, Newman's Lemma 388 to 414
Nr 13 Monday, October 18 Critical pairs, word problem, Knuth-Bendix completion, overview course 415 to 435
Nr 14 Wednesday, October 20 Presentation of examination January, 2020 (not on videocollege)



Last change: January 25, 2022