CS 433 : Automated Reasoning 2018

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.

Source material

Self-learning backrgound material

Evaluation structure

The presentations will be distributed over the semester. The topics and slots will be floated time to time in the class. And, the participants need to volunteer to present the topics.


The following lecture schedule is tentative


2018-07-17 : Lecture 1 - Introduction to satisfiability problem

2018-07-20 : Lecture 2 - Fol semantics and theories

2018-07-24 : Lecture 3 - Encoding problems into SAT/SMT

SAT solvers

2018-07-27 : Lecture 4 - SAT solver

2018-07-31 : Lecture 5 - Optimizations in SAT solvers

2018-08-03 : Lecture 6 - Encoding problems in SAT solvers

Satisfiability modulo theory(SMT) solvers

2018-08-07 : Lecture 7 - SMT solvers

2018-08-10 : Lecture 8 - Implementing theory of equality and uninterpreted functions (EUF)

2018-08-14 : Lecture 9 - Inside a solver

Theory of linear real arithmetic (LRA)

2018-08-17 : Lecture 10 - Basics of linear arithmetic

2018-08-21 : Lecture 11 - Simplex for LRA

2018-08-24 : Lecture 12 - Other methods for LRA

Theory of linear integer arithmetic (LIA)

2018-08-28 : Lecture 13 - Basics of linear integer arithmetic

2018-08-31/09-04 : Lecture 14/15 - Simplex for LIA

Midterm break

2018-09-07 : (cancelled)

2018-09-11/14 : (Midterm exam week)

2018-09-18 : (cancelled)

2018-09-21 : (holiday)

Other theories

2018-09-25 : Lecture 16 - Rational/Integer difference logic (RDL/IDL)

2018-09-28 : Lecture 17 - Theory of arrays

2018-10-02 : (holiday)

2018-10-05 : Lecture 18 - Theory of bit-vectors

2018-10-09 : Lecture 19 - Theory combination

Usage of SMT solvers

2018-10-12 : Lecture 20 - Oracle

2018-10-16 : Lecture 21 - Proof Generation

2018-10-19 : (holiday)

2018-10-23 : Lecture 22 - Interpolation

Interactive theorem provers

2018-10-26 : (cancelled) due to lack of Coq installations!

2018-10-30/11-02 : Lecture 25/26 - Interactive theorem prover


2018-11-04T10:00-14:00@SIC201 : Lecture 23/24 - Quantifiers in SMT solvers

2018-11-15 9:30-12:30 : Final exam

Student presentation schedule

The potential topics will be announced about a week before the slot. The students are allowed to borrow slides from the internet, authors of the reference, or any other source, with clear citation. However, it is their responsibility that ideas are clearly presented during the presentation. Students are allowed to trade their slots. Please help your colleagues who may be too busy in some week. If you miss your presentation slot, you loose 10%.
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
10Lohith 2018-11-04 Tobias Paxian, Sven Reimer and Bernd Becker. Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT, SAT18
11Sharath 2018-11-04fer Guthmann, Ofer Strichman, Anna Trostanetski. Minimal unsatisfiable core extraction for SMT, FMCAD16
12Teja 2018-11-04 Vijay D'Silva, Daniel Kroening, Mitra Purandare, Georg Weissenbacher. Interpolant Strength, VMCAI 2010

Last modified: ()