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

AbstractThe 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