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

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

### SAT solvers

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

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