**Instructor** : Ashutosh Gupta

**Mode of instruction** : weekly release of recorded videos and slides;
a weakly interactive session followed by an online quiz.

**Timings** : Inteactive session at 21:00 on Fridays

**Venue** : MSTeams, To join the course team, use team code: inff8lm (feel free to attend even if not taking the course)

**TA** : Kalyani Dole (PhD) (163050022 _at_ iitb . ac . in), Isha Pandey

**Quizes** : Quiz Portal (Login via CSE LDAP or special accounts)

The course is about the design and implementation of solvers for proving/disproving validity of statements in various logics arising in various areas such as verification of AI, software, hardware, etc. 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.

- Text book: Decision Procedures
- Supplementary sources
- Source codes
- Reference sources
- 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.
- Book: Theory of Linear and Integer Programming, Alexander Schrijver
- Algorithms for the Satisfiability (SAT) Problem - Gu et. al. p67-74

- Books on logic: (Any one should be ok!)
- A Mathematical Introduction to Logic, Second Edition - Herbert B. Enderton
- A First Course in Logic - Shawn Hedman
- First-Order Logic and Automated Theorem Proving - Melvin Fitting
- Logic in Computer Science Huth and Ryan
- Symbolic logic, Fifth edition - Irving M. Copi (For philosophy angle)
- NPTEL Video Course: Mathematical logic - Arindama Singh, IITM

- Programming assignments: 6% 10% 15% 10%
- Online Quizzes : 24% (2% each)
- Mid semester presentation: 10% (15 min)
- Final: 25% (2 hour)

- Videos: Intro
**No quiz in the first session.**

- Lecture 1 slides
- Videos: Logic classes, SAT problem, Derived problems
- Classes of logic, satisfiability problem, problems in logic

- Background slides CS228: 2020-CS228-lec-02 and 2020-CS228-lec-03
- Propositional logic syntax and semantics
- Lecture 2 slides: 2020-CS228-CNF-slides
- Video: NNF, CNF, Tseitens encoding
- Make groups of 2-3 students to do the assignments

- Background slides from CS228: CS228-lec-14 CS228-lec-15
- FOL syntax, semantics, and examples FOL theory
- Lecture 3 slides : 2020-CS228-Theory slides
- FOL theory, axioms, theory examples, and logic fragments (no video)
- Video: 3.0 Theory , 3.1 Axioms, 3.2 Theory examples,

- Z3(no video), Using Python interface of Z3(no video), SMT2 file format
- Encoding simple problems into satisfiability problems
- Lecture 4 slides
- Video: 4.3 SMT2 file format
- Please solve problems 4.3, 4.5-8, 4.14 on Z3 before coming to the class
- In live session, we will do 4.9 and 4.15, and a few others
- Suggested reading : A tutorial on z3py
- Assignment 1: Problems 4.16-4.20 in the slides, Due date : 2020-09-11 (lecture 8)
- Each group will do one problem! Problem Assignments

- CNF(conjunctive normal form), DPLL
- CDCL(conflict-driven clause learning), Learned clause minimization
- Lecture 5 slides
- Suggested reading : Handbook of Satisfiability (2009), chapter 4.1-4.4
- Video: 5.1 DPLL, 5.2 Clause learning, 5.3 CDCL, 5.4 Clause minimization,

- 2-watched literals, optimal storage, restarts
- decision orderings, learned clause deletion, phase saving
- Lecture 6 slides
- Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5
- Video: 6.1 2-watched, 6.2 Optimal storage, 6.3 Runtime choices,
- Assignment 2: Problems 6.13-6.16,6.21 in the slides, Due date : 2020-09-18 (lecture 10)
- Each group will do one problem! Problem Assignments

- 7.1 Binary decision diagrams(BDDs), 7.2 Reduced ordered BDDs(ROBDDs)
- 7.3 Algorithms for BDDs
- Lecture 7 slides
- Video: 7.1 BDDs, 7.2 ROBDDs, 7.3 Algorithm for BDDs,

- 8.1 Sat encoding of graph coloring, , pigeon-hole principle
- 8.2 Encoding cardinality constraints, 8.3 psuedo-boolean constraints(no video)
- 8.4 Solving sudoku and encoding bounded model checking(no video)
- Lecture 8 slides
- Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT
- Video: 8.1 Encoding problems, 8.2 Cardinality constraints

- 9.1 EUF theory, 9.2 Eager solver Ackermanns Reduction
- 9.3 Lazy solver, 9.4 Completeness of the lazy decision procedure
- Lecture 9 slides
- Video: 9.1 EUF, 9.2 Eager, 9.3 Lazy, 9.4 Completeness.

- 10.1 CDCL(Theory), 10.2 Theory deduction
- 10.3 Example theory interface for QF_EUF, 10.4 Optimizations(no video)
- Lecture 10 slides
- Suggested reading: DPLL(T)
- Video: 10.1 CDCLT, 10.2 Theory deduction, 10.3 Example theory interface.
- Assignment 3: (all groups) Problem 8.23 in the slides of lecture 8, Due date : 2020-10-10 (Post midsem week)

