Transcript Binary Decision Diagrams for First Order Predicate Logic

Binary Decision Diagrams for
First Order Predicate Logic
By: Jan Friso Groote
Afsaneh Shirazi
BDDs for FOL






First order predicate logic
Binary Decision Diagrams
Simple operations on BDDs
Advanced operations on BDDs
Algorithm
Example
2
First Order Predicate Logic


V : variables , F : functions , Pr : predicate symbols
Terms:




x  V is a term
If f  F is a function symbol of arity r and t1,…, tr are terms,
then f(t1,…, tr) is a term
Set of all terms over F and V is denoted by T(F,V)
Set of all predicates of the form P(t1,…,tr) is denoted
by P(Pr, F, V)
3
Substitution




Substitution is a mapping :V  T(F,V)
[x1:=t]: maps each variable x to (x), except
x1 to t
Composition:  o (t) = ((t))
We assume that  is extended : term to term,
predicates to predicates
4
Formulas

Formulas are defined by:






t, f
P(t1, …, tr)  P(Pr, F, V)
 is a formula   is a formula
 and  are formulas     is a formula
 is a formula, and x  V is a variable  x. and
x. are formulas
Set of all formulas: F (Pr, F, V)
5
Structure and Interpretation

A Structure is a ,multi-tuple  = <A; R1, R2,…;F1,
F2,…> where





A is a non empty set
R1, R2,… are relations on A
F1, F2,… are functions on A
Herbrand structures have the form H = <T(F,); R1,
R2,…;f1, f2,…>
Let  be a structure and  : V  A be a valuation. The
interpretation [t ] : T(F, V)  A of a term t is defined:
[ x]   ( x) if x V


[ fj (t1,...,tr )]  Fj ([t1] ,...,[tr ] )
6
Interpretation of a formula



[ ] : F (Pr, F, V)  {0,1}
 [ f ]  0
 [t ]  1



1
if

[
t
]
,...,
[
t
]

1 
r   Ri

 [ pi (t1 ,...,t r )]  
0 otherwise
 [ ]  1  [ ]
 [  ]  min([ ] , [ ] )
 [x. ]  minaA ([ ] [ x: a ] )
 [x. ]  maxaA ([ ] [ x: a ] )
7
FOL



, ╞  iff [ ]  1
╞  iff  , ╞ 
 unsatisifiable iff for each  there is a
valuation , , ╞ 
8
equivalency




   strongly (logically) equivalent
 (,╞  iff ,╞ )
   logically equivalent  (╞  iff ╞ )
   weakly (logically) equivalent
 ,╞  iff  ,╞ 
No free variables: strong logical equivalence
and logical equivalence coincide
9
Binary Decision Diagrams
f

t
A BDD, B  (Q, l , , , s,0,1) is an acyclic, node
labeled graph where






Q : finite set of nodes
l : Q {0, 1}  P(Pr, F, V)  {0, 1} is a node labeling,
that l(q)  0, 1 for all qQ
f
 is the false continuation of a node
t
is the true continuation of a node
s  Q {0, 1} is a start node
0 is a symbol representing false, and 1 representing
truth
0

1
Each sequence q0 q1… is bounded
10
Interpretation of a BDD

Let B be a BDD,  be a structure and  be a
valuation. A , -path of a node q0  Q is the
sequence
0
1
n 1
q 0  q1  ... qn


where qn  {0,1} and for each i, i = f if
,  ╞ l(qi) and i = t if , ╞ l(qi)
If q0 ends in 1 we say that q0 holds, ,  ╞ q0
So, A BDD yields a truth value.
11
Bf =
0
Bt
=
1
BP(t1, …, tr) =
P(t1,…,tr)
0
1
then B =
If B =
0 1
If B =
1 0
and B =
0 1
then B =
0 1
0 1
0 1
12
Example
P(x)
P(x)
P(x)
0
1
Q(y)
R(z)
0
0
P( x)  P( x)
1
( P( x)  Q( y))  R( z )
13
BDD


Let be a (quantifier free) formula and B its
corresponding BDD. For each structure  and
each
valuation

we
find
that
, ╞  iff , ╞ B
Proof: Straightforward on the structure of 
14
BDDs for FOL






First order predicate logic
Binary Decision Diagrams
Simple operations on BDDs
Advanced operations on BDDs
Algorithm
Example
15
Neglect Operator

f
t
f
t
Let B  (Q, l , , , s,0,1) be a BDD.
Neglect operator is defined for some q,
f
t
p q, pq by:
Np ( B)  (Q' , l , ' , ' , s ' ,0,1)
where
s if s  p
s'  
q if s  p
Q '  Q \ { p}



'  { r1, r 2   | r1  p, r 2  p}  { r1, q | r1  p}
16
p,q-join Operator

If
f
f
t
t
l ( p) l (q), p  r , p  r ' , q  r , q  r '
f
then
t
J p ,q ( B)  (Q' , l , ' , ' , s' ,0,1)
where
s if s  q
s'  
 p if s  q
