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

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

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

SAT solvers

2019-03-27T18:00 : Lecture 3 - SAT solver

• 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

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)

• prob-sum-to-one.py
• prob-magic-sq-3x3.py
• prob-sudoku.py

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: ()