Presentation on theme: "Quantifier Instantiation Techniques"— Presentation transcript
Quantifier Instantiation Techniques
for Finite Model Finding in SMT
Andrew Reynolds
,
Cesare
Tinelli
Amit
Goel
, Sava
Krstic
Morgan Deters, Clark Barrett
Satisfiability Modulo Theories (SMT)
•
SMT solvers are powerful tools
–
Used in many formal methods applications
–
Support many
background
theories
•
Arithmetic,
bitvectors
, arrays,
datatypes
, …
–
May generate:
•
Proofs
–
Theorem proving, software/hardware verification
•
Models
–
Failing instances of aforementioned applications
–
Invariant synthesis, scheduling, test case generation
SMT: Limitations
•
SMT solvers effective handling
ground
formulas
–
Fast decision procedures for UF, arithmetic, …
•
Ongoing challenge:
quantified
formulas
–
Heuristic methods for answering “
unsat
”
–
Limited capability of answering “sat”
•
Often will return “unknown” after some effort
Contributions
•
Finite Model Finding in SMT
–
Different from ATP finite model finders:
•
Native support for background (ground) theories
–
Different from SMT solvers:
•
Increased ability to answer “satisfiable”
•
New techniques for:
–
Constructing
good candidate models
–
Efficiently
checking
candidate models
DPLL(T) Architecture
SAT
Solver
Theory
Solvers
Satisfying
assignment
A
for
F
Clauses to add to
F
UNSAT,
proof
SAT,
model
A
is T

Consistent
A
is T

Inconsistent
F
is
sat
Formula
F
F
is
unsat
DPLL(T) Architecture : Challenge
SAT
Solver
Theory
Solvers
Clauses to add to
F
A
is T

Consistent
A
is T

Inconsistent
F
is
sat
Formula
F
F
is
unsat
•
Challenge: What if determining the consistency of
A
is difficult?
•
For quantified formulas, determining consistency is
undecidable
UNSAT,
proof
SAT,
model
Satisfying
assignment
A
for
F
•
If sat assignment contains quantified formula
Q
,
–
Heuristically add instances of
Q
to F
•
Typically based on pattern matching
–
May discover refutation, if right instances are added
Heuristic Instantiation for
Q
SAT
Solver
Theory
Solvers
Instances of
Q
to
add to
F
Consistency of
A
is
unknown
F
is
sat
Formula
F
F
is
unsat
UNSAT,
proof
Satisfying
assignment
A
for
F
SAT,
model
(containing
Q
)
Why Models are Important
SMT
solver
UNSAT
Verification
Condition
for P
Unknown
Manual
Inspection
Candidate
Model
Property P is
verified
(with quantifiers)
Why Models are Important
SMT
solver
UNSAT
Verification
Condition
for P
Unknown
Manual
Inspection
Candidate
Model
Property P is
verified
(with quantifiers)
Concrete
counterexample
for Property P
SAT
Model

Based Approach for Quantifiers
•
Given:
–
Set of
ground formulas
F
–
Set of
universally quantified formulas
Q
•
To determine the satisfiability of
F
Q
,
–
Construct
candidate models
for
Q
, based on
satisfying
assignments
for
F
•
Model

Based Quantifier Instantiation (MBQI)
–
[
Ge
/
deMoura
2009]
DPLL(T) Architecture (Extended)
SAT
Solver
Theory
Solvers
Satisfying
assignment
A
for
F
Clauses to
add
to
F
UNSAT,
proof
A
is
T

