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
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 simple quizzes : 24% (2% each)
- Mid semester presentations: 10% (15 min)
- End of semester presentation: 10% (15 min)
- Final: 15% (2 hour) or an additional project
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
| | Group | Problem | Status |
| 1 | Namrita/Debasish | 6.16 | |
| 2 | Smit/Sachin/Sivam | 6.17 | |
| 3 | Vedant/Akshat/Ghaskata | 6.18 | |
SAT solvers
2022-08-18 : Lecture 6 - SAT solver
2022-08-22 : Lecture 7 - SAT solver - Clause handling and storage
2022-08-25 : Lecture 8 - Sat solver - run time Optimizations
- restarts, decision orderings, learned clause deletion, phase saving
- pre(in)-processing
- Lecture 8 slides
- Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5
-
Video:
Runtime choices,
- Assignment 2: Problems 8.11-13 in the slides, Due date : Lecture 12
- Each group will do one problem! Problem Assignments
| | Group | Problem | Status |
| 1 | Namrita/Subhasish | | |
| 2 | Smit/Sachin/Sivam | | |
| 3 | Vedant/Akshat/Ghaskata | | |
2022-08-29 : Lecture 9 - Binary decision diagrams
2022-09-01 : Lecture 10 - Encoding problems in SAT solvers
Satisfiability modulo theory(SMT) solvers
2022-09-05 : Lecture 11 - Theory of equality and uninterpreted functions (EUF)
2022-09-09 : Lecture 12 - SMT solvers
2022-09-12 : Lecture 13 - Implementing QF_EUF
- 13.1 union-find, 13.2 Union-find in SMT solvers,
- 13.3 Implementing congruence, 13.4 implementing disequalities
- 13.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 13 slides
-
Video:
13.1 Union-find,
13.2 Union-find in SMT solver,
13.3 Congruence,
13.4 Disequality,
13.5 Model generation.
Midterm paper presentations
2022-09-15/19 Presentations
- Please choose a regular paper(full length; contributed)
from
SAT2022 program.
- You can borrow or make your own slides.(Points deducted for poor slides)
- Present to whole class in 20 mins
- Not compulsory for auditing students
- Midterm presentation assignment.
| | Student | Paper | Presentation slot |
| 1 | Smit | Andreas Niskanen, Jeremias Berg and Matti Järvisalo
Incremental Maximum Satisfiability | 2022-09-15T19:05 |
| 2 | Shivam | Markus Anders,SAT Preprocessors and Symmetry | 2022-09-15T19:25 |
| 3 | Sachin | Armin Biere, Md Solimul Chowdhury, Benjamin Kiesl, Marijn Heule and Michael Whalen Migrating Solver State | 2022-09-15T19:45 |
| 4 | Debasish | Lucas Berent, Lukas Burgholzer and Robert Wille
Towards a SAT Encoding for Quantum Circuits | 2022-09-15T20:05 |
| 5 | Namrita | Jakob Bach, Markus Iser and Klemens Böhm, A Comprehensive Study of k-Portfolios of Recent SAT Solvers | 2022-09-22T19:05 |
| 6 | Vedant | Gilles Audemard, Jean Marie Lagniez and Marie Miceli
A New Exact Solver for (Weighted) Max#SAT | 2022-09-22T19:25 |
| 7 | Ghaskata | IntelSAT | 2022-09-22T19:45 |
| 8 | Akshat | | 2022-09-22T20:05 |
2022-09-03 : Lecture 14 - Inside a solver(skipped due to presentations)
Linear arithmetic
2022-09-26 : Lecture 15 - Basics of linear arithmetic
- 15.0 Introduction to linear arithmetic
- 15.1 Fundamental theorem of linear inequality
- 15.2 Satisfiability conditions, 15.3 Linear programming(LP) and duality theorem
- 15.4 Completeness
- Lecture 15 slides
- Suggested reading : Schrijver chapter 7, sections 7.1,7.2(only definitions),7.3,7.4,7.6
-
Video:
15.0 Introduction,
15.1 Fundamental theorem Part 1,
15.1 Fundamental theorem Part 2,
15.2 Satisfiability,
15.3-4 LP and Completeness,
2022-09-29 : Lecture 16 - Simplex for linear rational arithmetic(LRA)
- 16.1 theory of LRA, 16.2 Intro to simplex
- 16.3 Notation for simplex, 16.4 Pivot operation
- 16.5 Incremental simplex(part video), 16.6 Complexity of simplex(no video)
- Lecture 16 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:
16.1-2 Introduction to LRA and Simplex,
16.3 Notation,
16.4 Pivot,
16.5 Incremental,
- Assignment 4: Checking robustness of neural networks using SMT solver. Due date: Last lecture
- 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
2022-10-03 : Lecture 17 - Linear integer arithmetic(LIA)
2022-10-06 : Lecture 18 - Solving LIA
Other theories
2022-10-10 : Lecture 19 - Rational/Integer difference logic (RDL/IDL)
2022-10-13 : Lecture 20 - Theory of arrays
- 20.1 Axioms of arrays, 20.2 implementation and optimizations for arrays
- 20.3 a decidable fragment of quantified array formulas(no videos)
- Lecture 20 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:
20.1 Arrays,
20.2 Array solver
2022-10-17 : Lecture 21 - Theory of bit-vectors (missed lecture; will do makeup)
- 21.1 Bitvector semantics and operators,
- 21.2 Solving bit-vector formulas and Term rewriting, 21.3 bit blasting
- 21.4 Lazy bit blasting, 21.5 Modular arithmetic
- Lecture 21 slides
- Suggested reading : Decision Procedures, chapter 6
ls
2022-10-20 : Lecture 22 - Theory combination
Usage of SMT solvers
2022-10-27 : Lecture 23 - Maximum satisfiability(no videos)
2022-10-31 : Lecture 24 - Proof Generation
Interactive theorem provers
2022-11-03/07 : Lecture 25/26 - Interactive theorem provers
2022-11-06 : Final presentations
| | Student | Paper | Presentation slot |
| 1 | Smit | Andreas Niskanen, Jeremias Berg and Matti Järvisalo
Incremental Maximum Satisfiability | 2022-09-15T19:05 |
| 2 | Shivam | Affine Loop Invariant Generation via Matrix Algebra from CAV 2022. | 2022-11-06T13:45 |
| 3 | Sachin | Proof-Guided Underapproximation Widening for Bounded Model Checking paper from CAV 2022. | 2022-11-06T..:.. |
| 4 | Debasish | Lucas Berent, Lukas Burgholzer and Robert Wille
Towards a SAT Encoding for Quantum Circuits | 2022-09-06T13:17 |
| 5 | Namrita | Shared Certificates for Neural Network Verification. Christian Sprecher, Marc Fischer, Dimitar I. Dimitrov, Gagandeep Singh, Martin Vechev. | 2022-09-06T..:.. |
| 6 | Vedant | First-Order Subsumption via SAT Solving. Jakob Rath, Armin Biere and Laura Kovacs | 2022-11-06T..:.. |
| 7 | Ghaskata | Counting minimal unsatisfiable subset. jaroslav and kuldeep s. Meel | 2022-09-22T19:45 |
| 8 | Akshat | | 2022-09-22T20:05 |
Last modified: ()