Abstract of Paper

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

Abstract:

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.