 Reduced ordered binary decision diagram

An ordered binary decision diagram with shared equal terminal nodes, no decision node having identical zero and one children, and no two decision nodes having the same tested Boolean variable and the same ordered pair of children. For a fixed variable ordering of a binary decision diagram, it is unique up to labelled graph isomorphism: each nonconstant remaining Boolean cofactor has a uniquely determined first essential Boolean variable, and its two children are recursively determined by its zero and one Boolean cofactors. This uniqueness does not compare different orderings.