Consistent
F
is
sat
Ground
Formulas
F
Candidate
model
M
Model
Verifier
M
is a model
for
Q
Quantified
Formulas
Q
SAT,
model
M
else
else
else
When can we represent/check models for
Q
?
•
Focus of talk
: Finite Model Finding
–
Limited to quantifiers over:
•
Uninterpreted sorts
–
Can represent memory addresses, values, sets, etc.
•
Other
finite sorts
–
Fixed width
bitvectors
,
datatypes
, …
•
Useful in applications:
–
Software/hardware verification
Constructing/Checking Candidate Finite Models
1.
How do we construct good candidate models
M
?
2.
How do we efficiently check if
M
is a model for
Q
?
–
If we fail, which instances do we add to
F
?
Sat assignment
A
for
F
Model
Verifier
Ground Solver
(Finite)
Candidate
model
M
UNSAT,
proof
SAT,
model
M
Instances of
Q
to
add
to
F
F
Q
Constructing Good Candidate Models
•
Navely, to determine whether
M
is model for
Q
:
–
Check if
M
satisfies
all instances
S
of
Q
•
Challenge
:
S
can be very large
–
For
Q
with n variables, domain size d, 
S
 can be O(
d
n
)
•
Solutions
:
–
Find models with small domain sizes
•
Use theory of finite cardinality constraints [CAV 2013]
–
Only consider instances of
Q
that are false in
M
•
Construct
M
such that most instances of
Q
are true
Constructing Good Candidate Models
Constructing Models : Example
d
istinct
(
NewYork
, Boston, Seattle)
travels(person
1
, Boston)
salesman(person
2
)
salesman(person
3
)
person
1
, person
2
, person
3
: Person
NewYork
, Boston, Seattle
: City
salesman: Person
Bool
travels : Person
City
Bool
x
: Person,
y : City.
salesman(x)
travels(
x,y
)
Q
F
Constructing Models : Example
d
istinct
(
NewYork
, Boston, Seattle)
travels(person
1
, Boston)
salesman(person
2
)
salesman(person
3
)
person
1
, person
2
, person
3
: Person
NewYork
, Boston, Seattle
: City
salesman: Person
Bool
travels : Person
City
Bool
x
: Person,
y : City.
salesman(x)
travels(
x,y
)
Q
F
Interpretation of “salesman”:
salesman(person
2
)
≈
,
salesman(person
3
)
≈ T,
salesman( x
1
) ≈
Interpretation of “travels”:
travels(person
1
, Boston
)
≈ T,
travels( x
1
, x
2
)
≈
Model Representation
•
Represent functions/predicates using
defining maps
•
Given sort
S
with domain
V
,
–
A defining map for
f
:
S
…
S
S
is:
•
Set of equations
D
f
of the form
f
(
t
1
, …,
t
n
)
≈
v
, where
–
v
V
–
Each
t
i
is either a unique variable or in
V
•
If
t
1
≈
v
1
and
t
2
≈
v
2
D
f
,
unifiable
with
mgu
s
, then:
–
s
is non

empty
–
t
1
s
≈
v
D
f
for some
v
•
f
(
x
1
, …,
x
n
) ≈
v
D
f
for some
v
Interpretation in Model
•
Interpretation
f
(
t
1
, …,
t
n
) is
v
, where:
–
t
≈
v
D
f
–
t
is m
ost specific generalization of
f
(
t
1
, …,
t
n
)
among LHS in
D
f
•
Guaranteed to exist and be unique
Constructing Models
•
Defining map
D
f
is a union of:
–
Entailed
ground equalities
–
Non

