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
For Windows:-
- Make sure python is installed.
- Open the following github link:- https://github.com/Z3Prover/z3.
- Open Releases
- Download z3-4.7.1-x64-win.zip
- Extract it and place the extracted folder to any desired destination.(e.g. C:\z3py\z3-4.7.1-x64-win)
- Now we have to set Environment Variables,
- Go to:- Control Panel > System and Security > System > Advanced system settings
- Select 'Advanced' tab and click on 'Environment Variables'
- In 'System Variable' section select variable with name 'Path' and click Edit button.
- Click on new button and paste the path of the 'bin' folder and press OK. (eg C:\z3py\z3-4.7.1-x64-win\bin)
- Click new in system variable section, write PYTHONPATH in Variable Name and paste the path of 'python' folder(eg C:\z3py\z3-4.7.1-x64-win\bin\python) which is located inside of 'bin' folder in Variable value. Press OK.
- Try to run example.py in the bin\python folder either through IDLE or cmd , it should not throw any error and give an output successfully.
- If the instructions do not work, contact the TA
For Linux:-
- Make sure python is installed.
- Open the following github link:- https://github.com/Z3Prover/z3.
- Open Releases
- Download
z3-4.7.1-x64-ubuntu-16.04.zip (or according to version of your ubuntu)
- Extract it.
- Open terminal and type following commands:-
(replace [BIN_PATH] with path of bin folder and [PYTHON_PATH] With path of python folder)
$export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:[BIN_PATH]
$export PYTHONPATH=[PYTHON_PATH]
Example :-
$export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:~/Downloads/z3-4.7.1-x64-ubuntu-16.04/bin
$export PYTHONPATH=~/Downloads/z3-4.7.1-x64-ubuntu-16.04/bin/python/
-
Try to run example.py in the bin\python folder , it should not throw any error and give an output successfully.
- To prevent resetting of path variables, type following command
gedit ~/.bashrc
Add both of above export lines to the end of file and save
- If the instructions do not work, contact the TA
Evaluation structure
- Programming assignments: 6% 10% 15% 10%
- Online Quizzes : 24% (2% each)
- Mid semester presentation: 10% (15 min)
- Final: 25% (2 hour)
Lectures
Introduction
2020-08-14@18:05 : Lecture 0 - Introduction
- Videos: Intro
- No quiz in the first session.
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
- Z3(no video), Using Python interface of Z3(no video), SMT2 file format
- Encoding simple problems into satisfiability problems
- Lecture 4 slides
- Video: 4.3 SMT2 file format
- Please solve problems 4.3, 4.5-8, 4.14 on Z3 before coming to the class
- In live session, we will do 4.9 and 4.15, and a few others
- Suggested reading : A tutorial on z3py
- Assignment 1: Problems 4.16-4.20 in the slides, Due date : 2020-09-11 (lecture 8)
- Each group will do one problem! Problem Assignments
| | Group | Problem | Status |
| 1 | Sankalp/Parth | 4.16 | submitted |
| 2 | Ravikant/Nikhil/Nitesh | 4.17 | submitted |
| 3 | Yash/Lakshya/Himanshu | 4.18 | submitted |
| 4 | Rohit/Bonela/Afzal | 4.19 | submitted |
| 5 | Dhruv/Anchal/Sreyas | 4.20 | submitted |
SAT solvers
2020-09-01 : Lecture 5 - SAT solver
2020-09-04 : Lecture 6 - Optimizations in SAT solvers
- 2-watched literals, optimal storage, restarts
- decision orderings, learned clause deletion, phase saving
- Lecture 6 slides
- Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5
-
Video:
6.1 2-watched,
6.2 Optimal storage,
6.3 Runtime choices,
- Assignment 2: Problems 6.13-6.16,6.21 in the slides, Due date : 2020-09-18 (lecture 10)
- Each group will do one problem! Problem Assignments
| | Group | Problem | Status |
| 1 | Sankalp/Parth | 6.13(page 32) | |
| 2 | Ravikant/Nikhil/Nitesh | 6.14(page 33) | |
| 3 | Yash/Lakshya/Himanshu | 6.15(page 34) | |
| 4 | Rohit/Bonela/Afzal | 6.16(page 35) | |
| 5 | Dhruv/Anchal/Sreyas | 6.21 (page 49) | |
2020-09-08 : Lecture 7 - Binary decision diagrams
2020-09-11 : Lecture 8 - Encoding problems in SAT solvers
- 8.1 Sat encoding of graph coloring,
, pigeon-hole principle
- 8.2 Encoding cardinality constraints, 8.3 psuedo-boolean constraints(no video)
- 8.4 Solving sudoku and encoding bounded model checking(no video)
- Lecture 8 slides
- Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT
-
Video:
8.1 Encoding problems,
8.2 Cardinality constraints
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
- 11.1 union-find, 11.2 Union-find in SMT solvers,
- 11.3 Implementing congruence, 11.4 implementing disequalities
- 11.5 Model generation (slides are at the end lecture 9)
- Suggested reading: Decision Procedures, chapter 3
- Suggested reading(in depth):
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. (section 4.2 and section 7)
- Lecture 11 slides
-
Video:
11.1 Union-find,
11.2 Union-find in SMT solver,
11.3 Congruence,
11.4 Disequality,
11.5 Model generation.
2020-09-25 : Lecture 12 - Inside a solver
Linear arithmetic
2020-09-29 : Lecture 13 - Basics of linear arithmetic
- 13.0 Introduction to linear arithmetic
- 13.1 Fundamental theorem of linear inequality
- 13.2 Satisfiability conditions, 13.3 Linear programming(LP) and duality theorem
- 13.4 Completeness
- Lecture 13 slides
- Suggested reading : Schrijver chapter 7, sections 7.1,7.2(only definitions),7.3,7.4,7.6
-
Video:
13.0 Introduction,
13.1 Fundamental theorem Part 1,
13.1 Fundamental theorem Part 2,
13.2 Satisfiability,
13.3-4 LP and Completeness,
2018-10-02 : (Pre-midterm gap)
Midterm paper presentations
2020-10-10 Presentations
- Please choose a regular paper(full length; contributed)
from
SAT2020 program.
- You can borrow or make your own slides.(Points deducted for poor slides)
- Present to whole class in 15 mins
- Not compulsory for auditing students
- Midterm presentation assignment.
| | Group | Paper | Presentation slot |
| 1 | Sankalp | Equivalence Between Systems Stronger Than Resolution. Bonet, M. L., & Levy, J. | 13:00 |
| 2 | Ravikant | Designing New Phase Selection Heuristics. Arijit Shaw, Kuldeep S. Meel | 13:20 |
| 3 | Nikhil | Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. Martin Jonas and Jan Strejcek. | 13:40 |
| 4 | Yash | On CDCL-Based Proof Systemswith the Ordered Decision Strategy by Nathan Mull, ShuoPang, and Alexander Razborov. | 14:00 |
| 5 | Lakshya | Positional Games and QBF: The Corrective Encoding. Valentin Mayer-Eichberger and Abdallah Saffidine. | 14:20 |
| 6 | Himanshu | Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles. Matthew Anderson, Zongliang Ji, and Anthony Yang Xu | 14:40 |
| 7 | Rohit | Sorting Parity Encodings by Reusing Variables, Leroy Chew and Marijn Heule | 15:00 |
| 8 | Afzal | SAT-Based Encodings for Optimal Decision Trees with Explicit Paths. MikolᨠJanota, António Morgado | 15:20 |
| 9 | Dhruv | On Weakening Strategies for PB Solvers. Daniel Le Berre, Pierre Marquis, Romain Wallon | 15:40 |
| 10 | Sreyas | On the Effect of Learned Clauses on Stochastic Local Search. Jan-Hendrik Lorenz, Florian Wörz | 16:00 |
| 11 | Nitesh | Reproducible Efficient Parallel SAT Solving | 16:20 |
| 12 | Bonela | Lower bound on DNNF Encodings of Pseudo-Boolean Constraints. Alexis de colnet | 16:40 |
Linear arithmetic (contd.)
2020-10-02 : Lecture 13 - Simplex for linear rational arithmetic(LRA)
- 14.1 theory of LRA, 14.2 Intro to simplex
- 14.3 Notation for simplex, 14.4 Pivot operation
- 14.5 Incremental simplex(part video), 14.6 Complexity of simplex(no video)
- Lecture 14 slides
- Suggested reading : Decision Procedures, section 5.1-5.2
- Suggested reading (in depth) : Schrijver chapter 11, sections 11.1,11.2 (whole chapter is worth reading!!)
-
Video:
14.1-2 Introduction to LRA and Simplex,
14.3 Notation,
14.4 Pivot,
14.5 Incremental,
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)
- 18.1 Difference Logic, Difference bound matrix, 18.2 Tightness
- 18.3 Octagonal constraints, Octagonal difference bound matrix(ODBM), 18.4 ODBM tightness
- Lecture 18 slides
- Suggested reading : Slides are developed from papers and source codes that are cited in the slides.
-
Video:
18.1 RDL,
18.2 Canonical,
18.3 Octagonal,
18.4 Octagonal Canonical,
- Assignment 4: Checking robustness of neural networks using SMT solver. Due date: 2020-11-20
- Find a trained neural network that classifies images and contains only ReLu and ArgMax non-linear neurons
- Using SMT solver, find the maximum perturbation (pixles altered upto a bound) on each training image such that the classification of the image is not changed
- All groups will do same problem!
2018-10-30 : (Holiday)
2020-11-03 : Lecture 19 - Theory of arrays
- 19.1 Axioms of arrays, 19.2 implementation and optimizations for arrays
- 19.3 a decidable fragment of quantified array formulas(no videos)
- Lecture 19 slides
- Suggested reading : L. Moura, N. Bjorner, Generalized, Efficient Array Decision Procedures.
FMCAD09 (section 2-4)
- Suggested reading : Decision Procedures, chapter 7
- Suggested reading : Aaron R. Bradley, Zohar Manna, Henny B. Sipma: What is Decidable About Arrays? VMCAI 2006
-
Video:
19.1 Arrays,
19.2 Array solver
2020-11-06 : Lecture 20 - Theory of bit-vectors (no videos)
- 20.1 Bitvector semantics and operators,
- 20.2 Solving bit-vector formulas and Term rewriting, 20.3 bit blasting
- 20.4 Lazy bit blasting, 20.5 Modular arithmetic
- Lecture 20 slides
- Suggested reading : Decision Procedures, chapter 6
ls
2020-11-10 : Lecture 21 - Theory combination
Usage of SMT solvers
2020-11-13 : Lecture 22 - Maximum satisfiability(no videos)
2020-11-17/20 : Lecture 23 - Model counting (invited lecture)
- By Prof. Supratik Chakraborty
(Uncovered topics this year) - (23-24 Proofs and Interpolation, 25-26 quantifiers in SMT and QBF)
Interactive theorem provers
2020-11-17/20 : Lecture 27/28 - Interactive theorem provers
- Please bring a laptop in the class with Coqide installed.
- Coq syntax, tactics, basic type system, proof scripts, proof terms
- Boolean reasoning, Predicate logic, Equality, Inductive types, Fixedpoints
- Lecture 27 slides
- Suggested reading : Coq tutorial
- Suggested reading : Another Coq tutorial
(2020-11-26) : Final exam (15:00-16:30 Part1 and 17:00-18:30 Part2)
Last modified: ()