A rewriting approach to binary decision diagrams

BDDs provide an established technique for propositional formula ma-nipulation. In this paper we present the basic BDD theory by means of standard rewriting techniques. Since a BDD is a DAG instead of a tree we need a notion of shared rewriting and develop appropriate theory. A rewriting system is presented by which canonical ROBDDs can be obtained and for which uniqueness of ROBDD representation is proved. Next, an alternative rewriting system is presented suitable for actual computing ROBDDs from formulas. For this rewriting system a layerwise strategy is defined, and it is proved that when replacing the classical apply-algorithm by layerwise rewriting, the same complexity bound is reached as in the clas-sical algorithm. Moreover, a layenIJise innermost strategy is defined and it is proved that the full classical algorithm for computing ROBDDs can be replaced by layerwise innermost rewriting without ·affecting the com-plexity. Finally a lazy strategy is proposed sometimes performing much better than the traditional algorithm.