ECCC-Report TR00-013https://eccc.weizmann.ac.il/report/2000/013Comments and Revisions published for TR00-013en-usMon, 06 Mar 2000 13:03:44 +0200
Paper TR00-013
| Algebraic and Uniqueness Properties of Parity Ordered Binary Decision Diagrams and their Generalization |
Daniel Král
https://eccc.weizmann.ac.il/report/2000/013Ordered binary decision diagrams (OBDDs) and parity ordered binary
decision diagrams have proved their importance as data structures
representing Boolean functions. In addition to parity OBDDs we study
their generalization which we call parity AOBDDs, give the algebraic
characterization theorem 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 creating the form which satisfies
the uniqueness conditions for parity OBDDs running in time $O(S^3)$ and
for parity AOBDDs running in time $O(nS^3)$ are presented ($n$ is
the number of variables, $S$ is the number of vertices); both
the algorithms are quite simple.
All the results are also extended to case of shared parity OBDDs and
shared parity AOBDDs --- data structures for representation of Boolean
function sequences.
Mon, 06 Mar 2000 13:03:44 +0200https://eccc.weizmann.ac.il/report/2000/013