**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.

- Book: A First Course in Logic - Shawn Hedman
- Book chapter: The Art of computer programming Section 7.2.2.2 (Beta version) - Donald Kunuth
- Book: Decision Procedures
- Please install Z3 and its python interface before lecture 3
- Z3 installation instructions for Linux and for Windows

- Evaluation Lab: 50% (7 hours)
- Final: 50% (1 hour)

- Introduction, course contents, introduction to SAT/SMT problems
- Introduction to propositional logic (FOL)
- Negation and conjunctive normal form
- Lecture 1 slides

- Using Python interface of Z3, SMT2 file format
- Encoding simple problems into satisfiability problems
- Lecture 2 slides
- Suggested reading : A tutorial on z3py

- CNF(conjunctive normal form), DPLL
- CDCL(conflict-driven clause learning), Learned clause minimization
- Lecture 3 slides(fixed on 2019-04-04)
- Suggested reading : Handbook of Satisfiability (2009), chapter 4.1-4.4

- Lab problems: 2.6,2.7,2.11,2.13 from lecture 2 slides

- 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

- 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

- CDCL(Theory), Theory interface
- QF_EUF(Quantifier-free theory of equality and uninterpreted functions)
- Lecture 6 slides
- Suggested reading: DPLL(T)

- 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.

Last modified: ()