**Instructor** : Ashutosh Gupta

**PG students can take the course.**

**Timings** : Monday and Thursday 19:00-20:25

**Venue** : CC101

**TA** : No TA

**First session** : 2022-07-28T08:30 (50 min session), FC Kohli

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

**For Discussion** : Join MSTeams with code: w00nhhx

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 simple quizzes : 24% (2% each)
- Mid semester presentations: 10% (15 min)
- End of semester presentation: 10% (15 min)
- Final: 15% (2 hour) or an additional project

May change later.

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

- Lecture 2 slides: 2022-CS228-CNF-slides (Section 7.1-7.3)
- Video: NNF, CNF, Tseitens encoding
- Make groups of 2-3 students to do the assignments

- Videos: 14.1 FOL syntax, 14.2 FOL semantics, 15.1 more definitions
- Slides: 2022-CS228-13-FOL-slides, 2022-CS228-14-FOL-Handling (Sections 14.1-14.2)
- FOL syntax, semantics, and examples

- Lecture 4 slides : 2022-CS228-Theory slides
- FOL theory, axioms, and theory examples
- Video: 4.0 Theory , 4.1 Axioms, 4.2 Theory examples,

- Z3(no video), Using Python interface of Z3(no video), SMT2 file format
- Encoding simple problems into satisfiability problems
- Lecture 5 slides
- Video: Using Z3, SMT2 file format
- Suggested reading : A tutorial on z3py
- Assignment 1: Problems 5.16-5.20 in the slides, Due date : (lecture 8)
- Each group will do one problem! Problem Assignments

- CNF(conjunctive normal form), DPLL
- CDCL(conflict-driven clause learning)
- Lecture 6 slides
- Suggested reading : Handbook of Satisfiability (2009), chapter 4.1-4.4
- Video: 6.1 DPLL, 6.2 Clause learning, 6.3 CDCL,

- Learned clause minimization, 2-watched literals, optimal storage
- Lecture 7 slides
- Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5
- Video: 7.4 Clause minimization, 7.1 2-watched, 7.2 Optimal storage,

- restarts, decision orderings, learned clause deletion, phase saving
- pre(in)-processing
- Lecture 8 slides
- Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5
- Video: Runtime choices,
- Assignment 2: Problems 8.11-13 in the slides, Due date : Lecture 12
- Each group will do one problem! Problem Assignments

- 9.1 Binary decision diagrams(BDDs), 9.2 Reduced ordered BDDs(ROBDDs)
- 9.3 Algorithms for BDDs
- Lecture 9 slides
- Video: 9.1 BDDs, 9.2 ROBDDs, 9.3 Algorithm for BDDs,

- 10.1 Sat encoding of graph coloring, implementation, pigeon-hole principle
- 10.2 Encoding cardinality constraints, 10.3 psuedo-boolean constraints(no video)
- 10.4 Solving sudoku and encoding bounded model checking(no video)
- Lecture 10 slides
- Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT
- Video: 10.1 Encoding problems, 10.2 Cardinality constraints

- 11.1 EUF theory, 11.2 Eager solver Ackermanns Reduction
- 11.3 Lazy solver, 11.4 Completeness of the lazy decision procedure
- Lecture 11 slides
- Video: 11.1 EUF, 11.2 Eager, 11.3 Lazy, 11.4 Completeness.

- 12.1 CDCL(Theory), 12.2 Theory deduction
- 12.3 Example theory interface for QF_EUF, 12.4 Optimizations(no video)
- Lecture 10 slides
- Suggested reading: DPLL(T)
- Video: 12.1 CDCLT, 12.2 Theory deduction, 12.3 Example theory interface.

- 13.1 union-find, 13.2 Union-find in SMT solvers,
- 13.3 Implementing congruence, 13.4 implementing disequalities
- 13.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 13 slides
- Video: 13.1 Union-find, 13.2 Union-find in SMT solver, 13.3 Congruence, 13.4 Disequality, 13.5 Model generation.

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

- We will get back to this lecture!
- We will need Z3 compiled in debug mode and some supporting tools;Installation instructions
- Input file for the lecture class.smt2
- Lecture 14 slides

- 15.0 Introduction to linear arithmetic
- 15.1 Fundamental theorem of linear inequality
- 15.2 Satisfiability conditions, 15.3 Linear programming(LP) and duality theorem
- 15.4 Completeness
- Lecture 15 slides
- Suggested reading : Schrijver chapter 7, sections 7.1,7.2(only definitions),7.3,7.4,7.6
- Video: 15.0 Introduction, 15.1 Fundamental theorem Part 1, 15.1 Fundamental theorem Part 2, 15.2 Satisfiability, 15.3-4 LP and Completeness,

- 16.1 theory of LRA, 16.2 Intro to simplex
- 16.3 Notation for simplex, 16.4 Pivot operation
- 16.5 Incremental simplex(part video), 16.6 Complexity of simplex(no video)
- Lecture 16 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: 16.1-2 Introduction to LRA and Simplex, 16.3 Notation, 16.4 Pivot, 16.5 Incremental,
- Assignment 4: Checking robustness of neural networks using SMT solver. Due date: Last lecture
- 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

- 17.1-2 Introduction to Linear integer arithmetic(LIA)
- 17.3-4Integral solutions of system of linear equations, Hermit normal form
- 17.5Hilbert basis
- Lecture 17 slides
- Suggested reading : Schrijver sections 4.1-2, 16.1,16.2,16.4
- Video: 17.1-2 LIA, 17.3 HNF, 17.4 Sat condition, 17.5 Lattice, 17.6 Hilbert basis,

- 18.1 Gomery cut, 18.2 Coopers method(no video)
- Lecture 18 slides
- Video: 18.1 Gomery Cut,

- 19.1 Difference Logic, Difference bound matrix, 19.2 Tightness
- 19.3 Octagonal constraints, Octagonal difference bound matrix(ODBM), 19.4 ODBM tightness
- Lecture 19 slides
- Suggested reading : Slides are developed from papers and source codes that are cited in the slides.
- Video: 19.1 RDL, 19.2 Canonical, 19.3 Octagonal, 19.4 Octagonal Canonical,

- 20.1 Axioms of arrays, 20.2 implementation and optimizations for arrays
- 20.3 a decidable fragment of quantified array formulas(no videos)
- Lecture 20 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: 20.1 Arrays, 20.2 Array solver

- 21.1 Bitvector semantics and operators,
- 21.2 Solving bit-vector formulas and Term rewriting, 21.3 bit blasting
- 21.4 Lazy bit blasting, 21.5 Modular arithmetic
- Lecture 21 slides
- Suggested reading : Decision Procedures, chapter 6

- 22.1 Nelson-Oppen method, 22.2 Correctness
- 22.3 implementation of the method
- Lecture 22 slides
- Video: 22.1 Nelson-Oppen method, 22.2 Correctness 22.3 Implementation

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

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

- 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 26 slides
- Coq proof script from the class
- Suggested reading : Coq tutorial
- Suggested reading : Another Coq tutorial

Last modified: ()