Transcript Equality Logic and Uninterpreted Functions

Generating minimum
transitivity constraints in
P-time for deciding
Equality Logic
Ofer Strichman and Mirron Rozanov
Technion, Haifa, Israel
Technion
1
Deciding Equality Logic (TE)

The eager approach: TE ! Pr

Bryant & Velev [BV-CAV’00] – Boolean satisfiability with
transitivity constraints.
Meir and Strichman [MS-CAV’05] – Yet another decision
procedure for equality logic.


This work: a ‘closure’ on [MS-CAV’05]
Technion
2
Basic notions
E: x = y Æ y = z Æ z  x
(non-polar) Equality Graph:
y
x
z
Technion
3
From Equality to Propositional Logic
E : x1 = x2 Æ x2 = x3 Æ x1  x3
sk :
e1,2 Æ
e2,3 Æ :e1,3
x1
e1,3
[BV-CAV'00] – the Sparse method
x2
x3

Encode all edges with Boolean variables

Add transitivity constraints
Technion
4
From Equality to Propositional Logic
E : x1 = x2 Æ x2 = x3 Æ x1  x3
sk :
e1,2 Æ
e2,3 Æ :e1,3
x1
e1,3
[BV-CAV'00] – the Sparse method
x2
x3

Transitivity Constraints: For each cycle of size n,
forbid a true assignment to n-1 edges
T S = (e1,2 Æ e2,3 ! e1,3) Æ
(e1,2 Æ e1,3 ! e2,3) Æ
(e1,3 Æ e2,3 ! e1,2)
Check: sk Æ T S
Technion
5
From Equality to Propositional Logic
[BV-CAV'00] – the Sparse method

Thm-1: It is sufficient to constrain chord-free simple
cycles
e2
e1
e5
e3
e4

There can be an exponential number of chord-free
simple cycles…
Technion
6
From Equality to Propositional Logic
[BV-CAV'00] – the Sparse method

Make the graph ‘chordal’.

In a chordal graph, it is sufficient to constrain only triangles.

Polynomial # of edges and constraints.

# constraints = 3 £ #triangles
Technion
7
An improvement
[MS-CAV’05] – the RTC method

So far we did not consider the polarity of the edges.
E: x = y Æ y = z Æ z  x

Assuming E is in Negation Normal Form
y
(polar) Equality Graph:
x

Technion
z
8
An improvement
Reduced Transitivity Constraints (RTC)

Here, T
R
= e3 Æ e2 ! e1 is sufficient
z

T
Allowing e.g.
:x = z, x = y, z  y
T
e3
e1
x

F
e2
’:x = z, x = y, z = y
=
y
T
This is only true because of monotonicity of NNF
Technion
9
Definitions

Dfn-1: A contradictory cycle is a cycle with exactly
one disequality edge.
T
T
C=
T
T


F
Dfn-2: A contradictory Cycle C is constrained under
T if T does not allow such an assignment.
Technion
10
Main theorem
[MS-CAV’05]

Let T R be a conjunction of transitivity constraints.

If T R constrains all simple contradictory cycles
then
E is satisfiable iff sk Æ T R is satisfiable
The Equality
Formula
Technion
11
Transitivity: 5 constraints
RTC: 0 constraints
T
T
T
Transitivity: 5 constraints
RTC: 1 constraint
T
F
Technion
12
Applying RTC

How can we use the theorem without enumerating
contradictory cycles ?

Answer:
 Consider
the chordal graph.
 Still – which triangles ? which constraints?
Technion
14
The RTC solution
[MS-CAV’05]
x2
x0
x4
cache:
e0,2 Æ e1,2 
e0,1 Æ e  e
e
1,3
2,3
1,2
e2,4 Æ e3,4  e2,3
e0,2 Æ e0,4  e2,4
x1

x3
1) Exp # cycles to traverse 2) Not all cycles are simple.



Solution to 1): Stop before adding an existing constraint
Solution to 2): Explore only simple cycles
These solutions cannot be combined.
Technion
15
Constraining simple contradictory cycles
x7
1. Focus on each solid edge es separately
- (find its dashed Bi-connected component)
2. Make the graph chordal
x0
x2
x4
x3
x5
es
x1
Dowe
weneed:
need:
Do
Technion
x6
Æee3,6! !ee3,5 ??
5,6Æ
ee3,5
3,6
5,6
18
Constraining simple contradictory cycles
3. Remove a vertex xk that leans on an edge (xi,xj)
4. Is (xi,xj) on a simple cycle with es? O(|E|)
5. If yes, add (ek,i Æ ek,j ! ei,j)
x0
e5,6 Æ e3,6  e3,5
x2
x4
x3
x5
es
x1
Technion
x6
19
Constraining simple contradictory cycles
3.
Remove a vertex vk that leans on an edge (vi,vj)
4.
Does (vi,vj) on the same simple cycle with es?
5.
If yes, add (ek,i Æ ek,j ! ei,j)
x0
e5,6 Æ e3,6  e3,5
x2
x4
es
x1
x5
x3
Technion
x6
20
Correctness

The set of generated constraints is sufficient.

The set of generated constraints is necessary.
Technion
21
Random graphs (Satisfiable)
[MS-CAV’05]
Technion
22
Results – random graphs
400000
350000
Constraints
300000
250000
RTC
RTCS
200000
150000
100000
50000
0
10
30
50
70
% dashed
V=200, E=800, 16 random topologies
# constraints:
Run time:
reduction of 17%
reduction of 32%
Technion
23
Results – random graphs
450
400
run-time
350
300
250
RTC
RTCS
200
150
100
50
0
10
30
50
70
% dashed
V=200, E=800, 16 random topologies
# constraints:
Run time:
reduction of 17%
reduction of 32%
Technion
24
SMT benchmarks

Never really finished the implementation…

Our 4-5 experiments with them showed that



We still have a small advantage comparing to the Sparse method.
Yet Yices is much better….
A result of the Uninterpreted functions.

Are there formulas for which the eager approach still wins?

Generating meaningful equality formulas is hard…
Technion
25
A crafted example
2n assignments satisfy sk. None satisfy the theory.
Technion
26
Thank you
Technion
27
Results
Uclid benchmarks* (all unsat)
* Results strongly depend on the reduction method of Uninterpreted Functions.
Technion
28

Possible refutations of CNF’s generated by Sparse
Boolean
Encoding
Æ
B
Transitivity
constraints
TS
TR
B
P3
P2
P0
P4
TS–TR
P1
P2
ofaccording
the formtoe1the
Æmain
e2 ! theorem.
e3
AConstraints
P3 proof exists
Hypothesis: (T S – T R) clauses hardly participate in the proof
Thm: B is satisfiable ! B Æ (T S – T R) is satisfiable
Technion
32
T
R
CNF
B
T S- T R
TR
Average on:
10 graphs,
~890K clauses
All Unsat
Sparse: ~ 22 sec.
RTC: ~ 12 Sec.
B
Core
B – Boolean encoding
T R – RTC constraints
T S – Sparse constraints
T S- T R
Technion
33
Summary

The RTC method is ~dominant over the Sparse
method.

Open issue: find a P-time algorithm that exploits the
full power of the main theorem.
Technion
34
Example: Circuit Transformations
Stage 1
Stage 2

A pipeline processes data in stages

Data is processed in parallel – as in an
assembly line

Formal Model:
Stage 3
Technion
40
Example: Circuit Transformations

The maximum clock frequency depends
on the longest path between two latches

Note that the output of g is used
as input to k

We want to speed up the design by
postponing k to the third stage
Technion
41
Validating Circuit Transformations
?
=
Technion
42
Validating a compilation process

Target program

u1 = x1 + y1;
u2 = x2 + y2;
z = u1  u2 ;

Compilation
Source program
z = (x1 + y1)  (x2 + y2);
Need to prove that:
(u1 = x1 + y1  u2 = x2 + y2  z = u1  u2) $ z = (x1 + y1)  (x2 + y2)
Source
Target
Technion
43
Validating a compilation process

Target program

u1 = x1 + y1;
u2 = x2 + y2;
z = u1  u2 ;

Compilation
Source program
z = (x1 + y1)  (x2 + y2);
Need to prove that:
(u1 = x1 + y1  u2 = x2 + y2  z = u1  u2) $ z = (x1 + y1)  (x2 + y2)
f1
f2
g1
f1
f2
g2
Technion
44
Validating a compilation process

Instead, prove:
under functional consistency: for every uninterpreted function f

x = y ! f(x) = f(y)
Need to prove that:
(u1 = x1 + y1  u2 = x2 + y2  z = u1  u2) $ z = (x1 + y1)  (x2 + y2)

Which translates to (via Ackermann’s
reduction):
g
f1
f2
1
f1
f2
g2
Technion
45
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 R
Technion
47
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
Technion
T
v2
48
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
Technion
T
v2
49
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
Technion
50
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
Technion
51
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 S

B is still satisfied (monotonicity of NNF)

Left to prove: all contradictory cycles are still
satisfied
Technion
52
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…
Technion
53
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…
Technion
54
Constraining simple contradictory cycles
The constraint e3,6 Æ e3,5  e5,6 is not added
x0
x1
x2
cache:
…
e5,6 Æ e4,6  e4,5
x4
x5
x3
x6
Open problem: constrain simple contradictory cycles in P time
Technion
55
Constraining simple contradictory cycles
the constraint
e3,6graph
Æ e3,5has
 e35,6
is not
added, though needed
Suppose the
more
edges
Here we will stop, although …
cache:
x0
x1
…
e5,6 Æ e4,6  e4,5
x2
x4
x5
x3
x6
Open problem: constrain simple contradictory cycles in P time
Technion
56