CS 433 : Automated Reasoning 2021
Instructor : Ashutosh Gupta
Mode of instruction : recorded videos on youtube, weekly release of slides;
two lectures each week, one online quiz every week.
Timings : Tuesday and Friday 19:00-20:25 (changed; does not conflict with any CS course)
Venue : MSTeams, To join the course team, use team code: y1qiap4
TA : No TA
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 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
2021-07-26T15:05 : Lecture 1 - Introduction (1 hour)
2021-07-29@17:30 : Lecture 2 - Propositional logic
2021-08-03 : Lecture 3 - First order logic
- Background videos from CS228:
14.1 FOL syntax,
14.2 FOL semantics,
15.1 more definitions,
Slides: lec-14,
lec-15
- FOL syntax, semantics, and examples FOL theory
- Lecture 3 slides : 2021-CS228-Theory slides
- FOL theory, axioms, theory examples, and logic fragments (no video)
-
Video:
3.0 Theory ,
3.1 Axioms,
3.2 Theory examples,
2021-08-06 : 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:
Using Z3,
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 : (lecture 8)
- Each group will do one problem! Problem Assignments
SAT solvers
2021-08-10 : Lecture 5 - SAT solver
2021-08-13 : 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 : Lecture 10
2021-08-17 : Lecture 7 - Binary decision diagrams
2021-08-20 : 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
2021-08-24 : Lecture 9 - Theory of equality and uninterpreted functions (EUF)
2021-08-27 : Lecture 10 - SMT solvers
2021-08-31 : 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.
2021-09-03 : Lecture 12 - Inside a solver
Linear arithmetic
2021-09-07 : 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-09-10 : (Holiday)
Midterm paper presentations
2021-10-21 Presentations
- Please choose a regular paper(full length; contributed)
from
SAT2021 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.
| | Student | Paper | Presentation slot |
| 1 | Saavan | Stepan Kochemazov, Alexey Ignatiev and Joao Marques-Silva.
Assessing Progress in SAT Solvers Through the Lens of Incremental SAT | 19:00 |
| 2 | Sahil | Matthieu Py, Mohamed Sami Cherif and Djamal Habet. A Proof Builder for Max-SAT | 19:15 |
| 3 | Aniruddha | Marijn Heule. Chinese Remainder Encoding for Hamiltonian Cycles | 19:30 |
| 4 | Aditya | Shaowei Cai and Xindi Zhang. Deep Cooperation of CDCL and Local Search for SAT | 19:45 |
| 5 | Gurudutta | Weighted Model Counting Without Parameter Variables by Paulius Dilkas and Vaishak Belle | 20:00 |
| 6 | Manan | Efficient Local Search for Pseudo Boolean Optimization: Zhendong Lei, Shaowei Cai, Chuan Luo and Holger Hoos | 20:15 |
| 7 | Tirthankar | Investigating the Existence of Costas
Latin Square via Satisfiability Testing. Jiwei Jin, Yiqi Lv, Cunjing Ge, Feifei Ma and Jian Zhang | 20:30 |
Linear arithmetic (contd.)
2021-09-24 : Lecture 14 - 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,
2021-09-28 : Lecture 15 - Other methods for LRA
- Fourier-Motzkin
- Ellipsoid method
- Lecture 15 slides
- Suggested reading : Schrijver sections 12.2, 13.1-13.4
-
Video:
15.1 Fourier-Motzkin,
15.2 Ellipsoid method,
15.3 Ellipsoids,
15.4 Ellipsoid method (algorithm),
- 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
2021-10-01 : Lecture 16 - Linear integer arithmetic(LIA)
2021-10-05 : Lecture 17 - Solving LIA
Other theories
2021-10-08 : Lecture 18 - Rational/Integer difference logic (RDL/IDL)
2021-10-12 : 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
2018-10-15 : (Holiday)
2018-10-19 : (Holiday)
2021-10-22 : 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
2021-10-26 : Lecture 21 - Theory combination
Usage of SMT solvers
2021-10-29 : Lecture 22 - Maximum satisfiability(no videos)
Interactive theorem provers
2021-11-02 : Lecture 23 - Interactive theorem provers
2021-11-05 : Lecture 24 - Solving non-linear constraints
2021-11-19 : Final presentations
| | Student | Paper | Presentation slot |
| 1 | Saavan | Reachability Analysis for AWS-Based Networks
, CAV19 | 19:10 |
| 2 | Aditya | SAT-Based Rigorous Explanations for Decision Lists. SAT 2021 | 19:28 |
| 3 | Gurudutta | Logical cryptanalysis with WDsat by Monika Trimoska , Gilles Dequen and Sorina lonica. SAT 2021 | 19:40 |
| 4 | Tirthankar | Jaroslav Bendık. On Decomposition of Maximal Satisfiable Subsets, FMCAD 21 | 20:00 |
| 4 | Sahil | An SMT Encoding of LLVM’s Memory Model for
Bounded Translation Validation. Juneyoung Lee ,Dongjoo Kim, Chung-Kil Hur, and Nuno P. Lopes CAV21 | 2021-11-26 |
| 6 | Aniruddha | Encoding Redundancy for Satisfaction-Driven Clause Learning. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. SAT 2021 | 2021-11-26 |
| 7 | Manan | Visualization by Example. Who Cheng long Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, Isil Dillig. POPL 2020 | 2021-11-26 |
Last modified: ()