ground equalities
for defining
default
values
•
How to chose default values?
–
Guided by sat assignment for
distinguished elements
•
See how one instance is satisfied, generalize this for all
Constructing Models : Example
d
istinct
(
NewYork
, Boston, Seattle)
travels(person
1
, Boston)
salesman(person
2
)
salesman(person
3
)
person
1
, person
2
, person
3
: Person
NewYork
, Boston, Seattle
: City
salesman: Person
Bool
travels : Person
City
Bool
x
: Person,
y: City.
salesman(x)
travels(
x,y
)
Q
F
•
Instantiate
Q
with distinguished elements
salesman(person
1
)
travels(person
1
,
NewYork
)
D
travels
:
{
travels(person
1
,
NewYork
)
≈ T
travels(person
1
, Boston
)
≈
,
travels( x
1
, x
2
)
≈ T }
Constructing Models : Example
d
istinct
(
NewYork
, Boston, Seattle)
travels(person
1
, Boston)
salesman(person
2
)
salesman(person
3
)
person
1
, person
2
, person
3
: Person
NewYork
, Boston, Seattle
: City
salesman: Person
Bool
travels : Person
City
Bool
x
: Person,
y: City.
salesman(x)
travels(
x,y
)
Q
F
T
salesman(person
1
)
travels(person
1
,
NewYork
)
D
salesman
:
{
salesman(person
2
)
≈
,
salesman(person
3
)
≈ T,
salesman( x
1
) ≈ T }
•
Choose defaults based on distinguished instance
–
Analagous
to Inst Gen Calculus [
Korovin
2008]
Efficiently Checking Candidate Models
Instances of
Q
to
add to
F
•
To check if
M
is a model for
Q
:
–
Naively, add every instance of
Q
to
F
–
Alternatively
,
only add instances that are false in
M
•
Identify sets of instances of
Q
that are equisatisfiable
Checking Candidate Models
SAT,
model
M
(Finite)
Candidate
model
M
Model
Verifier
M
is a
model for
Q
Ground
Solver
F
Q
Checking Candidate Models
d
istinct
(
NewYork
, Boston, Seattle)
travels(person
1
, Boston)
salesman(person
2
)
salesman(person
3
)
person
1
, person
2
, person
3
: Person
NewYork
, Boston, Seattle
: City
salesman: Person
Bool
travels : Person
City
Bool
x
: Person,
y: City.
salesman(x)
travels(
x,y
)
Q
F
salesman(person
1
)
travels(person
1
,
NewYork
)
D
salesman
:
{
salesman(person
2
)
≈
,
salesman(person
3
)
≈ T,
salesman( x
1
) ≈ T }
D
travels
:
{
travels(person
1
,
NewYork
)
≈ T
travels(person
1
, Boston
)
≈
,
travels( x
1
, x
2
)
≈ T }
Q
[person
1
,
NewYork
]
Q
[person
1
, Boston]
Q
[person
1
, Seattle]
Q
[person
2
,
NewYork
]
Q
[person
2
, Boston]
Q
[person
2
, Seattle]
Q
[person
3
,
NewYork
]
Q
[person
3
, Boston]
Q
[person
3
, Seattle]
Q
[person
1
,
NewYork
]
Q
[person
1
, Boston]
Q
[person
1
, Seattle]
Q
[person
2
,
NewYork
]
Q
[person
2
, Boston]
Q
[person
2
, Seattle]
Q
[person
3
,
NewYork
]
Q
[person
3
, Boston]
Q
[person
3
, Seattle]
Checking Candidate Models
d
istinct
(
NewYork
, Boston, Seattle)
travels(person
1
, Boston)
salesman(person
2
)
salesman(person
3
)
person
1
, person
2
, person
3
: Person
NewYork
, Boston, Seattle
: City
salesman: Person
Bool
travels : Person
City
Bool
x
: Person,
y: City.
salesman(x)
travels(
x,y
)
Q
F
salesman(person
1
)
travels(person
1
,
NewYork
)
D
salesman
:
{
salesman(person
2
)
≈
,
salesman(person
3
)
≈ T,
salesman( x
1
) ≈ T }
D
travels
:
{
travels(person
1
,
NewYork
)
≈ T
travels(person
1
, Boston
)
≈
,
travels( x
1
, x
2
)
≈ T }
true
false
true
true
true
Enhancement: Heuristic Instantiation
•
Idea:
–
First see if instantiations based on heuristics exist
–
If not, resort to model

