SAT@IIT Mandi 2019

Instructor : Ashutosh Gupta

Timings : 18:00-22:00
Venue : A1-3
TA : Priyanka Tiwari

The course focuses on the design and implementation of algorithms (solvers) for proving/disproving validity of statements in propositional or first-order logics. These solvers have important applications in the area of verification and testing of software, and many others. The problems of proving validity are inherently hard and there are no known provably efficient algorithms. However, we may have efficient heuristics that may solve some interesting instances of the problems. The course is about the heuristics.

Source material

Evaluation structure



2019-03-25T18:00 : Lecture 1 - Introduction to satisfiability problem and propositional logic

2019-03-26T18:00 : Lecture 2 - Encoding problems into satisfiability problem

SAT solvers

2019-03-27T18:00 : Lecture 3 - SAT solver

2019-03-27T20:00 : Lab 1 - Familiarizing with Z3 SAT solver and python (2 hours)

2019-03-28T18:00 : Lecture 4 - Optimizations in SAT solvers

2019-03-28T20:00 : Lab 2 - Encoding simple problems into SAT (2 hours)

2019-03-29T19:30 : Lecture 5 - Encoding problems in SAT solvers

SMT solvers

2019-03-30T18:00 : Lecture 6 - SMT solvers

2019-03-30T20:00 : Lab 3 - Evaluating perfromance of SAT solvers (2 hours)


2019-03-31T14:00 : Evaluation lab - Encoding an interesting problem (4 hours)

2019-04-05T18:00: Exam (1 hour)

Last modified: ()