CS 433 : Automated Reasoning 2020

Instructor : Ashutosh Gupta

Mode of instruction : weekly release of recorded videos and slides; a weakly interactive session followed by an online quiz.
Timings : Inteactive session at 21:00 on Fridays
Venue : MSTeams, To join the course team, use team code: inff8lm (feel free to attend even if not taking the course)
TA : Kalyani Dole (PhD) (163050022 _at_ iitb . ac . in), Isha Pandey
Quizes : Quiz Portal (Login via CSE LDAP or special accounts)

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

    Lectures

    Introduction

    2020-08-14@18:05 : Lecture 0 - Introduction

    2020-08-18 : Lecture 1 - Overview of logic

    2020-08-21 : Lecture 2 - Propositional logic

    2020-08-25 : Lecture 3 - First order logic

    2020-08-28 : Lecture 4 - Encoding problems into SAT/SMT

    SAT solvers

    2020-09-01 : Lecture 5 - SAT solver

    2020-09-04 : Lecture 6 - Optimizations in SAT solvers

    2020-09-08 : Lecture 7 - Binary decision diagrams

    2020-09-11 : Lecture 8 - Encoding problems in SAT solvers

    Satisfiability modulo theory(SMT) solvers

    2020-09-15 : Lecture 9 - Theory of equality and uninterpreted functions (EUF)

    2020-09-18 : Lecture 10 - SMT solvers

    2020-09-22 : Lecture 11 - Implementing QF_EUF

    2020-09-25 : Lecture 12 - Inside a solver

    Linear arithmetic

    2020-09-29 : Lecture 13 - Basics of linear arithmetic

    Midterm paper presentations

    2020-10-10 Presentations

    Linear arithmetic (contd.)

    2020-10-02 : Lecture 13 - Simplex for linear rational arithmetic(LRA)

    2020-10-16 : Lecture 15 - Other methods for LRA

    2020-10-20 : Lecture 16 - Linear integer arithmetic(LIA)

    2020-10-23 : Lecture 17 - Solving LIA

    Other theories

    2020-10-27 : Lecture 18 - Rational/Integer difference logic (RDL/IDL)

    2020-10-30 : Lecture 19 - Theory of arrays

    2020-11-03 : Lecture 20 - Theory of bit-vectors

    2020-11-06 : Lecture 21 - Theory combination


    Last modified: ()