×

zbMATH — the first resource for mathematics

Counterexamples to the long-standing conjecture on the complexity of BDD binary operations. (English) Zbl 1248.68265
Summary: In this article, we disprove the long-standing conjecture, proposed by R. E. Bryant in [IEEE Trans. Comput. 35, 677–691 (1986; Zbl 0593.94022)], that his binary decision diagram (BDD) algorithm computes any binary operation on two Boolean functions in linear time in the input-output sizes. We present Boolean functions for which the time required by Bryant’s algorithm is a quadratic of the input-output sizes for all nontrivial binary operations, such as \(\land\), \(\lor\), and \(\oplus\). For the operations \(\land\) and \(\lor\), we show an even stronger counterexample where the output BDD size is constant, but the computation time is still a quadratic of the input BDD size. In addition, we present experimental results to support our theoretical observations.

MSC:
68Q25 Analysis of algorithms and problem complexity
68P05 Data structures
68W40 Analysis of algorithms
06E30 Boolean functions
68R10 Graph theory (including graph drawing) in computer science
Software:
CUDD
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bryant, R.E., Graph-based algorithms for Boolean function manipulation, IEEE trans. comput., C-35, 8, 677-691, (1986) · Zbl 0593.94022
[2] Knuth, D.E., The art of computer programming, vol. 4, fasc. 1, bitwise tricks & techniques; binary decision diagrams, (2009), Addison-Wesley · Zbl 1178.68372
[3] S. Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, in: Proc. of 30th ACM/IEEE Design Automation Conference (DACʼ93), 1993, pp. 272-277.
[4] Shannon, C.E., A symbolic analysis of relay and switching circuits, Trans. AIEE, 57, 713-723, (1938)
[5] Somenzi, F., CUDD: CU decision diagram package, (accessed November 4, 2011)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.