Binary decision diagrams by shared rewriting
J.C. van dePol, Hans Zantema · 2000
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 layerwise strategy is proposed having the same time complexity as the traditional algorithm, and a lazy strategy sometimes performing much better than the traditional algorithm. 1991 Mathematics Subject Classification: 03B05 1991 ACM Computing Classification System: B.7.1, E.2, F4.2 Keywords and Phrases: binary decision diagrams, decision trees, term rewriting, sharing Note: Work carried out under project SEN2 1. Introduction Equivalence checking and satisfiability testing of propositional formulas are basic but hard problems in many applications, including hardware verification [6] and symbolic model checki...