Ordered Binary Decision Diagrams (OBDDs, in short) are well-known to be useful
representations for Boolean functions and applied in various fields such as design
and formal verification of digital systems, combinatorics, and Artificial Intelligence
(AI). One of difficulties in conventional method to construct OBDDs is that the
target OBDD cannot be obtained when some intermediate OBDDs blow up, even
if the size of the target is moderate. A breadth first algorithm is proposed to
resolve this difficulty by constructing the target OBDD directly in a top-down
fashion. Though this algorithm can construct OBDDs in an output-size sensitive
manner, it requires efficient strategy for equivalence test between subfunctions
which is intractable in general. Thus, it might be important to investigate how
this equivalence test is hard in several settings.
We adopt maximal independent sets of a graph as an important and suggestive
special case from the viewpoints of graph theory and Boolean function theory. We
show hardness in a direct application of the breadth first algorithm to the maximal
independent sets of a graph. On the other hand, we show that this algorithm can
be applied efficiently to the class of monotone Conjunctive Normal Forms (CNFs)
or Disjunctive Normal Forms (DNFs). As a counter example of the hardness, it is
shown that we can construct the OBDD of maximal independent sets of a mesh
graph in an output-size sensitive manner by combining the breadth first algorithm
and conventional algorithm, where we compute the logical conjunction of the two
OBDDs of independent sets and dominating sets.
Then we discuss relationship between the two OBDDs of a monotone function
and of the set of its prime implicants by comparing their subfunctions based on the
fact that the characteristic function of independent sets is monotone and that the
family of all the maximal independent sets can be considered as the set of all the
prime implicant of that function. As a result we show that there exists a monotone
function which has an O(n) size DNF but can not be represented by a polynomial
size OBDD. In other words, we cannot obtain the OBDD of the set of all the prime
implicants of a monotone function in an output-size sensitive manner once we have
constructed the OBDD of that function in worst case. This fact is also a solution
to open questions by Coudert who has given an implicit method to compute the
set of prime implicants of a Boolean function by using OBDDs.