Transcript equality-transitivity-constraints

Decision Procedures in
First Order Logic
Decision Procedures for
Equality Logic
Daniel Kroening and Ofer Strichman
1
Part III – Decision Procedures for Equality
Logic and Uninterpreted Functions

Algorithm I – From Equality to Propositional Logic
 Adding
transitivity constraints
 Making the graph chordal
 An improved procedure: consider polarity

Algorithm II – Range-Allocation
 What
is the small-model property?
 Finding a small adequate range (domain) to each variable
 Reducing to Propositional Logic
Decision Procedures
An algorithmic point of view
2
Decision Procedures for Equality Logic

We will first investigate methods that solve Equality
Logic. Uninterpreted functions are eliminated with
one of the reduction schemes.

Our starting point: the E-Graph GE(E)

Recall: GE(E) represents an abstraction of E:
It represents ALL equality formulas with the same set
of equality predicates as E
Decision Procedures
An algorithmic point of view
3
From Equality to Propositional Logic
Bryant & Velev 2000: the Sparse method
enc = e1

Æ
e2
Æ :e3
e3
E = x1 = x2 Æ x2 = x3 Æ x1  x3
Encode all edges with Boolean variables
 (note:
for now, ignore polarity)
 This is an abstraction
 Transitivity of equality is lost!
 Must add transitivity constraints!
Decision Procedures
An algorithmic point of view
4
From Equality to Propositional Logic
enc = e1

Æ
e2
Æ :e3
e3
E = x1 = x2 Æ x2 = x3 Æ x1  x3
For each cycle add a transitivity constraint
trans =
(e1 Æ e2 ! e3) Æ
(e1 Æ e3 ! e2) Æ
(e3 Æ e2 ! e1)
Check: enc Æ trans
Decision Procedures
An algorithmic point of view
5
From Equality to Propositional Logic

There can be an exponential number of cycles, so
let’s try to make it better.

Thm: it is sufficient to constrain simple cycles only
T
e2
T
T
e3
e4 F
e1
e6
T
e5
T
Decision Procedures
An algorithmic point of view
6
From Equality to Propositional Logic

Still, there is an exponential number of simple cycles.

Thm [Bryant & Velev]: It is sufficient to constrain
chord-free simple cycles
T
e2
T
F e1
e5
F
T
e3
T
e4
Decision Procedures
An algorithmic point of view
7
From Equality to Propositional Logic

Still, there can be an exponential number of chordfree simple cycles…
….

Solution: make the graph ‘chordal’ by adding edges.
Decision Procedures
An algorithmic point of view
8
From Equality to Propositional Logic

Dfn: A graph is chordal iff every cycle of size 4 or
more has a chord.

How to make a graph chordal ? eliminate vertices one
at a time, and connect their neighbors.
Decision Procedures
An algorithmic point of view
9
From Equality to Propositional Logic

Once the graph is chordal, we can constrain only the
triangles.
T
T
Contradiction!
T
T
T
F
T

Note that this procedure adds not more than a
polynomial # of edges, and results in a polynomial
no. of constraints.
Decision Procedures
An algorithmic point of view
10
Improvement

So far we did not consider the polarity of the edges.

Claim: in the following graph trans = e3 Æ e2 ! e1 is
sufficient
e1
e3
e2

This is only true because of monotonicity of NNF
Decision Procedures
An algorithmic point of view
11
Definitions

Dfn: A contradictory Cycle C is constrained under T
if T does not allow this assignment
T
T
C=
T
T
F
Decision Procedures
An algorithmic point of view
12
Main theorem

If
T R constrains all simple contradictory cycles,
and
S
S
S
For every assignment  ,  ² T !  ² T

R
From the Sparse
method
then
E is satisfiable iff B Æ T
The Equality
Formula
S
R
is satisfiable
Decision Procedures
An algorithmic point of view
13
Transitivity: 5 constraints
RTC: 0 constraints
T
T
T
Transitivity: 5 constraints
RTC: 1 constraint
T
F
Decision Procedures
An algorithmic point of view
14
Proof of the main theorem

