**Instructor** : Ashutosh Gupta

**Timings** : Tuesday and Friday, 14:00-15:25

**Venue** : CC 101

**TA** : Avais Ahmad (M-tech-2) (avais _at_ cse . iitb . ac . in)

The course is about the design and implementation of solvers for proving/disproving validity of statements in various logics. The solvers are often referred as reasoning engines, hence the course name *automated reasoning*. The reasoning problems are inherently hard and there are no known provably efficient algorithms for them. However, we may have efficient heuristics that may solve some interesting and important instances of the problems. In the last three decades, automated reasoning has risen to be a matured and an effective technology that can be applied to the reasoning problems arising from a wide range of fields.

The course will cover five major topics: satisfiability solvers, satisfiability modulo theories solvers, decision procedures (theories), interactive theorem provers, and first order logic solvers. In each part, we will discuss encoding the problems of interest into the reasoning problems, the efficient heuristics, the implementation issues of the heuristics, and their theoretical understanding. The course will include programming assignments/projects.

- Book: A First Course in Logic - Shawn Hedman
- Handbook of Satisfiability - by A. Biere (Editor), et al.
- Book chapter: The Art of computer programming Section 7.2.2.2 (Beta version) - Donald Kunuth
- Handbook of Automated reasoning - by A. Robinson (Editor), et al.
- Z3 source code
- Book: Decision Procedures
- Book: Theory of Linear and Integer Programming, Alexander Schrijver
- Coq tutorial
- Algorithms for the Satisfiability (SAT) Problem - Gu et. al. p67-74

- Text book: A Mathematical Introduction to Logic, Second Edition - Herbert B. Enderton
- NPTEL Video Course: Mathematical logic - Arindama Singh, IITM
- Book: Symbolic logic, Fifth edition - Irving M. Copi
- Introduction to BDDs - Henrik Reif Anderson
- Book: First-Order Logic and Automated Theorem Proving - Melvin Fitting

- Programming assignments: 5% 15% 15% 10%
- Quizzes : 10% (5% each)
- Midterm : 20% (1 hour)
- Presentation: 10% (15 min)
- Final: 15% (2 hour)

- Introduction, course contents, introduction to SAT/SMT problems
- Introduction to first-order logic (FOL) syntax
- Lecture 1 slides
- Suggested reading : Hedman 2.1-2.2 (p53-57), 2016 Logic Lecture 2 slides for discussion on parsing
- Please install Z3 and its python interface before lecture 3
- Z3 installation instructions Linux Windows

- FOL semantics, FOL theory, Theory examples
- Lecture 2 slides
- Suggested reading : Hedman 2.3-2.4, 2.7

- Using Python interface of Z3, SMT2 file format
- Encoding simple problems into satisfiability problems
- Lecture 3 slides
- Suggested reading : A tutorial on z3py
- Assignment 1: Problems 3.9-3.13 in the slides, Due date : 2018-08-03 (lecture 6)
- Each group will do one problem! Problem Assignments

- CNF(conjunctive normal form), DPLL
- CDCL(conflict-driven clause learning), Learned clause minimization
- Lecture 4 slides
- Suggested reading : Handbook of Satisfiability (2009), chapter 4.1-4.4
- We need
**two volunteers**to give 15 min presentations each in lecture 6.

- 2-watched literals, restarts, decision orderings
- learned clause deletion, pre-processing
- Lecture 5 slides
- Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5

- 2-SAT problem
- Sat encoding of graph coloring implementation , pigeon-hole principle
- Encoding cardinality constraints, psuedo-boolean constraints
- Solving sudoku
- Lecture 6 slides
- Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT
- Assignment 2: Problems 6.13-6.15 in the slides, Due date : 2018-08-17 (lecture 6)
- Each group will do one problem! Problem Assignments

- CDCL(Theory), Theory interface
- QF_EUF(Quantifier-free theory of equality and uninterpreted functions)
- Lecture 7 slides
- Suggested reading: DPLL(T)

- Ackermann's Reduction, Lazy vs. Eager solving
- Completeness of the lazy decision procedure
- Data structures for EUF, union-find, proof generation, congruence table
- Lecture 8 slides
- Suggested reading: Decision Procedures, chapter 3
- Suggested reading(in depth): Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. (section 4.2 and section 7)

- We will need Z3 compiled in debug mode and some supporting tools;Installation instructions
- Input file for the lecture class.smt2
- Lecture 9 slides

- Fundamental theorem of linear inequality
- Duality theorem, Farkas lemmas
- Lecture 10 slides
- Suggested reading : Schrijver chapter 7, sections 7.1,7.2(only definitions),7.3,7.4,7.6

