On the Descriptive and Algorithmic power of Parity Ordered Binary Decision Diagrams

摘要

We present a data structure for Boolean functions, which we call Parity-OBDDs or POBDDs, which combines the nice algorithmic properties of the well-known ordered binary decision diagrams (OBDDs) with a considerably larger descriptive power. Beginning from an algebraic characterization of the POBDD-complexity we prove in particular that the minimization of the number of nodes, the synthesis, and the equivalence test for POBDDs, which are the fundamental operations for circuit verification, have efficient deterministic solutions. Several functions of pratical interest, i.e. the storage access function, have exponential ODBB-size but are of polynomial size if POBDDs are used.