Satisfiability Modulo Theories

Report
Satisfiability Modulo Theories
(An introduction)
Magnus Madsen
Todays Talk
What are SMT solvers?
How are they used in practice?
Motivation
Find  and  s.t.:
 ≥3∧  ≤0∨ ≥0
Knowledge of
prop. logic
 ≥3∧ ≤0 ∨  ≥3∧ ≥0
Knowledge of
integers
 =3∧ =0
Solution
Knowledge of
integers
What is SMT?
Satisfiability
Modulo
+
Theories
What is a SMT instance?
A logical formula built using
– negation, conjunction and disjuction
k-SAT
• e.g.  ∧  ∨ 
• e.g.  ∨ ¬ ∨  ∧ ¬ ∨ ¬ ∨  ∧  ∨  ∨ 
theory of
theory of
– theory
bitwise specific operators
integers
operators
• e.g.  ≤ 5,  ≠ 
• e.g.  ⊕  ⊕  = 
• e.g.   = () ∧ (  ) ≠ (  )
theory of
uninterpreted
functions
Recall k-SAT
The Boolean SATisfiability Problem:
 ∨ ¬ ∨  ∧ ¬ ∨ ¬ ∨  ∧  ∨  ∨  ∧ ⋯
clause
literal or
negated literal
• 2SAT is solveable in polynomial time
• 3SAT is NP-complete (solveable in exponential
time)
Q: Why not
encode every
formula in SAT?
Graph Problems:
• Shortest-Path
• Minimum Spanning Tree
Optimization:
• Max-Flow
• Linear Programming
(just to name a few)
A: Theory
solvers have
very efficient
algorithms
Q: But then,
Why not get rid
of the SAT
solver?
A: SAT solvers
are very good at
case analysis
Formula
 ≥3∧  ≤0∨ ≥0
SMT Solver
 ≥3∧ ≤0
∧ ∨
 ≥3∧ ≥0
SAT
NO
YES
∧
∧
Theory
NO
add clause: ¬  ∧ 
YES
=3
=0
Important Properties
• Efficiency of both SAT and Theory solver!
• SAT Solver
– Incremental (supports adding new clauses)
• Theory Solver
– Ability to construct blocking clauses
– Ability to create so-called "theory lemmas"
Theories
Theory of:
– Difference Arithemetic
– Linear Arithmetic
– Arrays
– Bit Vectors
– Algebraic Datatypes
– Uninterpreted Functions
SMT-LIB
• A modeling language for SMT instances
– A declarative language with Lisp-like syntax
– Defines common/shared terminology
• e.g. LRA = Closed linear formulas in linear real
arithmetic
• e.g. QF_BC = Closed quantifier-free formulas over the
theory of fixed-size bitvectors.
– http://www.smtlib.org/
Example 1
=∧=
Solution
Example 2
Applications
•
•
•
•
•
Dynamic Symbolic Execution
Program Verification
Extended Static Checking
Model Checking
Termination Analysis
See Also: Tapas: Theory Combinations and Practical Applications
Dynamic Symbolic Execution
• combines dynamic and symbolic execution
– step 1: execute the program recording the
branches taken and their symbolic constraints
– step 2: negate one constraint
– step 3: solve the constraints to generate new
input to the program (e.g. by using a SMT solver)
– step 4: if a solution exists then execute the
program on the new input
Program Path
Negate ¬3
¬1
2
¬3
4
Run SMT
Solver
New Program Path
¬1
2
3
5
Example: Greatest Common Divisor
Original program
SSA unfolding
int gcd(int x, int y) {
while (true) {
int m = x % y;
if (m == 0) return y;
x = y;
y = m;
}
}
int gcd(int x0, int y0) {
while (true) {
int m0 = x0 % y0;
assert(m0 != 0)
if (m0 == 0) return y0;
x1 = y0;
y1 = m0;
int m1 = x1 % y1;
assert(m1 == 0)
if (m1 == 0) return y1;
}
}
int result = gcd(2, 4)
Collecting Constraints
Collected constraints
SSA unfolding
int result = gcd(2, 4)
int gcd(int x0, int y0) {
while (true) {
int m0 = x0 % y0;
assert(m0 != 0)
if (m0 == 0) return y0;
x1 = y0;
y1 = m0;
int m1 = x1 % y1;
assert(m1 == 1)
if (m1 == 0) return y1;
}
}
(assert (= m0 (mod x0 y0)))
(assert (not (= m0 0)))
(assert
(assert
(assert
(assert
(=
(=
(=
(=
x1
y1
m1
m1
y0))
m0))
(mod x1 y1)))
0))
(assert (not (= m1 0)))
Computing a new path
int gcd(int x, int y) {
while (true) {
int m = x % y;
if (m == 0) return y;
x = y;
y = m;
}
Iteration 1: x =
}
Iteration 2: x =
2&y=3
3&y=2
Iteration 3: x = 2 & y = 1
Solution:
x = 2 and y = 3
Program Verification
int binary_search(int[] arr, int low, int height, int key) {
assert(low > high || 0 <= < high);
while (low <= high) {
// Find middle value
int mid = (low + high) / 2;
assert(0 <= mid < high);
Assertion Violation:
int val = arr[mid];
low = 230, high = 230+1
// Refine range
if (key == val) return mid;
if (val > key)
low = mid + 1;
else
high = mid – 1;
}
return -1;
}
SMT Solvers
• Z3
– Microsoft Research
• MathSAT5
– University of Trento
• CVC4
– New York University
• Many more
SMT-COMP
• A yearly competition between SMT solvers
Z3
Research Directions in SMT
• Improving the efficiency of SAT/Theory solvers
• Improving the interplay between the SAT
solver and the theory solver
– e.g. "online" solvers (partial truth assignment)
• Developing solvers for new theories
• Combining different theories
With Thanks to Evan Driscoll
References
• Satisfiability Modulo Theories: Introduction
and Applications
– Leonardo De Moura & Nikolaj Bjørner
• Tapas: Theory Combinations and Practical
Applications
– Leonardo De Moura & Nikolaj Bjørner
• Z3 Tutorial Guide
– http://rise4fun.com/z3/tutorial/guide
Summary
Satisfiability Modulo Theory (SMT):
– constraint systems involving SAT + Theory
SMT solvers combine the best of:
– SAT solvers and theory solvers
SMTs have applications in program analysis
More Work To Be Done?

similar documents