Improving the efficiency of BDD-based operators by means of partitioning

Binary decision diagrams (BDD's) are a state-of-the-art core technique for the symbolic representation and manipulation of Boolean functions, relation s and finite sets. Many computer-aided design (CAD) applications resort to them, but size and time efficiency restrict their applicability to medium-s mall designs. We concentrate on complex operators used in symbolic manipulation. We analy ze and optimize their performance by means of new dynamic partitioning stra tegies. We propose a novel quick algorithm for the estimation of cofactor s ize, and a technique to choose splitting variables according to their discr imination power, so that their cofactors may be optimized by different vari able orderings (tending to the more flexible FBDD's), Furthermore, we analy ze time efficiency and the impact of hashing/caching on BDD-based operators , We finally include an experimental observation of memory usage and runnin g time for operators applied in symbolic manipulation.