Abstract of Paper

Binary Decision Diagrams by Shared Rewriting
by Jaco van de Pol and Hans Zantema


BDDs provide an established technique for propositional formula
manipulation. In this paper we propose a uniform description of basic BDD
theory and algorithms by means of term rewriting.  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 forms
can be obtained. Various reduction strategies give rise to different
algorithms.  A {\em layerwise} strategy is proposed having the same time
complexity as the traditional {\em apply}-algorithm, and the {\em lazy}
strategy is studied, which resembles the existing {\em up-one}-algorithm. We
show that the performance of these algorithms is incomparable.