Abstract of Paper

Algebraic and Uniqueness Properties of Parity Ordered Binary Decision Diagrams and their Generalization
by Daniel Kral

Abstract:

Ordered binary decision diagrams (OBDDs) and parity ordered binary
binary decision diagrams are important data structures representing
Boolean functions.  In addition to parity OBDDs, we study their
generalization which we call parity AOBDDs and we give the algebraic
characterization theorem for parity AOBDDs and compare their minimal
size to the size of parity OBDDs.

We prove that the constraint that no arcs test conditions of type
$x_i=0$ does not affect the node-size of parity (A)OBDDs and we give an
efficient algorithm for finding node-minimal parity (A)OBDDs with this
additional constraint.  We define so-called uniqueness conditions, use them
to obtain a canonical form for parity OBDDs and discuss similar results for
parity AOBDDs.
 
Algorithms for minimization and transformation to the form which satisfies
the uniqueness conditions for parity OBDDs running in time $O(S^3)$ and
space $O(S^2)$ or in time $O(S^3/log S)$ and space $O(S^3/log S)$ and for
parity AOBDDs running in time $O(nS^3)$ and space $O(nS^2)$ or in time
$O(nS^3/log S)$ and space $O(nS^3/log S)$ are presented ($n$ is the number
of variables, $S$ is the number of vertices).

All the results are also extended to case of shared parity (A)OBDDs --- data
structures for representation of Boolean function sequences.