Information about the course Automated Reasoning (2IMF25)

This course will be given in the fall of 2020, in the first quartile.

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

Due to Covid19 regulations the course will be offered by a series of recorded lectures. All of these lectures will be available before the dates as they are indicated in the schedule below. Please watch them no later than the indicated dates.

On every Monday at 15:30 you will be invited for a Canvas Conference. Here organizational issues will be mentioned and you have the opportunity to ask questions. The last regular one was on October 12; close to the examination there will be one more such meeting to ask questions; this will be on Monday, October 26, 15:30. Apart from that, 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 examination will be on November 6, 2020, from 13:30 - 16:30, on campus, following the Covid-19 guidelines; in any case it will be arranged in such a way that the distance between any two people will always be >= 1.5 meter.
If you do not have the opportunity to do the examination physically at the TU/e in this way, please send an email to h.zantema@tue.nl explaining why not. Depending on the reactions, an alternative may be arranged.

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



Last change: October 12, 2020