Counterexamples to the long-standing conjecture on the complexity of BDD binary operations

• Yoshinaka, Ryo

• Kawahara, Jun

• Denzumi, Shuhei

• Arimura, Hiroki

• Minato, Shin-ichi

Bibliographic Information

Other Title

• Vertex angle and crossing angle resolution of leveled tree drawings

Abstract

In this article, we disprove the long-standing conjecture, proposed by R.E. Bryant in 1986, 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 ⋀, ⋁, and ⊕. For the operations ⋀ and ⋁, 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.

Journal

• Information Processing Letters

  Information Processing Letters 112 (16), 636-640, 2012-08-31

  Elsevier B.V.

Keywords

• Analysis of algorithms
• Binary decision diagram
• Data structures

Details

• CRID: 1050564288965341056
• NII Article ID: 120004710971
• DOI: 10.1016/j.ipl.2012.05.006
• HANDLE: 2115/50105
• ISSN: 00200190
• Web Site: https://api.elsevier.com/content/article/PII:S0020019012001299?httpAccept=text/xml
• Web Site: https://api.elsevier.com/content/article/PII:S0020019012001299?httpAccept=text/plain
• Text Lang: en
• Article Type: journal article
• Data Source:
  • IRDB
  • Crossref
  • CiNii Articles
  • KAKEN