Transcript ppt - Microsoft Research

A Randomized Satisfiability Procedure for
Arithmetic and Uninterpreted Function Symbols
Sumit Gulwani
George Necula
EECS Department
University of California, Berkeley
Introduction
• Problem
– Check satisfiability of conjunction of literals
– Example: x = 2y+3 Æ F(x-3)  F(2y)
– Application: program verification
• Existing algorithms
– Linear arithmetic: Gaussian elimination, Simplex
– Uninterpreted function terms: congruence closure
– Combination: Nelson-Oppen, Shostak
• Our proposal
– A randomized algorithm
– We hope to gain: simplicity and efficiency
2
Outline
•
•
•
•
Linear arithmetic
Retracting assumptions
Extension to uninterpreted function symbols
Experimentation
3
Algebraic Interpretation of Satisfiability
1 : (z = x+y) Æ (x = y) Æ (z  0)
2 : (z = x+y) Æ (x = y) Æ (z  2x)
• 1 is satisfiable. For e.g. x=1, y=1, z=2
• 2 is not satisfiable since (z=x+y) Æ (x=y) ) (z=2x)
• Can we "test" the satisfiability of these formulae
with low error probability?
4
Geometric Interpretation of Satisfiability
1 : (z = x+y) Æ (x = y) Æ (z  0)
2 : (z = x+y) Æ (x = y) Æ (z  2x)
L
L
P
R1: z = 0
R2: z = 2x
Line L: solution space for (z = x+y) Æ (x = y)
IDEA: If we choose points randomly on L, we can
easily tell that L ) R1 and L ) R2
5
Overview of the Algorithm
1. Generate random assignments that satisfy all
equality literals
–
–
–
We do this incrementally
Start with a set of completely random assignments
Adjust them to satisfy each equality literal one by one
2. Test them on disequality literals
–
If the random assignments satisfy e1 = e2, then the
formula …. Æ e1  e2 Æ …. is unsatisfiable
6
Adjust Operation: Algebraic Interpretation
Notation
• Sample S = collection of assignments
• S ² g = 0 means all assignments in S satisfy g=0
Properties of S’ = Adjust(S, e=0)
1. If S ² g=0, then S’ ² g=0
2. S’ ² e=0
3. If S’ ² g’=0, then 9 g (S ² g=0 and g=0 Æ e=0 ) g’=0)
–
S’ satisfies exactly one more linearly independent
relationship satisfied by S
7
Adjust Operation: Geometric Interpretation
Algorithm to obtain S’ = Adjust(S, e=0)
S4
S1
.
S’3
S3
S’2

S’1
S2
• Assignments = points
• Adjust = projection onto the hyperplane
represented by an equality literal
• S’ satisfies e=0 and all relationships satisfied by S
8
The Satisfiability Procedure
• IsSatisfiable() =
– let  be
– S Ã R, where R is a random sample
– for i = 1 to k:
• S Ã Adjust(S,ei=0)
9
The Satisfiability Procedure
• IsSatisfiable() =
– let  be
– S Ã R, where R is a random sample
– for i = 1 to k:
• if S ² ei+c=0 for some c  0, then return Unsatisfiable
• else if S ² ei=0 then S Ã Adjust(S,ei=0)
– for j = 1 to m:
• if S ² ej’ = 0, then return Unsatisfiable
– return Satisfiable
10
Completeness Theorem
• “If IsSatisfiable() returns true, then  is
satisfiable”
• Proof:
– The final sample satisfies all the equality literals and the
disequality literals in the formula.
11
Soundness Theorem
• “If  is satisfiable, then IsSatisfiable() returns
true with high-probability”
• Error probability ·
–
–
–
–
m: #disequalities
|F|: size of set from which random values are chosen
r: #assignments in the initial sample R
k: #equality literals
• If m = k = 10, |F| ¼ 232, r = 15,
then error probability ·
12
Complexity
r = #assignments in the initial sample R
n = #variables
k = #equality literals
• Each adjust operation has cost O(nr)
• Number of adjust operations = O(k)
• Total cost = O(nkr) = O(nk2)
13
Retracting Assumptions: Motivation
• if z=x+y then
if x=y then assert (z=2x)
else assert (x=z-y)
• ) decide satisfiability of (z=x+y) Æ (x=y) Æ (z2x)
and (z=x+y) Æ (xy) Æ (xz-y)
• One easy way to retract is to remember old samples
– Space overhead
14
Retracting Assumptions: Unadjust Operation
S4
S1

S’3
S3
S’2
S’1
S’ = Adjust(S, e=0)
S2
• Remember 
• Unadjust(S’,e=0) = S’ [ { }
• (S’ [ { }) ² e=0 iff S ² e=0
15
Uninterpreted Function Symbols
• Use Ackerman transformation
– Replace uninterpreted term e with new variable Ve
– For any F(e) and F(e’) add if Ve = Ve’ then VF(e) = VF(e’)
• Example
(x=y) Æ (f(x)=u) Æ (f(y)=w)
!
(x=y) Æ (v1 =u) Æ (v2=w) Æ (if x=y then v1 = v2)
• Implementation
– After adjusting for an equality, check if any of the
conditional literals require adjustment.
16
Experimental Results
Example
Arithdense
Arithsparse
Bothdense
Bothsparse
Uf
#equalities 26
25
20
50
35
#adjusts
25
14
29
42
72
#points
30
20
40
50
40
Rand (ms)
2.3
1.3
3.4
7.5
9.6
ICS (ms)
386.4
84.8
37.0
73.9
23.1
ICS/Rand
168
65
11
10
2.5
ICS = Integrated Canonizer and Solver
17
Comparison with Shostak’s Algorithm
• Symbolic manipulation vs. expression evaluation
• Shostak’s solver » adjust operation
• Shostak’s canonizer » probabilistic canonical form
18
Conclusion and Future Work
• Randomization can help achieve simplicity and
efficiency at the expense of making soundness
probabilistic
• Generate proofs
• Can we extend these ideas to other theories –
inequalities, arrays?
• Integrate symbolic techniques with randomized
ones
19