SAT@IIT Mandi 2019
Instructor : Ashutosh Gupta
Timings : 18:00-22:00
Venue : A1-3
TA : Priyanka Tiwari
The course focuses on the design and implementation of algorithms (solvers) for proving/disproving validity of statements in propositional or first-order logics. These solvers have important applications in the area of verification and testing of software, and many others. The problems of proving validity are inherently hard and there are no known provably efficient algorithms. However, we may have efficient heuristics that may solve some interesting instances of the problems. The course is about the heuristics.
Source material
For Windows:-
- Make sure python3 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 python3 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
- Evaluation Lab: 50% (7 hours)
- Final: 50% (1 hour)
Lectures
Introduction
2019-03-25T18:00 : Lecture 1 - Introduction to satisfiability problem and propositional logic
- Introduction, course contents, introduction to SAT/SMT problems
- Introduction to propositional logic (FOL)
- Negation and conjunctive normal form
- Lecture 1 slides
2019-03-26T18:00 : Lecture 2 - Encoding problems into satisfiability problem
SAT solvers
2019-03-27T18:00 : Lecture 3 - SAT solver
2019-03-27T20:00 : Lab 1 - Familiarizing with Z3 SAT solver and python (2 hours)
- Lab problems: 2.6,2.7,2.11,2.13 from lecture 2 slides
2019-03-28T18:00 : Lecture 4 - Optimizations in SAT solvers
- 2-watched literals, restarts, decision orderings
- learned clause deletion, pre-processing
- Lecture 4 slides
- Suggested reading : Handbook of Satisfiability, chapter 4.4.2-4.5.5
2019-03-28T20:00 : Lab 2 - Encoding simple problems into SAT (2 hours)
2019-03-29T19:30 : Lecture 5 - Encoding problems in SAT solvers
- 2-SAT problem
- Sat encoding of graph coloring, pigeon-hole principle
- Encoding cardinality constraints, psuedo-boolean constraints
- Solving sudoku
- Lecture 5 slides
- Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT
SMT solvers
2019-03-30T18:00 : Lecture 6 - SMT solvers
- CDCL(Theory), Theory interface
- QF_EUF(Quantifier-free theory of equality and uninterpreted functions)
- Lecture 6 slides
- Suggested reading: DPLL(T)
2019-03-30T20:00 : Lab 3 - Evaluating perfromance of SAT solvers (2 hours)
- Prob 1: Implement nxn magic square in Z3. And plot the time to solve the problem
- Prob 2: Implement graph coloring in Z3. Generate a random graph for n nodes and m edges. Plot coloring time for first k edges with d colors. Plot time taken to color. Choose suitable n, m, and d.
- Prob 3: In prob 2, generate several random graphs and find the smallest k for each graph such that the coloring is unsatisfiable for first k edges. Give average of k.
Evaluation
2019-03-31T14:00 : Evaluation lab - Encoding an interesting problem (4 hours)
2019-04-05T18:00: Exam (1 hour)
Last modified: ()