### Conflict - Leonardo de Moura

```Model-Driven Decision Procedures
for Arithmetic
SYNASC 2013
Leonardo de Moura
Microsoft Research
Logic Engines as a Service
SAGE
3
Satisfiability
Solution/Model
2
+
2
< 1   > 0.1
2 +  2 < 1   > 1
=
7
8
unsat, Proof
Is execution path P feasible?
SAGE
sat,  =
1
,
8
Is assertion X violated?
W
I
T
N
E
S
S
Is Formula F Satisfiable?
The RISE of Model-Driven
Techniques
Saturation x Search
Model-finding
Proofs
Proof-finding
Models
SAT
1 ∨ ¬2,
1 = ,
¬1 ∨ 2 ∨ 3,
2 = ,
3
3 =
CNF is a set (conjunction) set of clauses
Clause is a disjunction of literals
Literal is an atom or the negation of an atom
Two procedures
Resolution
Proof-finder
Saturation
DPLL
Model-finder
Search
Resolution
∨ ,  ∨ ¬ ⇒  ∨
, ¬
⇒ unsat
Improvements
Delete tautologies  ∨ ¬ ∨
Ordered Resolution
Subsumption (delete redundant clauses)
∨
…
Resolution: Example
Resolution: Example
Resolution: Example
Resolution: Example
Resolution: Example
Resolution: Problem
Exponential time and space
Unit Resolution
∨ , ¬
⇒

subsumes
∨
DPLL
Split rule

,
, ¬
DPLL = Unit Resolution + Split rule
DPLL
∨ ,
¬ ∨ ,
∨ ,
¬ ∨ ,
∨ ¬,
¬ ∨ ¬,

∨ ¬,
¬ ∨ ¬
DPLL
∨ ,
¬ ∨ ,
∨ ,
¬ ∨ ,
∨ ¬,
¬ ∨ ¬,

∨ ¬,
¬ ∨ ¬
DPLL
∨ ,
,
¬,

¬ ∨ ,
∨ ¬,
¬ ∨ ¬
DPLL
∨ ,
¬ ∨ ,
,
¬,
,

∨ ¬,
¬ ∨ ¬
DPLL
∨ ,
¬ ∨ ,
,
¬,
,

∨ ¬,
∨ ,
¬ ∨ ,
∨ ¬,
¬ ∨ ¬,
¬
¬ ∨ ¬
DPLL
∨ ,
¬ ∨ ,
,
¬,
,

∨ ¬,
∨ ,
¬ ∨ ,
∨ ¬,
¬ ∨ ¬,
¬
¬ ∨ ¬
CDCL: Conflict Driven Clause Learning
DPLL
Resolution
Model
Proof
Linear Arithmetic
Fourier-Motzkin
Proof-finder
Saturation
Simplex
Model-finder
Search
Fourier-Motzkin
1 ≤ ,
1 ≤ ,
≤ 2
≤ 2
1 ≤ 2
Very similar to Resolution
Exponential time and space
Polynomial Constraints
AKA
Existential Theory of the Reals
R
2 − 4 +  2 −  + 8 < 1
− 2 − 2 + 4 > 1
Applications
1. Project/Saturate set of polynomials
2. Lift/Search: Incrementally build assignment :  →
Isolate roots of polynomials  (, )
Select a feasible cell , and assign  some  ∈
If there is no feasible cell, then backtrack
2
4 − 2 + 1
2
+ −1<0
−1>0
1. Saturate
2 − 1

2. Search
(−∞, −)
−
(−, )

(, )

(, ∞)
4 − 2 + 1
+
+
+
+
+
+
+
2 − 1
+
0
-
-
-
0
+

-
-
-
0
+
+
+

4 − 2 + 1

+ −<0
−>0
1. Saturate
2 − 1

(−∞, − )

− (− , ∞)

4 + 2 − 1
+
+
+
−2y − 1
+
0
-
 −
2. Search
(−∞, −)
−
(−, )

(, )

(, ∞)
4 − 2 + 1
+
+
+
+
+
+
+
2 − 1
+
0
-
-
-
0
+

-
-
-
0
+
+
+

4 − 2 + 1

+ −<
−1>0
1. Saturate
2 − 1

(−∞, − )

− (− , ∞)

+  −
+
+
+
−2y − 1
+
0
-
 −
CONFLICT
2. Search
(−∞, −)
−
(−, )

(, )

(, ∞)
4 − 2 + 1
+
+
+
+
+
+
+
2 − 1
+
0
-
-
-
0
+

-
-
-
0
+
+
+
Models
Static x Dynamic
Optimistic approach
Key ideas
Proofs
NLSAT: Model-Based Search
Start the Search before Saturate/Project
We saturate on demand
Model guides the saturation
NLSAT (1)
Two kinds of decision
1. case-analysis (Boolean)
2 + 2 < 1 ∨  <  ∨   > 1
 −
(−∞, −)
−
(−, )

(, )

(, ∞)
4 − 2 + 1
+
+
+
+
+
+
+
2 − 1
+
0
-
-
-
0
+

-
-
-
0
+
+
+
NLSAT (1)
Two kinds of decision
1. case-analysis (Boolean)
Parametric calculus:  ,
Finite basis explanation function
Explanations may contain new literals
They evaluate to false in the current state
NLSAT (2)
Key ideas: Use partial solution to guide the search
Feasible Region
3 + 2 2 + 3 2 − 5 < 0
Starting search
Partial solution:
← 0.5
−4 − 4 +  > 1
What is the core?
2 + 2 < 1
Can we extend it to ?
NLSAT (2)
Key ideas: Use partial solution to guide the search
Feasible Region
3 + 2 2 + 3 2 − 5 < 0
Starting search
Partial solution:
← 0.5
−4 − 4 +  > 1
What is the core?
2 + 2 < 1
Can we extend it to ?
NLSAT (3)
Key ideas: Solution based Project/Saturate
Standard project operators are pessimistic.
Coefficients can vanish!
NLSAT (4)
Key ideas: Lemma Learning
Prevent a Conflict from happening again.
Current assignment
→ 0.75
→ 0.75
Conflict
2 + 2 + 2 < 1
Current assignments does
not satisfy new constraint.
Lemma
−1 <  < 1 ∧  > 2 1 −  2 −  2 ⇒ ⊥
NLSAT (5)
Key ideas: Nonchronological Backtracking
Conflict
=1

=1
The values chosen for  and
are irrelevant.
=
=
Machinery
Multivariate & univariate Polynomials
Basic operations, Pseudo-division,
GCD, Resultant, PSC, Factorization,
Root isolation algorithms, Sturm sequences
Binary rationals

2
Real Algebraic Numbers
Experimental Results (1)
OUR NEW ENGINE
Experimental Results (2)
OUR NEW ENGINE
Other examples
(for linear arithmetic)
Generalizing DPLL to
richer logics
Fourier-Motzkin
X
[McMillan et al 2009]
Conflict Resolution
[Korovin et al 2009]
Other examples
Array Theory by
Axiom Instantiation
X
Lemmas on Demand
For Theory of Array
[Brummayer-Biere 2009]
∀, , :   ≔   =
∀, , , :  =  ∨   ≔   = []
Saturation: successful instances
Polynomial time procedures
Gaussian Elimination
Congruence Closure
MCSat
Model-Driven SMT
Lift ideas from CDCL to SMT
Generalize ideas found in model-driven approaches
Easier to implement
Model construction is explicit
MCSat
≥ 2,
¬ ≥ 1 ∨  ≥ 1 ,
( 2 +  2 ≤ 1 ∨  > 1)
MCSat
≥ 2,
¬ ≥ 1 ∨  ≥ 1 ,
( 2 +  2 ≤ 1 ∨  > 1)
≥2
Propagations
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
( 2 +  2 ≤ 1 ∨  > 1)
≥1
Propagations
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥1
Propagations
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
Boolean Decisions
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1  → 2
Semantic Decisions
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1  → 2
Conflict
We can’t find a value for
s.t. 4 +  2 ≤ 1
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1  → 2
Conflict
We can’t find a value for
s.t. 4 +  2 ≤ 1
Learning that
¬  2 +  2 ≤ 1 ∨ ¬(= 2)
is not productive
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
¬( = 2)
¬  2 +  2 ≤ 1 ∨ ¬( = 2)
Learning that
¬  2 +  2 ≤ 1 ∨ ¬(= 2)
is not productive
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
¬( = 2)  → 3
¬  2 +  2 ≤ 1 ∨ ¬( = 2)
Learning that
¬  2 +  2 ≤ 1 ∨ ¬(= 2)
is not productive
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
“Same” Conflict
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
¬( = 2)  → 3
¬  2 +  2 ≤ 1 ∨ ¬( = 2)
We can’t find a value for
s.t. 9 +  2 ≤ 1
Learning that
¬  2 +  2 ≤ 1 ∨ ¬(= 2)
is not productive
≥ 2,
≥2

( 2 +  2 ≤ 1 ∨  > 1)
¬ ≥ 1 ∨  ≥ 1 ,
≥1
≥ 1 2 + 2 ≤ 1  → 2
Conflict
2 + 2 ≤ 1

→2
−1 ≤ ,  ≤ 1
¬( 2 +  2 ≤ 1) ∨  ≤ 1
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
≤1
¬( 2 +  2 ≤ 1) ∨  ≤ 1
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
≤1
¬( 2 +  2 ≤ 1) ∨  ≤ 1
Conflict
¬  ≥ 2 ∨ ¬( ≤ 1)
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
¬( 2 +  2 ≤ 1) ∨  ≤ 1
Learned by resolution
¬  ≥ 2 ∨ ¬( 2 +  2 ≤ 1)
MCSat
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 ¬( 2 +  2 ≤ 1)
¬  ≥ 2 ∨ ¬( 2 +  2 ≤ 1)
¬( 2 +  2 ≤ 1) ∨  ≤ 1
MCSat: FM Example
− +  + 1 ≤ 0  → 0
− +  + 1 ≤ 0,
≡
+ 1 ≤ ,
− ≤0
− ≤0
→0
→ 0,
≤
1 ≤ ,
≤0
We can’t find a value of
→0
MCSat: FM Example
− +  + 1 ≤ 0  → 0
− +  + 1 ≤ 0,
− ≤0
− ≤0
→0
→ 0,
→0
∃: − +  + 1 ≤ 0 ∧  −  ≤ 0
+1− ≤0
Fourier-Motzkin
¬ − +  + 1 ≤ 0 ∨ ¬  −  ≤ 0 ∨  + 1 −  ≤ 0
MCSat: FM Example
− +  + 1 ≤ 0  → 0
− ≤0
+1− ≤0
¬ − +  + 1 ≤ 0 ∨ ¬  −  ≤ 0 ∨  + 1 −  ≤ 0
MCSat: FM Example
− +  + 1 ≤ 0  → 0
− ≤0
+1− ≤0
→1
¬ − +  + 1 ≤ 0 ∨ ¬  −  ≤ 0 ∨  + 1 −  ≤ 0
− +  + 1 ≤ 0,
≡
+ 1 ≤ ,
− ≤0
→ 0,
≤
1 ≤ ,
≤1
→1
MCSat: FM Example
− +  + 1 ≤ 0  → 0
− ≤0
+1− ≤0  →1  →1
¬ − +  + 1 ≤ 0 ∨ ¬  −  ≤ 0 ∨  + 1 −  ≤ 0
− +  + 1 ≤ 0,
≡
+ 1 ≤ ,
− ≤0
→ 0,
≤
1 ≤ ,
≤1
→1
MCSat – Finite Basis
Every theory that admits quantifier elimination has a finite
basis (given a fixed assignment order)
[, 1 , … ,  ]
1 → 1 , … ,  →
∃: [, 1 , … ,  ]
1 [1 , … ,  ] ∧ ⋯ ∧  [1 , … ,  ]
¬ , 1 , … ,  ∨  [1 , … ,  ]
MCSat – Finite Basis
[1, 2 , … , −1 ,  ]
−1 [1, 2 , … , −1 ]
…
2 [1, 2 ]
1 [1 ]
MCSat – Finite Basis
[1, 2 , … , −1 ,  ]
−1 [1, 2 , … , −1 ]
…
2 [1, 2 ]
1 [1 ]
MCSat – Finite Basis
[1, 2 , … , −1 ,  ]
−1 [1, 2 , … , −1 ]
…
2 [1, 2 ]
1 [1 ]
MCSat – Finite Basis
[1, 2 , … , −1 ,  ]
−1 [1, 2 , … , −1 ]
…
2 [1, 2 ]
1 [1 ]
MCSat – Finite Basis
Every “finite” theory has a finite basis
Example: Fixed size Bit-vectors
[, 1 , … ,  ]
1 → 1 , … ,  →
¬ , 1 , … ,  ∨ ¬(1 = 1 ) ∨ ⋯ ∨ ¬( =  )
MCSat – Finite Basis
Theory of uninterpreted functions has a finite basis
Theory of arrays has a finite basis [Brummayer- Biere 2009]
In both cases the Finite Basis is essentially composed of
equalities between existing terms.
MCSat: Uninterpreted Functions
=  + 1,   − 1 < ,   >
=  + 1,   < ,   > ,  =  − 1
=  + 1,   < ,   > ,  =  − 1
Treat () and () as variables
Generalized variables
MCSat: Uninterpreted Functions
=  + 1,   < ,   > ,  =  − 1
→ 0  → 0 () → 0 () → 2
Conflict:   and   must be equal
¬  =  ∨   = ()
MCSat: Uninterpreted Functions
=  + 1,   < ,   > ,  =  − 1
→ 0  → 0 () → 0  =
(Semantic) Propagation
¬  =  ∨   = ()
MCSat: Uninterpreted Functions
=  + 1,   < ,   > ,  =  − 1
→ 0  → 0 () → 0  =
= ()
¬  =  ∨   = ()
MCSat: Uninterpreted Functions
=  + 1,   < ,   > ,  =  − 1
→ 0  → 0 () → 0  =
= () () → 0
¬  =  ∨   = ()
MCSat – Finite Basis
We can also use literals from the finite basis in decisions.
Application: simulate branch&bound for bounded linear
integer arithmetic
2 6
LP solution:
1 ≤ 0
1 = 0
2 = 3
1 = 0.8
2 = 2.4
1 ≥ 1
1 = 1
2 = 2
5
4
3
2
1
0
1
2
3
4
5
6
1
MCSat: Termination
Propagations
Boolean Decisions
Semantic Decisions
MCSat
≻
Propagations
Boolean Decisions
Semantic Decisions
MCSat
≻
Propagations
Boolean Decisions
Semantic Decisions
MCSat
Maximal Elements
…
||
…
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 2 + 2 ≤ 1
Conflict
¬  ≥ 2 ∨ ¬( ≤ 1)
≤1
¬( 2 +  2 ≤ 1) ∨  ≤ 1
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
≥ 1 2 + 2 ≤ 1
Conflict
¬  ≥ 2 ∨ ¬( ≤ 1)
≥ 2,
≥2
≤1
¬( 2 +  2 ≤ 1) ∨  ≤ 1
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 ¬( 2 +  2 ≤ 1)
¬  ≥ 2 ∨ ¬( 2 +  2 ≤ 1)
¬( 2 +  2 ≤ 1) ∨  ≤ 1
≥ 2,
≥2
¬ ≥ 1 ∨  ≥ 1 ,
≥1
≥ 1 2 + 2 ≤ 1
Conflict
¬  ≥ 2 ∨ ¬( ≤ 1)
≥ 2,
≥2
≤1
¬( 2 +  2 ≤ 1) ∨  ≤ 1
¬ ≥ 1 ∨  ≥ 1 ,
≥1
( 2 +  2 ≤ 1 ∨  > 1)
( 2 +  2 ≤ 1 ∨  > 1)
≥ 1 ¬( 2 +  2 ≤ 1)
¬  ≥ 2 ∨ ¬( 2 +  2 ≤ 1)
¬( 2 +  2 ≤ 1) ∨  ≤ 1
MCSat
< 1 ∨ ,
→1
¬ ∨  = 2
MCSat
< 1 ∨ ,
→1

¬ ∨  = 2
MCSat
< 1 ∨ ,
→1
¬ ∨  = 2

Conflict (evaluates to false)
MCSat
< 1 ∨ ,
→1
¬ ∨  = 2

New clause
<1∨ =2
MCSat
< 1 ∨ ,
→1
¬ ∨  = 2

New clause
<1∨ =2
<1
MCSat
< 1 ∨ ,
→1
¬ ∨  = 2

New clause
<1∨ =2
<1
MCSat: Architecture
Arithmetic
Arrays
Boolean
Lists
MCSat prototype: 7k lines of code
Deduction Rules
Boolean Resolution
Fourier-Motzkin
Equality Split
Ackermann expansion
aka Congruence
Normalization
MCSat: preliminary results
prototype: 7k lines of code
QF_LRA
MCSat: preliminary results
prototype: 7k lines of code
QF_UFLRA and QF_UFLIA
Conclusion
Logic as a Service
Model-Based techniques are very promising
MCSat
http://z3.codeplex.com
http://rise4fun.com/z3
```