Database Reference
In-Depth Information
5.2
COMPILING
P ()
Compiling
a propositional formula
means converting the formula into a Boolean circuit that
has some nice properties, ensuring that we can compute
P ()
in linear time in the size of the
circuit. Several types of circuits have been discussed in the verification and in the AI communities,
which trade off representation power with ease of construction. Whenever a tractable compilation
is possible, then
P ()
is computable in polynomial time, but the converse is not necessarily true.
We review here four compilation targets: read once formulas, OBDDs, FBDDs, and d-DNNFs.
Throughout this section, we assume that all discrete variables
X
are Boolean variables, i.e.,
their domain is
. A circuit for a formula
is a rooted, labeled DAG computing
, with
the following types of gates and restrictions:
{
false, true
}
Independent AND
Such a gate has
n
≥
0 children, representing formulas
1
,...,
n
; the gate
represents the formula
1
∧···∧
n
. The following property is required to hold: for all
i
=
j
,
Va r (
i
)
∩
Va r (
j
)
=∅
.
Independent OR
Such a gate has
n
0 children, representing formulas
1
,...,
n
; the gate
represents the formula
1
∨···∨
n
. The following property is required to hold: for all
i
=
j
,
Va r (
i
)
∩
≥
Va r (
j
)
=∅
.
Disjoint OR
Such a gate has
n
≥
0 children, representing formulas
1
,...,
n
; the gate represents
the formula
1
∨···∨
n
. The following property is required to hold: for all
i
=
j
,
i
∧
j
≡
false
.
¬
.
NOT
Has a single child; if the child represents
, then the gate represents
Conditional gate
The gate is labeled with a Boolean variable
X
and has two children. The edges
leading to the children are labeled with
X
=
0 and
X
=
1, respectively. The node computes
the formula
(
¬
X
∧
0
)
∨
(X
∧
1
)
, where
0
and
1
are the formulas represented by the
two children. The following property must hold
X
∈
Va r (
0
)
and
X
∈
Va r (
1
)
.
Leaf Node
The gate is labeled either with 0 or 1 representing either
false
or
true
, respectively, or
with a variable
X
.
Algorithm 2
can be modified easily to compute a circuit for
instead of computing the
probability
P ()
directly: each rule in the algorithm will construct a gate of the corresponding type.
Moreover, given any circuit for
, one can compute the probability
P ()
in linear time in the size
of the circuit, by traversing the nodes in topological order, and computing the probability at each
node from the probabilities of the children.
The goal of compilation is to find a circuit for
satisfying the restrictions above, and whose
size is polynomial in the size of
.
We consider four compilation targets: read-once formulas, OBDD, FBDD, and d-DNNF
¬
.
We review them here, in decreasing order of their expressive power.
