Database Reference
In-Depth Information
and of NOT gates, which are allowed to combined in any order. The family d-DNNF
¬
is closed
¬
, simply add a new root node, labeled NOT, to the d-DNNF
¬
for
. Given an d-DNNF
¬
-circuit representing a formula
, one can compute the probability
P ()
in linear time in the size of the circuit.
under negation: to compute
5.2.2 FBDD
A
Free Binary Decision Diagram
is a circuit where every internal node is a conditional gate on some
variable
X
, and where every leaf gate is either 0 or 1 [
Wegener
,
2004
].They are called Binary Decision
Diagrams because each internal node makes a decision based on one variable
X
; they are called free
because of the restriction that every path from the root to a leaf checks every variable
X
at most once.
Figure 5.2
shows an FBDD. d-DNNF's are at least as powerful as FBDD's in the following sense.
Any
FBDD
of size
n
can be converted to an d-DNNF of size at most 5
n
[
Darwiche and Marquis
,
2002
], as follows. For every node in the
FBDD
that tests a variable
X
, write its formula as
(
¬
X)
∧
0
∨
X
∧
1
, where
0
,
1
are the two formulas of its 0-child and 1-child, respectively: obviously,
the
's are “decomposable”. We have thus replaced one node in the
FBDD with 5 nodes in the d-DNNF:
∨
is “deterministic”, and the
∧
∨
,
∧
,
∧
,
X
, and
¬
X
.
5.2.3 OBDD
An
Ordered Binary Decision Diagram
is an FBDD with the property that every path from the root to
a leaf node inspects the Boolean variables in the same order. Thus, every OBDD is also an FBDD,
but the converse is not true. The FBDD shown in
Figure 5.2
is actually an OBDD because all
paths inspect the variables in the same order,
X
1
,Y
1
,Y
2
,X
2
,Y
3
,Y
4
. We review here two important
properties of OBDDs. The first is that every read-once formula
has an OBDD of linear size. The
proof is by induction, as follows: if
2
, then one first constructs inductively an OBDD
for
1
and for
2
. Then, redirect all 1-leaves of
1
, to the root of the OBDD for
2
. The result
is still an OBDD because
is read-once, meaning that
1
and
2
use disjoint sets of Boolean
variables; hence, any path, starting in
1
and continuing in
2
, inspects every variable only once.
The case
=
1
∨
2
is similar. Thus, by induction, a read-once expression
has an OBDD of
linear size. The second property is that OBDDs can be
synthesized
, inductively on the structure of
a formula. To describe the synthesis process, we will assume that every path in an OBDD from the
root to a leaf node contains all variables: this can be ensured by inserting new nodes for the missing
variables, with both edges leading to the same child. Call the
width
of an OBDD at level
i
, the
number of conditional gates for the variable
X
i
; the
width
of the OBDD is the largest width at any
level. Clearly, an OBDD of width
w
has size
=
1
∧
≤
wn
, where
n
is the number of Boolean variables.
The synthesis property is the following. Suppose we are given two OBDDs for
1
,
2
, respectively,
of width
w
1
and
w
2
, and that they use the same variable order. Then one can construct an OBDD
for
1
∧
2
(or for
1
∨
2
, respectively) of width at most
w
1
·
w
2
. The reader is invited to check
the proof: the synthesized OBDD simply keeps track, at leach level
i
, of all nodes in both OBDDs,
