Efficient Boolean Manipulation with OBDD''s Can be Extended to FBDD''s.
OBDD's are the state-of-the-art data structure for Boolean function manipulation. Basic tasks of Boolean manipulation such as equivalence test, satisfiability test, tautology test and single Boolean synthesis steps can be performed efficiently in terms of fixed ordered OBDD's. The bottleneck of most OBDD-applications is the size of the represented Boolean functions since the total computation merely remains tractable as long as the OBDD-representations remain of reasonable size. Since it is well known that OBDD's are restricted FBDD's (free BDD's, i.e., BDD's that test, on each path, each input variable at most once), and that FBDD-representations are often much more (sometimes even exponentially more) concise than OBDD-representations. We propose to work with a more general FBDD-based data structure. We show that FBDD's of a fixed type provide, similar as OBDD's of a fixed variable ordering, canonical representations of Boolean functions, and that basic tasks of Boolean manipulation can be performed in terms of fixed typed FBDD's similarly efficient as in terms of fixed ordered OBDD's. In order to demonstrate the power of the FBDD-concept we show that the verification of the circuit design for the hidden weighted bit function proposed Bryant can be carried out efficiently in terms of FBDD's while this is, for principal reasons, impossible in terms of OBDD's.
Introduction
The need for data structures for Boolean functions becomes obvious if one has applications
in mind as circuit design, optimization, verification, testing, etc. Let us
consider e.g. basic problems of logic verification. By means of hardware description
languages circuits can be described at a very high level of abstraction, that allows
the designer to specify the behavior of a circuit before realizing it. In order to validate
these specifications and in order to verify a designed circuit, with respect to
its specification, formal methods were developed that lead to problem descriptions
in terms of Boolean functions. The verification problem is then solved by analyzing
and manipulating these functions. Let us consider as an example the problem of
determining whether a combinational circuit C correctly implements a given specification
S. That is to test whether are the functions realized
by C and S, respectively. One possibility to do this [e.g. Eve91, FFK88, MWBS88,
is, first, to construct representations for fC and f S (usually in terms of the
primary inputs), and, second, to perform the equivalence test for both functions in
terms of these representations. Hence, efficient algorithms for solving the verification
task under consideration require
ffl efficient algorithms for deriving the representations of the involved Boolean
functions (e.g. from a circuit description) as well as
ffl efficient algorithms to solve the equivalence test or similar tests such as satisfiability
or tautology in terms of these representations.
In the past, a great variety of representations of Boolean functions such as truth-
tables, disjunctive (DNF) and conjunctive normal forms (CNF), Reed-Muller-expansions,
various types of formulas, Boolean circuits, or branching programs have been inves-
tigated. However, the demand for supporting the mentioned basic tasks in Boolean
manipulation became obvious only then when computer applications really had
started to work with more complex Boolean functions.
In order to come to a full understanding of the fundamental trade-off between
succinctness of the representation and efficiency of solving the basic tasks observe
that the complexity has to be measured in the length of the representations of
the input functions. Hence, working e.g. with truth-tables one has much time for
computations. However, such a representation requires in any case space ressources
that are exponential in the number of primary inputs. On the other side, working
with e.g. formulas one often obtains very succinct and, consequently, space efficient
representations but solving e.g. the equivalence test becomes co-NP-hard.
Unfortunately, a systematic inspection of the different succinct representation schemes
[e.g. GM92a] has shown that allmost all of them do not support efficient solutions
of the Boolean manipulation basic tasks. More worse, performing the basic tasks
often requires the solution of NP-hard problems. The only exceptions seem to be
BDD-based Boolean function representations [e.g. Ake78, Bry86, Mei91, GM92a]
that provide with so-called OBDD's the state-of-the-art data structure for Boolean
functions. They allow
1. canonical representations (and, hence, efficient solutions of the equivalence test
and similar tests such as satisfiability or tautology test), and allow
2. efficient performance of binary Boolean synthesis steps (and, hence, efficient
procedures for deriving the OBDD-representation of a Boolean function from
a given circuit description).
Due to these nice properties, OBDD's are successfully used in many applications such
as, for example, sequential circuit verification [e.g MB90, BCM90, Fil91], testing
[e.g. Bec92, KBS93], or logic optimization [Kar89]. For a survey see [Bry92].
Unfortunately, OBDD-representations are not very succinct and, hence, not very
space-efficient. It arises the question whether there are more sophisticated BDD-
representations that are, first, more succinct and space-efficient as OBDD's, and,
second, allow efficient solutions of the basic tasks of Boolean manipulation similarly
as OBDD's do. A number of OBDD-extensions were proposed with the aim to overcome
the mentioned disadvantages of OBDD's [e.g. ADG91, JPHS91, BJAAF92].
However, the obtained increase in space-efficiency of the representation has to be
paid in the mentioned approaches with co-NP-completeness of the equivalence test
[GM92a]. A natural candidate for an OBDD-extension that allows efficient equivalence
test (at least probabilistical [BCW80]) are BDDs that read input variables in
the course of computation at most once, so-called FBDD's. Since OBDD's are special
structured BDDs with this read-once-only property, FBDD's indeed generalize
the OBDD-concept.
BDD-based Data Structures for
Boolean Functions
BDD-based data structures for Boolean functions use the following representations
schemes.
A binary decision diagram (BDD) over a set X of Boolean variables
is a directed acyclic graph with one source and at most two sinks labeled by 0 and
1. Each non-sink node v is labeled by a Boolean variable l(v) 2 X n , and has two
outgoing edges one labeled by 0 and the other by 1. The computation path for an
input starts at the source. At an inner node with label x i the
outgoing edge with label a i is chosen. The BDD P represents a Boolean function
if the computation path for each input a leads to the sink with label f(a).
f is sometimes denoted by f P .
A BDD is called on each path, each
variable is tested at most once.
An ordered binary decision diagram (OBDD) is an FBDD with the property that
on each path the variables are tested in a fixed order.
Examples of an FBDD and an OBDD are given in Figure 1. Generally we draw
BDDs in such a way that, if the edges are not labeled, then we assume the left edge
to be labeled by 0 and the right edge by 1.
A
A
A
A


\Gamma\Psi
@
@
@
@R
\Gamma\Psi
@
@
@
@R
A
A
A
AU
\Deltaff
A
A
A
AU
\Deltaff
\Gamma\Psi
@
@
@
@R
\Gamma\Psi
A
A
A
AU
\Deltaff
A
A
A
AU

\Phi-

x 40(a) (b)

Figure

1.
Example of an FBDD (a) and an OBDD (b) for the function f(x 1
Because of the remarkable property that (the logarithm of) BDD-size corresponds to
Turing machine space under the name of branching programs BDD-
representations have been extensively studied in complexity theory [e.g. Weg87,
Mei89]. The theoretical interest in FBDD-representations which are known in complexity
theory as read-once-only branching programs arises from a similar correspondence
to eraser Turing machine space.
It is well known that each Boolean function f 2 IB n over X n can be represented
in terms of BDDs, in terms of FBDD's or, for any variable ordering, in terms of
OBDD's. Optimal BDD-representations are, in comparison with two-level-represen-
tations such as DNFs or CNFs or with multi-level-representations such as Boolean
formulas, more succinct and space-efficient [e.g. Mei89]. However this succinctness
makes it often difficult or sometimes even infeasible to perform the basic tasks of
Boolean manipulation. For example, it is a co-NP-complete problem to test whether
two BDDs represent the same Boolean function [CHS74].
The situation changes dramatically if one works with restricted types of BDDs.
Then, it is sometimes possible to perform efficiently the basic tasks of Boolean
manipulation, although restriction properties have to be maintained in the course
of the computation. Bryant [Bry86] was the first who observed that OBDD's have
this property. In more detail, OBDD's possess the following outstanding properties.
Fact 1 [Bry86].
1. With respect to a fixed variable ordering the representation of a Boolean function
by means of a reduced OBDD is canonical, i.e. uniquely determined.
2. Let P 0 and P 00 be two OBDD's with the same variable ordering. Each binary
Boolean synthesis step can be performed in time O(size(P
Due to these properties OBDD's defined over a fixed variable ordering are well suited
to be used as a data structure for Boolean functions [Bry86]. Indeed, nowadays
such OBDD's are the state-of-the-art data structure for Boolean functions utilized
in various packages for applications in CAD [e.g. BRB91]. However, the disadvantage
of OBDD data structures is the often very low space efficiency of the OBDD-
representations. Although wide classes of practically important Boolean functions
possess - at least with respect to some well-suited variable orderings - space-efficient
(i.e. polynomial size) OBDD-representations, there are many important functions
without such succinct representations. For example, there exist Boolean functions
such as integer multiplication, hidden weighted bit function (HWB), or indirect storage
access function (ISA) that can not be represented by OBDD's of polynomial size
[FHS78, Bry91, BHR91] for any variable ordering.
Computational Advantages of the FBDD's
Although there are many Boolean functions such as e.g. all symmetric functions for
which optimal FBDD-representations are OBDD's for many important functions
the restriction of FBDD's to OBDD's causes an exponential increase in size. Here
we are going to discuss some Boolean functions with the property that, for each
variable ordering, the OBDD-size is exponential in the FBDD-size.
The first idea to construct examples of Boolean functions with small (i.e. polynomial
FBDD-size and large (i.e. exponential size) OBDD-size is to consider Boolean
functions of the form
where f 0 and f 1 have polynomial size OBDD's for variable orderings - 0 , and - 1 ,
and exponential size OBDD's for - 1 , and - 0 , respectively. If we replace the single
multiplexer variable x 0 by a larger Figure 2), and if
we take functions f with polynomial size OBDD's which do not have a
good variable ordering in common we can get a large class of Boolean functions with
small FBDD-size and large OBDD-size.
@
@
@
@@

Figure

2.
Due to a similar idea, Fortune, Hopcroft and Schmidt have constructed in [FHS78]
an FBDD P of size smaller than 3n 2 such that each OBDD for
at least 2
n=2\Gamma(log 3 n+1)=2 . Verification methods and circuit realizations of FHS are
presented in [JBAF92].
A second interesting example is the indirect storage access function ISA. ISA is
defined variables as follows: Let let the variables of
ISA be partitioned in m+ 1 groups
If P
then the output of ISA is x j with
and 0 otherwise.
Breitbart, Hunt III and Rosenkrantz have proven that any OBDD computing ISA
has size at least 2 n=logn\Gamma1 [BHR90]. On the other hand, they have shown that ISA
can be computed by an FBDD (even by a decision tree) of size at most 2n 2 =logn.
@
@
@ @
@
@
\Gamma\Psi
. y
x (l\Gamma1)k x (l\Gamma1)k+1 . x
Memory
Register

Figure

3.
Indirect storage access function ISA.
Finally we are going to discuss in more detail the hidden weighted bit function HWB
discussed by Bryant in [Bry91]. Let wt(x) be the number of ones in the input
assignment
and Although each OBDD-representation of HWB is of
exponential size [Bry91] it can be computed by a polynomial (even a quadratic) size
FBDD. To explain this we use a construction due to Bryant [Bry92b]. It is based
on the computation of appropriately chosen restrictions of HWB. If x i:j represents
and
One can easily verify that
and
The main idea is explained in Figure 4. Simultaneously we compute H 1:n and G 1:n .
restrictions on the same level are merged together. Since, on each level,
k is fixed, we have at most 2n nodes on each level. Furthermore, on any source-
to-sink-path each variable is tested. Hence, the FBDD size of HWB is at most
@
@
@ @R
\Gamma\Psi
@
@
@ @R
\Gamma\Psi
@
@
@ @R
\Gamma\Psi
@
@
@ @R
\Gamma\Psi
@
@
@ @R
\Phi-
G 1:n
G 2:n

Figure

4.
Construction of an FBDD PHWB that computes the hidden weighted bit function
HWB.
After having seen that there are important functions with small size FBDD's whose
OBDD-sizes are, with respect to any variable ordering, exponential, let us mention
a further computational advantage of FBDD's over other Boolean function repre-
sentations. Due to [BCW80] we can assign to each FBDD a signature that allows
to test functional equivalence of FBDD's probabilistically in polynomial time. This
property applied to OBDD's is the basis of very efficient hash techniques that are
used extensively in efficiently working OBDD-packages such as in the package of
Brace, Bryant and Rudell [BRB90]. The signatures of Boolean functions have found
many further applications [YBAF92, Kri93, KBS93]. Since signatures can be computed
for FBDD's similarly as for OBDD's these hash techniques can be used to
work with FBDD's, too. We remark only, that no similar property is known for
other (compact) Boolean function representations.
4 FBDD Types
In order to extend the efficient manipulation of OBDD's to FBDD's we have to show
that it is possible to perform single Boolean synthesis steps in terms of FBDD's similar
efficiently (i.e. in polynomial time) as in the case of OBDD's. To be more precise,
let   be a Boolean operator   2 IB 2 . Then, by
we denote the problem of constructing an FBDD P for
the function f 00 from given FBDD-representations P 0 and P 00 for f 0 and
f 00 . Sometimes we suppress the operator   and write easily SY N FBDD . SY NOBDD
denotes the similar problem for OBDD's. Unfortunately, investigations of the complexity
of SY N FBDD have shown that performing Boolean synthesis steps in terms
of FBDD's is NP-hard [GM92a]. The reason for the intractability of SY N FBDD
is caused by the different ways the input FBDD's can test the variables. Indeed,
considering OBDD's instead of FBDD's the same effect can be observed: Performing
a Boolean synthesis step (SY NOBDD ) with OBDD's of different variable orders
is NP-hard, too [GM92a]. However, if we restrict the problem to OBDD's of the
same variable order - (SY N -OBDD ) the problem becomes efficiently solvable in time
The goal of this section is to introduce formally the
notion of a type of an FBDD that generalizes the linear variable ordering of OBDD's
and that allows to
canoncially represent Boolean functions in terms of FBDD's with respect to
any given complete type - , and to
ffl efficiently perform a single Boolean synthesis step for FBDD's of the same
An (FBDD-)type is defined similarly as an FBDD with the only exception that it
possesses merely one sink that is labeled by a symbol t.
If P is an FBDD than tp(P ) is derived easily from P by identifying the sinks of P .
@
@
@
@R
\Gamma\Psi
J-
\Omega \Omega \Omega \Omega AE
\Omega \Omega \Omega \Omega AE
A
A
A
A AU
\Omega \Omega \Omega \Omega \Omega AE
A
A
A
AU
'/
@
@
@ @R
@
@
@
@ @R


\Gamma\Psi
\Gamma\Psi
'/
\Omega \Omega \Omega \Omega \Omega AE
A
A
A
A AU
\Omega \Omega \Omega \Omega AE
A
A
A
AU

Figure

5.
An FBDD P and the type tp(P ).
There are two syntactical reduction rules usually applied to BDDs, FBDD's, OBDD's,
and types in order to reduce their sizes without any functional change. An important
observation is that these reductions do not change substantially the way a BDD, an
FBDD, or an OBDD tests the input variables. This is the reason we can use these
reductions to generalize the notion of variable order to FBDD's.
Merging rule:
If two nonterminal nodes u and v have the same label
v0 and eliminate one of these two nodes and redirect all incoming
edges to the other node. Figure 6 illustrates the application of the merging
rule to type tp(P ) of Figure 5. Observe, that, for each input assignment,
the sequence of variable tests remains invariant w.r.t. to applications of the
merging rule. Moreover, if one considers BDDs as an algebraical structure,
then the application of the merging rule defines a congruence relation on the
set of nodes of the BDD. For this reason sometimes we speak of the merging
rule as of an algebraical reduction.
Deletion rule:
If nonterminal node v, then eliminate v and redirect all incoming
edges to v0. Figure 7 illustrates the application of the deleting rule. A node
on which deletion rule can by applied is called simple reducible. In opposite
to the merging rule the deletion rule decreases the information contained in a
type.
@
@
@
@
@R
@
@
@
@ @R


\Gamma\Psi
'/
\Omega \Omega \Omega \Omega \Omega AE
A
A
A
A AU
\Omega \Omega \Omega \Omega \Omega AE
A
A
A
A AU
Z Z
Z Z Z~
Z Z
Z Z
Z Z Z~
ae
ae
ae
ae
ae
ae ae=
ae
ae
ae
ae
ae
ae
ae=
'/
@
@
@R
\Gamma\Psi
""/
x 400111

Figure

6.
Application of the merging rule to tp(P ) from Figure 5.
Z
Z Z
Z Z Z Z~
Z
Z Z
Z Z
Z Z~
ae
ae
ae
ae
ae
ae
ae=
ae
ae
ae
ae
ae
ae
ae=
'/
""/
@
@
@ @R
\Gamma\Psi
x 400111
Z Z
Z Z Z~
Z Z
Z Z
Z Z Z~
ae
ae
ae
ae
ae
ae ae=
ae
ae
ae
ae
ae
ae
ae=
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta \Thetafl
'/
'/

Figure

7.
Application of the deleting rule to the type - from Figure 6.
(Reduced FBDD's and types.)
A FBDD P is called reduced if neither the merging rule nor the deletion rule can be
applied to P .
or an FBDD P is said to be algebraically reduced if the merging rule can
not be applied to - or to P .
Z Z
Z Z
Z Z Z~
Z
Z Z Z
Z Z Z~
ae
ae
ae
ae
ae
ae ae=
ae
ae
ae
ae
ae
ae
ae=
'/
""/
@
@
@ @R
\Gamma\Psi
red a (tp(P))

Figure

8.
Algebraical reduced type for the type tp(P ) of Figure 5.
Proposition 1. (Unique reduction.)
The reduced FBDD obtained from an FBDD P by applying merging and deletion
rule is uniquely determined and can be computed in linear time. Similarly, the
algebraically reduced FBDD and the algebraically reduced type obtained by applying
the merging rule are uniquely determined and can be computed in linear time.
Proof.
For an FBDD P we denote a reduced FBDD by red(P ), and an algebraical reduced
FBDD by red a (P ). Similar, for a type - we denote by red a (- ) an algebraical reduced
type red a (- ).
First we prove that red a (P ) and red a (- ) are uniquely determined. Two nodes u and
are said to be algebraical congruent (u - a v) if
1.
2. u0 - a v0 and u1 - a v1 (if u and v are inner nodes).
Obviously, - a defines an equivalence relation. Interpreting the left-son-relation
(v0) and the right-son-relation (v1) as unary operations on the set of nodes, the
labels l(v) as unary predicates on the set fx 1 by means of
a few simple axioms, P or - can be considered as an algebra. Now it can be checked
easily that - a is in fact a congruence relation. The factorization over this relation
produces red a (P ) or red a (- ), respectively. This is true since FBDD's or types rooted
in algebraical congruent nodes are isomorphic. Hence, any two merging sequences of
maximal length merge all concruent nodes into a single node and lead to the same
result red a (P ) or red a (- ).
The algebraical idea behind the proof of the uniqueness of red a (P ) and red a (- ) can
not be applied directly to red(P ) since there is a fundamental difference between
the merging and the deletion rule. In terms of universal algebra this difference
can be explained by the fact that the relation - a defined by the merging rule is a
congruence relation while the relation to be defined in the following by means of the
merging and the deletion rule is merely an equivalence relation. Two nodes u and v
of the FBDD P are said to be equivalent (u - v) if
1. u and v are algebraical congruent (u - a v), or
2. one of them is the only successor of the other node in P , or
3. there exist nodes
Observe that neither the deletion rule nor the merging rule does affect the equivalence
of two nodes in P . However, it is clear that any application of the merging
or the deletion rule merges together two different equivalent nodes. It is easy to
see that in order to prove the uniqueness of red(P ) it suffices to prove that P can
be transformed into an FBDD all of whose equivalent nodes are merged together.
The proof can be done easily by induction on the difference between size(P ) and
the number of equivalence classes on P . If this difference is zero, i.e. if there do not
exist two different equivalent nodes in P then we have nothing to merge together. P
is reduced. But if the difference is positive then we can always find two equivalent
nodes which can be merged together by means of the deletion rule or the merging
rule. At the next step we can use the induction hypothesis.
What about the complexity of constructing red(P ), red a (P ) or red a (- ). Reductions
of BDDs were already discussed by Akers [Ake78]. An efficient algorithm for the construction
of red(P ) was developed by Bryant [Bry86]. By the way, OBDD-packages
[e.g. BRB90] do not use separate reduction procedures. However, reduction can be
performed in the average by means of linear many arithmetical operations Finally,
the algorithm of Bryant was improved in [SW92] to run in deterministic linear time
by replacing the sorting procedure by a (linear time) bucket sort technique.
In order to identify FBDD's testing the variables in a similar way it suffices to
compare their types. We define the notion of a subtype in analogy to the notion of
a linear suborder.
Let - be type. A type - 0 is called a subtype of - can be
constructed from - by applying the merging and the deletion rule.
@
@
@
@ @R
@
@
@
@ @R


\Gamma\Psi
\Gamma\Psi
'/
\Omega \Omega \Omega \Omega \Omega AE
A
A
A
A AU
\Omega \Omega \Omega \Omega AE
A
A
A
AU
Z Z Z
Z
Z Z~
Z Z
Z Z
Z Z~
ae
ae
ae
ae
ae
ae=
ae
ae
ae
ae
ae
ae=
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta
'/

Figure

9.
A type - and a subtype - 0 .
It is easy to see that, with respect to -, the set of all types constitutes a partially
ordered set.
(Complete type, FBDD of type - .)
is complete if, on each source-to-sink path, each
variable of X n is tested.
Let - be complete type. An FBDD P is of type - if there exists a type - 0 such that
red a (- 0 red a (- ).
Due to the definition of a type - of an FBDD we can always assume that - is algebraically
reduced. Sometimes, by write -FBDD to indicate an FBDD's to be of a
complete type - . Obviously, a single FBDD can belong to several types. Variable
orderings provide very simply structured complete types the so-called OBDD-types
(for an example see Figure 10). However, in Section 3 it was shown that for important
functions such OBDD-types are not optimal.
To give a more interesting example of a type of an FBDD we deduce the type
of the FBDD PHWB for the hidden weighted bit function HWB
described in Section 3. Since each variable is tested on each source to sink path
- HWB is a complete type. Figure 11 shows - HWB for giving types for
H 1:n (= HWB) and for G 1:n .

Figure

10.
Example of an OBDD-type.
Proposition 2. (Efficient type-check for FBDD's)
Let P be an FBDD P , and let - be a complete type. Then it can be checked efficiently
whether P is of type - .
Proof:
Since the apply algorithm to be presented in Section 5 produces always FBDD's
consistent with the given type, in most practical applications we do not need to
check whether an FBDD belongs to a predefined type. Hence it suffice to scetch an
test whether there exists a type - 0 such that two FBDD's
are of type - 0 [GM92b]. In particular, for
answer the question whether P is of type - .
Each node v of an FBDD or a type can be characterized by the set s v of variables
that are tested on a v-to-sink path. s v can be computed with a straightforward
traverse algorithm in time that is linear in the output. We say that two nodes u
and v are consistent if, for l(u) 6= l(v), it is not the case that l(u) 2 s v as well as
Now, if we run the algorithm synthesis (the apply procedure described in Section 5.2)
taking P 0 and P 00 as inputs then we can check whether the sources of every recursive
call of synthesis are consistent. (Let us remark that in this case the procedure
synthesis needs no input type and can work with any binary Boolean operation
since the resulting FBDD is not of interest.) By induction it can be easily proved
that, all checked pairs of nodes are consistent if and only if there exists a common
@R
\Gamma\Psi
@
@ @R
\Gamma\Psi
@
@
@R
@
@
@R
@
@
@R
@
@
@R
\Gamma\Psi? ?
@
@
\Gamma\Psi
\Gamma\Psi
@
@
\Gamma\Psi
@
@
@R
\Gamma\Psi
@
@
@R
@
@
@R
\Gamma\Psi
A
A
AU
\Deltaff
\Deltaff
A
A
AU
A
A
AU
\Deltaff
@
@
\Gamma\Psi
A
A AU
\Theta
\Theta
\Deltaff
A
A
AU
BN
\Deltaff
\Theta
\Theta
@
@
@R
A
A
AU
BN
\Deltaff
\Theta
\Theta
\Gamma\Psi
A
A AU
BN
\Deltaff
\Theta
\Theta
@
@
@R
@
@
@R
A
A AU
BN
\Deltaff
\Theta
\Theta
\Gamma\Psi
\Gamma\Psi
Z Z
Z
Z Z Z
Z Z
Z Z
Z Z
Z Z Z~
ae
ae
ae
ae
ae
ae
ae
ae
ae
ae
ae
ae
ae
ae
ae=
@
@
@
@
@
@
@
@
@
@
@ @R
A
A
A
A
A
A
A
A
A
A
A AU
\Deltaff

Figure

11.
The type - of the FBDD for the hidden weighted bit
function given in Section 3 given by means of the types for H 1:n (= HWB) and for
G 1:n . (- HWB roots in the source labeled by x 7 .)
Efficient Solutions of the Basic Tasks of Boolean
Manipulation in Terms of FBDD's
5.1 Canonical FBDD Representations
Now we are ready to prove that, with respect to a given complete type, reduced
FBDD's similarly to reduced OBDD's provide a canoncial representation for Boolean
functions. In order to do this we start with the following easy observation.
For each input variable x there exists a BDD that consists of exactly one nonterminal
node labelled by x, a 0-sink, and a 1-sink. Let us call this BDD (it is actually an
OBDD) the standard representation of x.
Proposition 3.
Let - be a complete type over X n , and let x 2 X n . The standard representation of
x is of type - .
Proof:
Since - is a complete type the nodes labelled by x form a cut in - . By means of the
deletion rule we can eliminate all predecessors of the nodes labeled by x in - . After
iterated applications of the merging rule we get a type - 0 such that a single node
labelled by x is the only predecessor of the sink t. Finally, using the deletion rule
we can successively construct from - 0 the standard representation of x.
Theorem 4. (Canonical FBDD representation.)
Let - be a complete type over X n and let f 2 IB n . There is, up to isomorphism,
exactly one reduced FBDD of type - that represents f .
Proof.
There is exactly one complete binary decision tree T for f such that red a (T
red a (- ). Let P be an FBDD for f of type - . It is easy to see that tp(P ) - tp(T ).
Since P and T represent the same Boolean function, P can be constructed from T
by applying the merging and deletion rules. As a consequence of Proposition 1 we
get red(P
As an easy consequence of Theorem 4 and Proposition 1 we obtain an efficient
algorithm that solves the equivalence problem EQU -FBDD
Corollary 5.
EQU -FBDD , the equivalence of two FBDD's P 0 and P 00 of type - can be decided in
linear time O(size(P
Let us mention that the best result for solving EQU FBDD is a probabilistic polynomial
time algorithm [BCW80].
5.2 Efficient Performance of Boolean Synthesis Steps
In the following we show how the efficient APPLY procedure for OBDD's of the
same variable ordering [Bry86] can be extended to FBDD's of the same type. In the
meantime, similar results could be obtained in [SW92].
Theorem 6. (Efficient Boolean synthesis of FBDD's.)
Let   be a binary Boolean operation, and let P 0 , P 00 be two FBDD's of the same
complete type - . An FBDD P of type - representing the Boolean function
can be constructed in time O(size(-
Before proving the Theorem we remark only that in many cases, binary Boolean
synthesis steps for FBDD's can be performed in quadratic instead of cubic time.
This is true for instance if we consider FBDD's of bounded width types or if at least
one of the input FBDD's is large enough (i.e. each variable appears on each source-
to-sink path). Then we can eliminate the factor size(- ) and obtain a time bound
of O(size(P 0 )size(P 00 )). The quadratic upper bound O(size(P 0 )size(P 00 )) can be
obtained also if we do not require as result an FBDD of type - [GM92b]. However,
since also small size FBDD's such as the standard representations (i.e. FBDD's of
size 1) and for certain types - the result of the synthesis can be of size O(size(- ))
there is no hope to eliminate the factor size(- ) from the general upper bound.
Proof:
We start with a brief sketch of the synthesis algorithm.
Algorithm for SY N -FBDD
Input:
- a binary Boolean operation   2 IB
- a complete type
- two FBDD's P 0 and P 00 of type
Output:
- an FBDD P of type - that represents
begin
compute P := red(Q);
return(P
end.
We give now a short recursive description of the procedure synthesis( , - ,
P ) which is a generalization of the apply procedure proposed in [Bry86].
Let top(- ) denote the top variable (the label of the source) of - . Then - j top(-)=ff is
the type rooting in the ff-successor, ff 2 f0; 1g, of the source of - . Similar notations
are used in the case of FBDD's. The terminal case is reached if one of the two input
FBDD's P 0 and P 00 represents a constant. Then the recursion stops, and the output
FBDD can be derived by modifying the sinks of the other FBDD. For instance, if P 0
is 1-sink and  each fi-sink of P 00 has to be replaced by a -
1g.
begin
if (P 0 or P 00 is a sink) /* terminal case */
then return the result; /* the construction of P is straightforward */
else
construct P such that top(P
return(P
For any   2 IB 2 , by means of the classical Shannon expansion applied in the form
each recursion step of synthesis( , - , easily be verified. Let us only
remark that if P 0 and P 00 are of type - then are of type - j x=ff . Since
modifications of the sinks of an FBDD do not change its type we get, as result, an
FBDD P of type - .
To improve the running time we use a global table T of size size(- ) \Theta size(P 0 ) \Theta
us consider the call synthesis( , - 0 , P 0, P 00, Q). Since the restrictions
Qj x=ff have the property that either x = top(Q) or x does not appear in Q the
sources
2 correspond to nodes of - , P 0 and P 00 , respectively. If
synthesis is supported by the table T such that T [v; contains a pointer to the
result of the corresponding synthesis call (or nil if synthesis was not called on these
nodes) we can save much computation and bound the running time by the size of
T .
Let us remark an important property of this straightforward synthesis algorithm.
The procedure synthesis generates as result an FBDD P which is not reduced.
Moreover, each variable appears on each source-to-sink path in P . That is why for
the next call of synthesis applied to P and P new as input (P new is any FBDD of type
- ) we do not need anymore the type - (the information of - is always encoded in
repeated applications of synthesis we get a quadratic upper bound
new )) for the running time. As an example, let us mention that the
FBDD PHWB for the hidden weighted bit function described in Sections 3 encodes
all informations of the type - HWB (Section 4). Hence, working with PHWB we do
not need at all the type - HWB . (For an application we refer to Section 6.)
Finally we remark, that the algorithm presented in the proof of Theorem 6 is not
optimal. The programming techniques used e.g. in the OBDD-package developed
by Brace, Rudell and Bryant [BRB90] can be applied also in the case of FBDD's.
For instance with the help of an appropriate hash table we can force synthesis to
produce only reduced FBDD's. Hence, no reduction algorithm is needed.
6 FBDD's versus OBDD's
Let us start the comparision between the FBDD data structure and the OBDD data
structure with a general remark. Since both data structures provide canonical repre-
sentations, since binary Boolean synthesis steps can be performed, in both cases, in
quadratic time (at least for "large" inputs which is the interesting case in practice),
and since FBDD's provide more - sometimes even exponentially more - concise
representations than OBDD's, in any application that is based on these properties
it makes sense to use FBDD's instead of OBDD's. However, since OBDD's are
especially easily structured FBDD's, and since there is a great variety of reason-able
heuristics [e.g. FS90, BRKM91] for designing efficient OBDD's it seems to be
a meaningful strategy to work with OBDD's as long as they fit into the computer.
Only when OBDD's became too large then one should work with the more efficient
and sophisticated structure of FBDD's.
Before we start to demonstrate the power of the FBDD-concept by showing that the
verification of the circuit design for the hidden weighted bit function HWB given in
[Bry91] can be efficiently carried out in terms of FBDD's let us present some ideas
how to perform efficiently variable quantification in terms of FBDD's.
6.1 FBDD's and variable quantifications. First insights.
Beside of performing two-valued logical synthesis some applications of OBDD's
are based on the possibility of an efficient performance of variable quantification
[e.g. CMB90, Bry92]. For x 2 X n and f 2 IB n variable quantifications are defined
by the identities
Starting with an OBDD for f these operations can be performed by deriving OBDD's
for both restrictions f j x=0 and f j x=1 and carrying out the according Boolean synthesis
step. However, in terms of FBDD's the situation is more difficult. Starting
with an FBDD P for f similarly to the case of OBDD's one can easily construct
the FBDD's P 0 and P 1 for the restrictions f j x=0 and f j x=1 of f by deleting in P
each node v labelled by x and, to obtain P 0 , replacing it by the 0-successor node v0,
or, to obtain P 1 , by the 1-successor node v1. But now we get into trouble. Since,
in general, P 0 and P 1 are not of the same FBDD-type no efficient algorithm for
performing the necessary Boolean synthesis step for P 0 and P 1 is known [GM92b].
Nevertheless there are many and important situations for which, also in terms of
FBDD's, efficient quantification is possible. In the following we describe two paradigmatic
situations.
First let us consider an FBDD P of type - , and let all nodes of - that are labeled
by a variable x are simple reducible (i.e. can be reduced by means of the deletion
rule). Then it is guaranteed that the FBDD's for the restrictions constructed from
P are of the same type. Hence quantification can be performed efficiently similar as
in the case of OBDD's.
In order to illustrate the importance of that observation let us discuss an interesting
application in the verification of switch-level circuits [FMK90]. A modeling method
of a transistor as a switch is as follows: If a switch (transistor) is on, then source
and drain have the same value. Hence, the circuit shown in Figure 12 is modeled as
a switch using propositional logic as
where d is an internal signal.
c
a
d
e

Figure

12.
A transitor-level circuit.
Since d is not observable from outside the circuit, d can be considered to be an existential
quantified variable. To get the relationship of only external signals (a; b; c; e)
the internal signal d must be eliminated. If the logical description of the circuit
(e.g. (1)) is expressed in terms of FBDD's then this operation can be efficiently
implemented if quantification of internal signals can be efficiently performed. Since,
from the very beginning, the external signals are known the following heuristic for
designing well-suited FBDD-types guarantees that quantification of internal signals
can be done efficiently. We separately create
ffl an appropriate FBDD-type - e that is complete with respect to the variables
corresponding to the external signals, and
ffl an appropriate order - i of the variables corresponding to the internal signals.
(Obviously, - i defines an OBDD-type that is complete with respect to the
internal variables.)
Then, starting with - e , a complete FBDD-type - is designed by including as occasion
demands - i piecewise into - e . As a result we get a type where we can quantify, restrict
and compose in the internal variables without problems. Without going into further
details we mention merely that this technique generally can be successfully applied
to all approaches that are based on verifying modularized circuits.
A second more general situation where variable quanitification can be perform efficiently
in terms of FBDD's is the following: Assume the set X n of variables is
partitioned into blocks X . We consider types - that are segmented,
i.e. that consists of segments - r k; such that segment - r starts with exactly
one node and tests the variables from X (r) . See Figure 13 for an example.
if P is an FBDD of a segmented type - then it is easy to see that restricting
simultaneously all variables of a block provides FBDD's that are again of type
- . Hence, due to Theorem 6, the variables of each block can be (simultaneously)
quantified efficiently although in the course of restricting the single variables of a
block, there emerge FBDD's that, in general, are not of type - . Let us mention that
in many application we do not quantify single variables but blocks of variables. For
example, consider any FBDD P of the type - cited in Figure 13. If we restrict x k+1
to 0 and to 1, respectively, then we obtain two inconsistent FBDD's whose types
are incomparable. This is true, since, for the input assigment x
the variable x k+2 ist tested before x k+3 while in P j x k+1 =1 the variable x k+3 ist tested
before x k+2 . Figure 14 shows the type - j x k+1 =0 of P j x k+1 =0 and the type - j x k+1 =1 of
\Deltaff
\Gamma\Psi
A
A
A AU
@
@
@ @R
ae
ae
ae
ae=
ae
ae
ae
ae=
\Omega \Omega \Omega \Omega \Omega \Omega \Omega AE
ae
ae
ae
ae=
Z Z
Z Z~
x
x k+2 x k+3
x k+3 x k+2
x k+4

Figure

13.
Segment of a segmented type - .
\Deltaff
\Gamma\Psi
A
A AU
@
@ @R
ae
ae
ae
ae=
BBN
\Theta
\Theta
\Theta
\Theta
\Theta
Z
Z Z Z~
Z Z
Z Z~
x k+4
x k+2
x k+3
x k+3
x k+2
\Deltaff
\Gamma\Psi
A
A AU
@
@ @R
ae
ae
ae
ae=
BN
\Theta
\Theta
\Theta
\Theta
\Theta
\Theta \Thetafl j
Z Z
Z Z~
Z Z
Z Z~
x k+4
x k+2
x k+3
x k+3
x k+2

Figure

14.
Segments of the restrictions - j x k+1 =0 and - j x k+1 =1 of type - cited in Figure 13.
6.2 The power of FBDD's in circuit verification.
The hidden weighted bit function.
In the following we review a result described in detail in [GM93b] that shows that
the verification of the circuit design proposed by Bryant in [Bry91] for the hidden
weighted bit function HWB can be carried out efficiently in polynomial space using
FBDD's. This demonstrates the power of the FBDD-concept since in [Bry91] it was
shown that working with OBDD's exponential space is needed.
Recall from Section 3 that the hidden weighted bit function HWB can be mathematically
specified by means of the recursive equations:
and
?From the above description an FBDD PHWB for HWB can be derived easily (see
Section 3). Its type - HWB was drawn in Section 4.
The circuit design C for HWB given in [Bry91] leads to a nearly optimal VLSI
implementation of area \Theta time 2 complexity O(n 1+ffl ) for any ffl ? 0. The main idea
of this design is illustrated in Figure 15.
@
@
@
@
@
a a a a a a
a a a a a a666HWBx 1

Figure

15.
Circuit design C for the hidden weighted bit function HWB. The w
the weight of
?From

Figure

it becomes obvious how C looks like for any n 2 IN . For simplicity
we assume 1. In this case log
In
order to verify C in terms of FBDD's of type - HWB we have to construct a reduced
FBDD PC of type - HWB for the function fC computed by C, and then to test its
equivalence (in fact the equality since FBDD-representations of a fixed type are
canonical) with PHWB . For constructing PC we introduce, motivated by the logical
structure of C, a few
satisfy the equation
. The FBDD P cited in Figure 16 exactly
mirrors the main design idea for C. Obviously,
\Omega \Omega \Omega AE
J-
BBBN
\Omega \Omega \Omega AE
\Theta
\Theta
J-
JJ-
\Omega \Omega \Omega AE
J-
\Omega \Omega \Omega AE
\Omega \Omega \Omega AE
J-
\Omega \Omega \Omega AE
J-
\Omega \Omega \Omega AE
J-
\Omega \Omega \Omega AE
J-
Figure

16.
The output function of the circuit of HWB in terms of -FBDD over the primary
inputs and the new internal variables.
let us consider the type - cited in Figure 17. It is easy to see that P is
an FBDD of type - . Now we start to eliminate all internal variables in the order
. We are going to prove that all FBDD's arising in this
elimination process are of small size. Let us mention that, as in the example of
Section 6.1, we can quantify, restrict and compose in the internal variables. Let f i ,
denotes the Boolean function computed by P after the elimination
of . In order to describe f i and its FBDD we consider
the Shannon decomposition of f i in which can be illustrated
by the tree cited in Figure 18.

Figure

17.
Definition of the type - .
\Omega \Omega \Omega AE
J-
BBBN\Omega \Omega \Omega AE
\Theta
\Theta
J-
JJ-
\Omega \Omega \Omega AE
J-\Omega \Omega \Omega AE
\Omega \Omega \Omega AE
J-
\Omega \Omega \Omega AE
J-

Figure

18.
Visualization of the cofactors of the Shannon expansion of f i in the
If wt i
The function f (k)
i can be described easily in the following way. We partition the
set of input variables x 0 denotes the constant
groups of 2 m\Gammai variables
With wt i (x) we choose the appropriate group. k is the offset we need to determine
the output variable. k depends only on w
To extract from C an FBDD PC for its output we do the following. We start with
. Then we construct an FBDD of type - for wm\Gamma1 and eliminate wm\Gamma1 from P
by means of the compose operation. In the second step, by means of the compose
operation, we eliminate in the same manner wm\Gamma2 . At the last step we eliminate
What we get is an FBDD PC of type - HWB for the circuit C. In more detail, we
begin with P construct successively FBDD's for the functions
Under the assumption that we use for each
single synthesis step the programming techniques (hash table, hash-based cash etc.)
presented in [BRB90] then in usual practical implementations the expected space
complexity for extracting PC equals the size of the maximal reduced FBDD derived
for one of the above mentioned functions. Since C computes HWB, and since PC
is a reduced FBDD of type - HWB it is equal to PHWB and, hence, of quadratic size.
That is why the space complexity of the verification has to be at least quadratic.
What about the FBDD-sizes of the functions f i and w i ? In order to estimate the
FBDD-size of the functions f i in the above process it is sufficient to design small
FBDD's of type - for the f (k)
. Using the tree of Figure 18 the size of the resulting
at most a factor of n larger than the size of
such - HWBFBDD for f (k)
Let us mention some useful properties of - HWB . If we exclude the last two levels
(the sink t and its predecessors) each node of - HWB can be labeled by a function G i:j
or H i:j . The source is labelled by H 1:n . We claim that the number of ones we have
tested on any path from H 1:n to H i:j or G i:j equals respectively. Hence, we
can consider - HWB to be a counting schema. The proof of this claim follows easily
by induction on can be a 0-successor, a 1-successor of H i;j+1 or
G i\Gamma1;j , respectively. If the induction hypothesis holds for H i;j+1 and G i\Gamma1;j then it
is true for H i;j and G i;j , too.
An easy consequence of the above mentioned counting property of - HWB is that each
symmetric Boolean function including the functions w i can be realized by means of
FBDD's of type - HWB of at most quadratic size. Now we are going to design an
- HWBFBDD for the f (k)
. Without loss of generality let
us take the, with respect to - , uniquely determined complete decision
tree of f (0)
i of type - HWB . We consider the restrictions of f (0)
i computed on level l.
The number of ones tested on a path from the source to a node on level l labeled by x s
has at most two values. If w is the number of ones for u and v where
then u and v correspond to the same restriction if and only if x w div 2 m\Gammai\Gamma1 has the
same value on the source-to-u and on the source-to-v paths. Altogether the nodes
on level l labeled by x s compute at most four different restrictions. Hence, the
number of restriction on level l is at most 4n and, hence, the size of the - HWBFBDD
for f (0)
i is at most 4n 2 . Analogously we obtain the same upper bound for f (k)
any k. That is why the FBDD of f i has size at most 4n 3 . We remark only that the
size can be further reduced if all similarities between the - HWBFBDD's of f (k)
be merged together.
Altogether it is shown that C can be verified in terms of FBDD's of type - HWB with
low degree polynomial space and time. Since, for principal reasons, this is impossible
in terms of OBDD's this example makes the power of the FBDD-concept evident.
Conclusions
In the paper we extend the feasible manipulation in terms of OBDD's to FBDD's.
In detail we have shown that these
ffl FBDD's provides much more (sometimes even exponentially more) efficient
representations for Boolean functions as OBDD's do (Section 3),
reduced FBDD's of a fixed type provide canonical representations (Theo-
rem 4), and
ffl basic tasks of Boolean manipulation such as performing a Boolean synthesis
step, testing equivalence, satisfiability or tautology can be performed similar
efficiently in terms of FBDD's as in terms of OBDD's (Theorem 6, Corollary
5).
Instead of giving experimental evidence we prove formally for each problem size n
that the benchmark circuit for the hidden weighted bit function proposed in [Bry91]
can be verified in terms of at most cubic size FBDD's (Section 5.2) while it was shown
by Bryant that verification in terms of OBDD's in any case needs exponential space
complexity.
What spellt out to be more difficult to do in terms of FBDD's than in terms of
OBDD's are operations that are based on restrictions (e.g. variable quantification or
composition). However, we have characterized (Section 5) some situations that frequently
occure in practical applications for which these operations can be performed
efficently in terms of FBDD's, too.
An open and interesting problem is to develop heuristics for creation good types.
Of course, this is an extension of the problem of determining good variable orders
for OBDD applications. Since there is much greater freedom to define types than
to define orders this problem seems to be very trickery. However, all what is know
about OBDD's can be used if working with FBDD's. For example, a useful strategy
to work with FBDD's is to work with OBDD's (as extremely easy structed
FBDD's) as long as the OBDD's under consideration fit into the computer. Only
when OBDD's became to large then one should (try to) work with the more efficient
and sophisticated FBDD's.



--R

Binary Decision Diagrams
Boolean Satisfiability and Equivalence Checking Using General Binary decision Diagrams
Synthesis for Testability: Binary decision Diagrams
Equivalence of Free Boolean Graphs Can Be Decided Probabilistically in Polynomial Time

Efficient Implementation of a BDD Package

On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Applications to Integer Multipli- cation
Symbolic Boolean Manipulation with Ordered Binary decision Diagrams

Symbolic Model Checking: states and beyond
Sequential Circuit Verification Using Symbolic Model Checking
Efficient Verification of Multiplier and Other Different Functions Using IBDDs
Heuristics to Compute Variable Orderings for Efficient Manipulation of Ordered Binary decision Diagrams

Verifying Temporal Properties of Sequential Machines without Building Their State Diagrams
Verifikation digitaler Systeme
The Complexity of Equivalence and Containment for Free Single Program Schemes
Evaluation and Improvements of Boolean Comparison Method Based on Binary decision Diagrams
A Method for Symbolic Verification of Sunchronous Circuits
Automatic and Semi-Automatic Verification of Switch-Level Circuits with Temporal Logic and Binary decision Diagrams
Finding the Optimal Variable Ordering for Binary decision Diagrams
Computers and Intractability
Analysis and Manipulation of Boolean Functions in Terms of decision Graphs
Efficient Analysis and Manipulation of OBDD's Can Be Extended to Read-once-only Branching Programs
Frontiers of Feasible and Probabilistic Feasible Boolean Manipulation with Branching Programs
Combinational Logic Verification with FBDD's
Functional Partitioning for Verification and Related Problems
Extended BDD's
Using if-then-else DAGs for Multi-Level Logic Minimization
PLATO: A Tool for Computation of Exact Signal Probabilities

Modified Branching Programs and Their Computational Power
Branching Programs - An Efficient Data Structure for Computer-Aided Circuit Design
Logic Verification Using Binary decision Diagrams in a Logic Synthesis Environ- ment
Graph Driven BDDs - A New Data Structure for Boolean Functions
The Complexity of Boolean Functions
--TR
Graph-based algorithms for Boolean function manipulation
Modified branching programs and their computational power
Finding the Optimal Variable Ordering for Binary Decision Diagrams
Using if-then-else DAGs for multi-level logic minimization
On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication
Efficient implementation of a BDD package
Sequential circuit verification using symbolic model checking
Shared binary decision diagram with attributed edges for efficient Boolean function manipulation
Heuristics to compute variable orderings for efficient manipulation of ordered binary decision diagrams
Symbolic Boolean manipulation with ordered binary-decision diagrams
Boolean Satisfiability and Equivalence Checking Using General Binary Decision Diagrams
The Complexity of Equivalence and Containment for Free Single Variable Program Schemes
Synthesis for Testability
Frontiers of Feasible and Probabilistic Feasible Boolean Manipulation with Branching Programs
Analysis and Manipulation of Boolean Functions in Terms of Decision Graphs
Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams
Gate-Delay-Fault Testability Properties of Multiplexor-Based Networks

--CTR
J. Jain , K. Mohanram , D. Moundanos , I. Wegener , Y. Lu, Analysis of composition complexity and how to obtain smaller canonical graphs, Proceedings of the 37th conference on Design automation, p.681-686, June 05-09, 2000, Los Angeles, California, United States
Chunghee Kim , Luciano Lavagno , Alberto Sangiovanni-Vincentelli, Free MDD-based software optimization techniques for embedded systems, Proceedings of the conference on Design, automation and test in Europe, p.14-19, March 27-30, 2000, Paris, France
Sieling , Ingo Wegener, A Comparison of Free BDDs and Transformed BDDs, Formal Methods in System Design, v.19 n.3, p.223-236, November 2001
Olaf Schrer , Ingo Wegener, The Theory of Zero-Suppressed BDDs and the Number of Knights Tours, Formal Methods in System Design, v.13 n.3, p.235-253, Nov. 1998
Wolfgang Gnther , Rolf Drechsler, Efficient manipulation algorithms for linearly transformed BDDs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.50-54, November 07-11, 1999, San Jose, California, United States
R. Drechsler , A. Sarabi , M. Theobald , B. Becker , M. A. Perkowski, Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams, Proceedings of the 31st annual conference on Design automation, p.415-419, June 06-10, 1994, San Diego, California, United States
Sieling, The complexity of minimizing and learning OBDDs and FBDDs, Discrete Applied Mathematics, v.122 n.1-3, p.263-282, 15 October 2002
Wolfgang Gnther , Rolf Drechsler, Minimization of free BDDs, Integration, the VLSI Journal, v.32 n.1-3, p.41-59, November 2002
Wolfgang Gnther , Rolf Drechsler, Efficient Minimization and Manipulation of Linearly Transformed Binary Decision Diagrams, IEEE Transactions on Computers, v.52 n.9, p.1196-1209, September
Jayram S. Thathachar, On separating the read-k-times branching program hierarchy, Proceedings of the thirtieth annual ACM symposium on Theory of computing, p.653-662, May 24-26, 1998, Dallas, Texas, United States
Christoph Meinel , Anna Slobodov, A Unifying Theoretical Background for Some Bdd-based Data Structures, Formal Methods in System Design, v.11 n.3, p.223-237, Oct. 1997
Beate Bollig, A very simple function that requires exponential size nondeterministic graph-driven read-once branching programs, Information Processing Letters, v.86 n.3, p.143-148, 16 May
Bogdan J. Falkowski , Chip-Hong Chang, Forward and Inverse Transformations Between Haar Spectra and Ordered Binary Decision Diagrams of Boolean Functions, IEEE Transactions on Computers, v.46 n.11, p.1272-1279, November 1997
Jawahar Jain , William Adams , Masahiro Fujita, Sampling schemes for computing OBDD variable orderings, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.631-638, November 08-12, 1998, San Jose, California, United States
Henrik Reif Andersen , Henrik Hulgaard, Boolean expression diagrams, Information and Computation, v.179 n.2, p.194-212, December 15, 2002
Amit Narayan , Jawahar Jain , M. Fujita , A. Sangiovanni-Vincentelli, Partitioned ROBDDsa compact, canonical and efficiently manipulable representation for Boolean functions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.547-554, November 10-14, 1996, San Jose, California, United States
Randal E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.236-243, November 05-09, 1995, San Jose, California, United States
Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
Adnan Darwiche, A compiler for deterministic, decomposable negation normal form, Eighteenth national conference on Artificial intelligence, p.627-634, July 28-August 01, 2002, Edmonton, Alberta, Canada
Stephen Ponzio, A lower bound for integer multiplication with read-once branching programs, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.130-139, May 29-June 01, 1995, Las Vegas, Nevada, United States
Beate Bollig , Stephan Waack , Philipp Woelfel, Parity graph-driven read-once branching programs and an exponential lower bound for integer multiplication, Theoretical Computer Science, v.362 n.1, p.86-99, 11 October 2006
Ingo Wegener, BDDs: design, analysis, complexity, and applications, Discrete Applied Mathematics, v.138 n.1-2, p.229-251, 29 March 2004
Adnan Darwiche, Decomposable negation normal form, Journal of the ACM (JACM), v.48 n.4, p.608-647, July 2001
Rina Dechter , Robert Mateescu, AND/OR search spaces for graphical models, Artificial Intelligence, v.171 n.2-3, p.73-106, February, 2007
tautology test;data structure;satisfiability test;OBDD;circuit design;total computation;equivalence test;data structures;canonical representations;boolean manipulation;boolean functions;logic design;boolean function manipulation