() E is satisfiable  BÆT S is satisfiable  BÆT
is satisfiable

() Proof strategy:
R
R be a satisfying assignment to B Æ T R
 We will construct S that satisfies B Æ T S
 From this we will conclude that E is satisfiable
 Let
Decision Procedures
An algorithmic point of view
Skip proof
15
Definitions for the proof…

A Violating cycle under an assignment R:
F
eF
eT1
T
Either
dashed or
solid
T
eT2

This assignment violates T S but not necessarily T
Decision Procedures
An algorithmic point of view
R
16
More definitions for the proof…

An edge e = (vi,vj) is equal under an assignment  iff
there is an equality path between vi and vj all assigned
T under . Denote:
v3
F
T
T
v1
T
Decision Procedures
An algorithmic point of view
T
v2
17
More definitions for the proof…

An edge e = (vi,vj) is disequal under an assignment 
iff there is a disequality path between vi and vj in
which the solid edge is the only one assigned false by
. Denote:
v3
F
T
T
v1
T
Decision Procedures
An algorithmic point of view
T
v2
18
Proof…

Observation 1:
The combination
is impossible if = R
(recall: R ² T R)
v3
F
T
T
v1

v2
Observation 2: if (v1,v3) is solid, then
Decision Procedures
An algorithmic point of view
19
ReConstructing S
Type 1:
Type 2:
It is not the case that
Otherwise it is not the case that
v3
v3
F
F
T
T
F
T
T
v1

T
v1
v2
Assign S (e23) = F

v2
Assign  (e13) = T
In all other cases S = R
Decision Procedures
An algorithmic point of view
20
ReConstructing S

Starting from R, repeat until convergence:


(eT) := F in all Type 1 cycles
(eF) := T in all Type 2 cycles

All Type 1 and Type 2 triangles now satisfy T

B is still satisfied (monotonicity of NNF)

Left to prove: all contradictory cycles are still
satisfied
Decision Procedures
An algorithmic point of view
S
21
Proof…

Invariant: contradictory cycles are not violating
throughout the reconstruction.
T
v3
F
T
F
T
T
v1

v2
contradicts the precondition to make this
assignment…
Decision Procedures
An algorithmic point of view
22
Proof…

Invariant: contradictory cycles are not violating
throughout the reconstruction.
v3
F
T
T
T
T
F
v1

v2
contradicts the precondition to make this
assignment…
Decision Procedures
An algorithmic point of view
23
Applying RTC

How can we use the theorem without enumerating
contradictory cycles ?

Answer:
 Consider
the chordal graph.
 Constrain triangles if they are part of a (simple)
contradictory cycle
 How?
Decision Procedures
An algorithmic point of view
24
• Should we constrain
this triangle?
• In which direction ?
• Is this constraint
necessary ?
Decision Procedures
An algorithmic point of view
26
Decomposing the graph

Focus on Bi-connected dashed components built on
top of a solid edge
 Includes
all contradictory cycles involving this edge
Decision Procedures
An algorithmic point of view
27

Make the component chordal
 Chordal-ity guarantees: every
cycle contains a simplicial
vertex, i.e. a vertex that its neighbors are connected.
Decision Procedures
An algorithmic point of view
28
The RTC algorithm

Constraints cache:



e2 Æ e3 ! e1
e4 Æ e7 ! e2
e5 Æ e8 ! e4
5
8
6
4
7
3
9
2
1
11
Decision Procedures
An algorithmic point of view
12
29
Constrains all contradictory cycles

Constraints cache:



e2 Æ e3 ! e1
e4 Æ e7 ! e2
e6Æ e3 ! e4
5
8
6
4
7
3
9
2
1
11
Decision Procedures
An algorithmic point of view
12
30
Results – random graphs
400000
350000
250000
Sparse
200000
RTC
150000
# constraints
300000
100000
50000
0
10:01
05:01
02:01
01:01
01:02
01:05
01:10
Solid : Dashed
V=200, E=800, 16 random topologies
Decision Procedures
An algorithmic point of view
31
Random graphs (Satisfiable)
Decision Procedures
An algorithmic point of view
32