On the descriptive and algorithmic power of parity ordered binary decision diagrams

Abstract

The main result of this paper is a polynomial time algorithm that minimizes the number of nodes in a parity OBDD (ordered binary decision diagram). Moreover, we prove that the synthesis and the equivalence test for +OBDDs, which are the fundamental operations for circuit verification, have polynomial time deterministic solutions. We conclude that it takes deterministic polynomial time to decide whether the parity of clauses/implicants is satisfiable. Several functions typically used as examples in theory, e.g., the indirect storage access function, have exponential OBDD-size but are of polynomial size if +OBDDs are used. (C) 2001 Academic Press.