based instantiation
•
May lead to:
–
Discovering easy conflicts, if they exist
–
Arriving at model faster
•
Instantiations rule out spurious models
Experiments
•
DVF Benchmarks
–
Taken from verification tool DVF used by Intel
–
Both SAT/UNSAT benchmarks
•
SAT benchmarks generated by removing necessary
pf
assumptions
–
Many theories: UF, arithmetic, arrays,
datatypes
–
Quantifiers only over free sorts
•
Memory addresses, Values, Sets, …
•
TPTP Benchmarks
•
Isabelle Benchmarks
–
Provable and
unprovable
goals, contains some arithmetic
Results: DVF
cvc4 :
•
f : finite model
•
i
: heuristic
•
m
: model

based
SAT
german
refcount
agree
apg
bmk
Total
Time
#
45
6
42
19
37
149
z3
45
1
0
0
0
46
8.1
cvc4+i
2
0
0
0
0
2
0.0
cvc4+f
45
6
42
18
36
147
1413.1
cvc4+fi
45
6
42
19
36
148
1333.9
cvc4+fm
45
6
42
19
37
149
605.4
cvc4+fmi
45
6
42
19
37
149
409.8
UNSAT
german
refcount
agree
apg
bmk
Total
Time
#
145
40
488
304
244
1221
z3
145
40
488
304
244
1221
31.0
cvc4+i
145
40
484
304
244
1217
21.3
cvc4+f
145
40
476
298
242
1201
7512.2
cvc4+fi
145
40
488
302
244
1219
1181.4
cvc4+fm
145
40
471
300
242
1198
6949.7
cvc4+fmi
145
40
488
302
244
1219
1185.0
•
cvc4
with finite
model finding (
cvc4+f)
•
Effective for answering sat
•
Using
heuristic instantiation,
solves 4
unsat
that cvc4 cannot
Results: TPTP
•
Using techniques described in this work:
–
Of 1995 satisfiable benchmarks:
•
Paradox solves 1305
•
iProver
solves 1231
•
cvc4 solves 1109 (with model

based instantiation)
–
Includes 2 problems with rating 1.0
–
Of 12568 unsatisfiable benchmarks:
•
z3 solves 5934
•
cvc4 solves 3028 (with model

based+heuristic
instantiation)
–
Orthogonal, 282 cannot be solved by z3
•
Placed 3
rd
in FNT (non

theorem) division of CASC 24
Results : TPTP
•
Model

Based Instantiation is often essential
–
Solves where
exh
. instantiation requir�e 1 billion instances
Results: Isabelle
•
cvc4+fmi solves 244
unsat
that z3 cannot, 164
that cvc4 cannot
UNSAT
Arrow
FFT
FTA
Hoare
NS
QEP
SNorm
TwoSq
TypeSafe
Total
z3
261
224
765
497
135
236
240
451
325
3134
cvc4+i
199
217
682
456
97
244
231
486
239
2851
cvc4+f
120
99
298
214
36
105
84
316
132
1404
cvc4+fm
102
91
330
246
26
117
80
310
128
1430
cvc4+fmi
155
170
467
328
42
161
97
411
188
2019
SAT
Arrow
FFT
FTA
Hoare
NS
QEP
SNorm
TwoSq
TypeSafe
Total
z3
3
19
24
46
10
49
1
17
11
180
cvc4+i
0
9
0
0
0
0
0
8
0
17
cvc4+f
22
138
172
153
56
79
12
59
69
760
cvc4+fm
26
139
171
151
49
80
12
59
69
756
cvc4+fmi
26
151
174
159
60
81
12
60
78
801
cvc4 :
•
f : finite model
•
i
: heuristic
•
m
: model

based
Summary
•
CVC4 with finite model finding:
–
Constructs “good” candidate models
–
Incorporates various instantiation strategies
•
Model

based quantifier instantiation
•
Heuristic instantiation (E

matching)
–
Increased ability to answer “
satisfiable
”
•
Publicly available:
http://cvc4.cs.nyu.edu/web/
Further Work
•
Further work:
–
Would like to show:
•
Finite model completeness
•
Refutational
completeness for certain fragments
–
Improved algorithm for checking candidate models
–
Apply similar techniques to:
•
Bounded integer quantification
•
Datatypes
, strings with bounded length
Thank you
•
Questions?