CS 433 : Automated Reasoning 2022

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.

Source material

Self-learning background material

Software

  • Please install Z3 and its python interface before second week
  • Evaluation structure

    May change later.

    Lectures

    Introduction

    2022-07-28T08:30 : Lecture 1 - Introduction (1 hour)

    2022-07-29@17:30 : Lecture 2 - Propositional logic

    2022-08-04 : Lecture 3 - First order logic

    2022-08-08 : Lecture 4 - Theory

    2022-08-11 : Lecture 5 - Encoding problems into SAT/SMT

    SAT solvers

    2022-08-10 : Lecture 6 - SAT solver

    2022-08-10 : Lecture 7 - SAT solver - Clause minimization


    Last modified: ()