Binary Decision Diagrams by Shared Rewriting. Software Engineering

摘要

BDDs provide an established technique for propositional formula manipulation. In this paper the authors 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 proposed having the same time complexity as the traditional algorithm, and a lazy strategy sometimes performing much better than the traditional algorithm.