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.
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: ()