Ordered binary decision diagrams (OBDDs) nowadays belong to the most common representation types for Boolean functions. Although they allow important operations such as satisfiability test and equality test to be performed efficiently, their limitation lies in the fact that they may require exponential size for important functions. Bryant [8] has shown that any OBDD-representation of the function MUL{sub}(n－1,n), which computes the middle bit of the product of two n-bit numbers, requires at least 2{sup}(n/8) nodes. In this paper a stronger bound of 2{sup}(n/2) / 61 is proven by a new technique, using a recently found universal family of hash functions [23]. As a result, one cannot hope anymore to find reasonable small OBDDs even for the multiplication of relatively short integers, since for only a 64-bit multiplication millions of nodes are required. Further, a first non-trivial upper bound of 7/3·2{sup}(4n/3) for the OBDD size of MUL{sub}(n－1,n) is provided.
展开▼
