BDDs provide an established technique for propositional formula manipulation. In this paper we re-develop the basic BDD theory using 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. For this rewriting system a {em layerwise strategy is proposed having the same time complexity as the traditional algorithm, and a {em lazy strategy sometimes performing much better than the traditional algorithm.

, ,
CWI
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

van de Pol, J., & Zantema, H. (2000). Binary decision diagrams by shared rewriting. Software Engineering [SEN]. CWI.