- 11.1 union-find, 11.2 Union-find in SMT solvers,
- 11.3 Implementing congruence, 11.4 implementing disequalities
- 11.5 Model generation (slides are at the end lecture 9)
- 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)
- Lecture 11 slides
- Video: 11.1 Union-find, 11.2 Union-find in SMT solver, 11.3 Congruence, 11.4 Disequality, 11.5 Model generation.

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

- 13.0 Introduction to linear arithmetic
- 13.1 Fundamental theorem of linear inequality
- 13.2 Satisfiability conditions, 13.3 Linear programming(LP) and duality theorem
- 13.4 Completeness
- Lecture 13 slides
- Suggested reading : Schrijver chapter 7, sections 7.1,7.2(only definitions),7.3,7.4,7.6
- Video: 13.0 Introduction, 13.1 Fundamental theorem Part 1, 13.1 Fundamental theorem Part 2, 13.2 Satisfiability, 13.3-4 LP and Completeness,

- Please choose a regular paper(full length; contributed) from SAT2020 program.
- You can borrow or make your own slides.(Points deducted for poor slides)
- Present to whole class in 15 mins
- Not compulsory for auditing students
- Midterm presentation assignment.

- 14.1 theory of LRA, 14.2 Intro to simplex
- 14.3 Notation for simplex, 14.4 Pivot operation
- 14.5 Incremental simplex(part video), 14.6 Complexity of simplex(no video)
- Lecture 14 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!!)
- Video: 14.1-2 Introduction to LRA and Simplex, 14.3 Notation, 14.4 Pivot, 14.5 Incremental,

- Fourier-Motzkin
- Ellipsoid method
- Lecture 15 slides
- Suggested reading : Schrijver sections 12.2, 13.1-13.4
- Video: 15.1 Fourier-Motzkin, 15.2 Ellipsoid method, 15.3 Ellipsoids, 15.4 Ellipsoid method (algorithm),

- 16.1-2 Introduction to Linear integer arithmetic(LIA)
- 16.3-4Integral solutions of system of linear equations, Hermit normal form
- 16.5Hilbert basis
- Lecture 16 slides
- Suggested reading : Schrijver sections 4.1-2, 16.1,16.2,16.4
- Video: 16.1-2 LIA, 16.3 HNF, 16.4 Sat condition, 16.5 Lattice, 16.6 Hilbert basis,

- 17.1 Gomery cut, 17.2 Coopers method(no video)
- Lecture 17 slides
- Video: 17.1 Gomery Cut,

- 18.1 Difference Logic, Difference bound matrix, 18.2 Tightness
- 18.3 Octagonal constraints, Octagonal difference bound matrix(ODBM), 18.4 ODBM tightness
- Lecture 18 slides
- Suggested reading : Slides are developed from papers and source codes that are cited in the slides.
- Video: 18.1 RDL, 18.2 Canonical, 18.3 Octagonal, 18.4 Octagonal Canonical,
- Assignment 4: Checking robustness of neural networks using SMT solver. Due date: 2020-11-20
- Find a trained neural network that classifies images and contains only ReLu and ArgMax non-linear neurons
- Using SMT solver, find the maximum perturbation (pixles altered upto a bound) on each training image such that the classification of the image is not changed
- All groups will do same problem!

- 19.1 Axioms of arrays, 19.2 implementation and optimizations for arrays
- 19.3 a decidable fragment of quantified array formulas(no videos)
- Lecture 19 slides
- Suggested reading : L. Moura, N. Bjorner, Generalized, Efficient Array Decision Procedures. FMCAD09 (section 2-4)
- Suggested reading : Decision Procedures, chapter 7
- Suggested reading : Aaron R. Bradley, Zohar Manna, Henny B. Sipma: What is Decidable About Arrays? VMCAI 2006
- Video: 19.1 Arrays, 19.2 Array solver

- 20.1 Bitvector semantics and operators,
- 20.2 Solving bit-vector formulas and Term rewriting, 20.3 bit blasting
- 20.4 Lazy bit blasting, 20.5 Modular arithmetic
- Lecture 20 slides
- Suggested reading : Decision Procedures, chapter 6

- 21.1 Nelson-Oppen method, 22.2 Correctness
- 22.3 implementation of the method
- Lecture 21 slides
- Video: 21.1 Nelson-Oppen method, 21.2 Correctness 21.3 Implementation

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

- By Prof. Supratik Chakraborty

- Please bring a laptop in the class with Coqide installed.
- Coq syntax, tactics, basic type system, proof scripts, proof terms
- Boolean reasoning, Predicate logic, Equality, Inductive types, Fixedpoints
- Lecture 27 slides
- Suggested reading : Coq tutorial
- Suggested reading : Another Coq tutorial

Last modified: ()