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

概要

論文の詳細を見る
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.
2012-08-31