**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 3 slides : 2022-CS228-Theory slides
- FOL theory, axioms, and theory examples
- 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 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), Learned clause minimization
- Lecture 6 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,

Last modified: ()