- Simplex
- Lecture 11 slides
- Suggested reading : Decision Procedures, section 5.1-5.2
- Suggested reading (in depth) : Schrijver chapter 11, sections 11.1,11.2 (whole chapter is worth reading!!)

- Fourier-Motzkin
- Ellipsoid method
- Lecture 12 slides
- Suggested reading : Schrijver sections 12.2, 13.1-13.4

- Integral solutions of system of linear equations, Hermit normal form
- Integer hull, Hilbert basis
- Lecture 13 slides
- Suggested reading : Schrijver sections 4.1-2, 16.1,16.2,16.4

- Total duality integrality, Cutting planes, Gomery cut
- Lecture contents of 14-15 overlapped and are in a single presentaion.
- Lecture 14 slides
- Suggested reading : Schrijver sections 22.1, 23.1, 23.2, 23.8(Gomery cut presented here has a diffrent normal form!)
- Assignment 3: problem statement Due date : 2018-10-02 (lecture 18)
- All groups will do same problem and compete!

- We will exclude Elloposid method and Cooper's method from the midterm.

- Difference Logic, Difference bound matrix, Tightness
- Octagonal constraints, Octagonal difference bound matrix
- Lecture 16 slides
- Suggested reading : Slides are developed from papers and source codes that are cited in the slides.

- Axioms of arrays, implementation and optimizations for arrays
- a decidable fragment of quantified array formulas
- Lecture 17 slides
- Suggested reading : L. Moura, N. Bjorner, Generalized, Efficient Array Decision Procedures. FMCAD09 (section 2-4)
- Suggested reading : Decision Procedures, chapter 7

- Bitvector semantics and operators
- Term rewriting and bit blasting
- Modular arithmetic
- Lecture 18 slides
- Suggested reading : Decision Procedures, chapter 6

- Nelson-Oppen method
- Correctness and implementation of the method
- Lecture 19 slides

- SAT solver as oracle
- Solving MaxSat using SAT solvers
- Lecture 20 slides
- Suggested reading : extended tutorial

- Clausal proofs, proof checking, resolution proofs
- Proof minimization
- Lecture 21 slides
- Suggested reading : proof formats

- Interpolants, partial interpolants
- Interpolants in propositional logic, QF_LRA, and QF_EUF
- Lecture 22 slides
- Suggested reading :

- Second quiz
- Please bring a laptop in the class with Coq installed.
- Coq syntax, tactics, basic type system, proof scripts, proof terms
- Boolean reasoning, Predicate logic, Equality, Inductive types, Fixedpoints
- Lecture 25/26 slides
- Suggested reading : Coq tutorial
- Suggested reading : Another Coq tutorial
- Assignment 4: all groups will solve problem 25.11. Deadline: 2018-11-09

- Lecture 23 slides
- Suggested reading : Leonardo de Moura and Nikolaj Bjorner, Efficient E-matching for SMT Solvers (section 1-4)
- Link to the presentation for QBF: QBF slides (slides 15-44)

Student | Date | Topic | |
---|---|---|---|

1 | Adwait | 2018-08-07 | Vadim Ryvchin and Alexander Nadel. Chronological Backtracking, SAT 18 |

2 | Aditya | 2018-08-10 | Sima Jamali and David Mitchell. Centrality-Based Improvements to CDCL Heuristics. SAT 18 |

3 | Ajeesh | 2018-08-17 | Jia Liang et al. Machine Learning-based Restart Policy for CDCL SAT Solvers. SAT 18 |

4 | Akhil | 2018-08-24 | Jan Elffers et al. Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers |

5 | Akshith | 2018-10-05 | Simplex is average time linear!(Late) |

6 | Ananya | 2018-09-04 | Rewrites for SMT Solvers using Syntax-Guided Enumeration. A. Reynolds et el. |

7 | Balaji | 2018-10-16 | Array Folds Logic, Przemyslaw Daca, Thomas A. Henzinger, Andrey Kupriyanov, CAV 16 |

8 | Harsha | 2018-10-12 | Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv: Generalizing DPLL to Richer Logics. 462-476, CAV 2009 |

9 | Kalyani | 2018-10-23 | Cuts from Proofs, Isil Dillig, Thomas Dillig, Alex Aiken, CAV 2009 |

10 | Lohith | 2018-11-04 | Tobias Paxian, Sven Reimer and Bernd Becker. Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT, SAT18 |

11 | Sharath | 2018-11-04 | fer Guthmann, Ofer Strichman, Anna Trostanetski. Minimal unsatisfiable core extraction for SMT, FMCAD16 |

12 | Teja | 2018-11-04 | Vijay D'Silva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher. Interpolant Strength, VMCAI 2010 |

Last modified: ()