Q '  Q \ {q}



'  { r1, r 2   | r 2  q}  { r1, p | r1  q}
17
f-merge and f-sort operators



f-merge and f-sort operators, sort the BDD
such that labels occur in ascending order.
Sorting a BDD is NP-hard
Avoid sorting a BDD
18
f-merge Operator
f

p  q, l ( p) l (q)
If
f
then
t
M ( B)  (Q' , l , ' , , s,0,1)
f
p
where
Q'  Q(non reachablepart sare removed)
f
f
f
'  { r1, r 2   | r1  p, r 2  q}  { p, r | p  q}
19
f-sort Operator
f

If p  q, l ( p) l (q) then
f
t
S ( B)  (Q' , l ' , ' , ' , s' ,0,1)
f
p
where
l ( p ) if r  p '

l ' ( r )  l ( q ) if r  p ' '
l ( r ) ot herwise

Q '  Q  { p ' , p ' '}( non reachablepart sare removed)
f
f
f
'  { r1, r 2   | r1  p or r 2  p}  { r , p ' ' | r  p} 
f
t
{ p ' ' , p }  { p ' , r | q  r}  { p, r | q  r}
t
t
t
'  { r1, r 2   | r 2  p}  { r , p ' ' | r  p} 
t
{ p ' ' , p ' }  { p ' , r | p  r}
20
21
Simple Operations on BDDs


Lemma: (Soundness) Let B be a BDD. In
case O is applicable to B, O(B)  B
(O is one of N p , J p,q , M tp , M pf , S tp and S pf )
Proof: check that for all structures and
valuations  , ╞ O(B) iff  , ╞ B
Definition: B is reduced iff non of the
operators is applicable
22
Simple Operations on BDDs

Lemma: Let B, C be BDDs pQB and
qQC .Let  be a structure and  a
valuation such that  , ╞ p and ,  ╞ q.
P(t1,…,tn) : label not occurring in subdags
p and q. Then


Exists a structure  and a valuation 
, ╞ p, , ╞ q and , ╞ P(t1,…,tn)
Exists a structure  and a valuation 
, ╞ p, , ╞ q and , ╞ P(t1,…,tn)
23
Simple Operations on BDDs

Lemma: Let B and C be reduced BDDs.
pQB and qQC such that p  q. Then,




l(p) = l(q)
pf  qf
pt  qt
If B,C are the same, then p=q
back
24
Isomorphism


Let B and C be BDDs.
f: QB{0B,1B}  QC{0C,1C} is called
homomorphism
iff
lC(f(p))=lB(p),
f(pf ) = f(p)f and f(pt) = f(p)t . In case f is
bijective, f is called isomorphism.
B = C (isomorphic) if there exists an
isomorphism f.
25
Example
C
B
f
P(x)
Q(x)
0
1
P(x)
Q(x)
0
P( x)  Q( x)
26
Theorem

B and C are reduced BDDs,
B  C. Then B = C (isomorphic).

Proof
back
27
Theorem

Operators N p , J p,q , M tp , M pf , S tp and S pf can be
applied a finite number of times to B.

Proof
back
28
R(B)




Let B be a BDD, C be a reduced BDD,
B  C. According to theorem C is unique up
to an isomorphism and It can be efficiently
obtained (Thrm)  R(B) for C
R(B) = Bt ( tautology)
R(B) = Bf ( contradiction)
Basis for Propositional Logic
29
Advanced Operations on BDDs


Copying Operator C(B): puts B in conjunction
with a copy of itself (different variables)
Unification Operator U(B): instantiate B
according to  ( is a relevant unifier)
30
Copy Operator


Let B be a BDD in which variables
occur.


x1
x

C ( B)  B  B[ x : x 1 ]
not occurring in B
31
Unifier




A substitution  is called a unifier of P(t1, …, tn) and
Q(u1, …, um) iff (P(t1,…, tn))=(Q(u1,…,um))
A unifier is most general (MGU) iff for each unifier ’
of P(t1,…, tn) and Q(u1,…,um) there is a substitution
 such that  o  = ’
Idempotent MGU:  ((x)) = x
Linear time
32
Relevant Unifier



A node p of B is redundant iff pt  pf
A path
0
1
n 1
n
p0  p1 ... pn  l
is allowed iff there are no i, j such that
l(pi)=l(pj) and i  j
A node is truth-truth capable iff there is an
allowed path
t
1
n 1
n
p  p1  ... pn 1
33
Relevant Unifier

A valuation  is a relevant unifier iff
0
1
n 1
n
s  p1  ... pn 1
pi is not redundant, if i = f, pi is not truth-truth
capable, and for some i, j, i = f, j = t and  is
an idempotent MGU of l(pi) and l(pj).
34
Lemma

Let B be a reduced BDD.




No redundant nodes
Every path allowed
If pi is not truth-truth capable pit = 0
 is a relevant unifier iff for some i, j, i=f, j=t
and  is the MGU of l(pi) and l(pj) on the
rightmost path of B
0
1
n 1
n
p0  p1 ... pn 1
35
MGU
y=a
36
Unification Operator

If  is a relevant unifier of B
U ( B)  ( B)

Lemma: (Soundness)



B C(B)
B B U(B)
Proof: easy logical consequence
back
37
BDDs for FOL






First order predicate logic
Binary Decision Diagrams
Simple operations on BDDs
Advanced operations on BDDs
Algorithm
Example
38
Algorithm
Solve( ) 
B : R ( B )
Avoid expensive sorting operator
Repeat
T ryT oReduce(B )
B : R (C ( B ))
Endrepeat
All pairs of pi, pj in the
rightmost path, with pit=0
and pjt0
 Linearly in size of terms
T ryT oReduce(B ) 
If B  B f , report' unsatisfiable' and stop
For all relevantunifiers of B T ryT oReduce(R (U  ( B )))
39
Algorithm
Solve( ) 
B : R ( B )
Repeat
T ryT oReduce(B )
B : R (C ( B ))
Endrepeat
T ryT oReduce(B ) 
The depth of recursive
calls is limited by the
number of free variables
Avoid sorting by grouping
predicates with the same
predicate symbol
If B  B f , report' unsatisfiable' and stop
For all relevantunifiers of B T ryT oReduce(R (U  ( B )))
40
Algorithm
Solve( ) 
B : R ( B )
Repeat
T ryT oReduce(B )
B : R (C ( B ))
Endrepeat
R(U1 (R(U 2 (...R(C(...R(C(B ))))))))
T ryT oReduce(B ) 
If B  B f , report' unsatisfiable' and stop
For all relevantunifiers of B T ryT oReduce(R (U  ( B )))
41
Algorithm

The program is browsing through larger and
larger BDDs of the form
R(U1 (R(U 2 (...R(C(...R(C(B ))))))))

We stop:


Bf Lemma
Bt
42
Russel’s Paradox




A set which contains those sets that are
not members of themselves
F(x,y): x is a member of y
Problem: xy( F ( y, x)  F ( y, y))
negated and Skolemised formula
F ( y, a)  F ( y, y)
43
Russel’s Paradox
F ( y, a)  F ( y, y)
(y) = a
Example
44
Thank You
45
Appendix A
Thrm: B and C are reduced BDDs,
B  C. Then B = C (isomorphic).
 Proof: Define f: QBQC and g: QCQB
f(p) = q such that p  q
g(q) = p such that p  q
f is a homomorphism, g is the inverse of f
 f is an isomorphism
We assumed f and g are well defined.

46
Proof



B  C and all nodes in B are reachable from
the root  each node in B is related via  to
1 node in C
p related to q1,q2  q1  q2
 q1 = q2
(using thrm)
back
47
Appendix B
Proof: The transformation operators can be
formulated as rewrite rules.l1 and l2 are
predicates. l1 > l2
l1 (l2 ( x, y ), z )  l2 (l1 ( x, z ), l1 ( y, z ))
S pf
l1 ( x, l2 ( y, z ))  l2 (l1 ( x, z ), l1 ( y, z ))
S tp
l1 ( x, x)  x
Np
l1 (l1 ( x, y ), z )  l1 ( x, z )
M pf
l1 ( x, l1 ( y, z ))  l1 ( x, z )
M tp
48
Proof



To each DAG we can obtain its canonical tree
by undoing the sharing of subdags.
Application of these rules must terminate on
these trees.
Each rewrite of the DAG corresponds to one
or more rewrite of canonical tree.
In Join operator the number of nodes are
strictly decreasing  It should terminate
back
49
Appendix C




A set is circular if it is a member of another
set, which in turn is a member of the original.
There is no set containing all non circular
sets.
Problem: yx( F ( x, y)  z( F ( x, z)  F ( z, x)))
negated and Skolemised formula (a, f are
skolem functions)
( F ( x, a)  ( F ( x, z )  F ( z, x))) 
(( F ( x, f ( x))  F ( f ( x), x))  F ( x, a))
50
There are no circular sets
Two relevant unifier:
1. Mapping z and x to a
2. Mapping x to z
( F ( x, a)  ( F ( x, z )  F ( z, x))) 
(( F ( x, f ( x))  F ( f ( x), x))  F ( x, a))
51
There are no circular sets
We must apply copying
operator.
6 relevant unifier:
1. x:=a z:=a
2. u:=a v:=a
3. x:=v u:=a
4. u:=z x:=a
5. z:=x
6. v:=u
52
There are no circular sets
We apply first unifier.
4 relevant unifier:
1. u:=f(a) v:=a
2. u:=a v:=a
3. u:=a
4. v:=u
back
53