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.

A fixed order in which Boolean variables may be tested along each branch of an ordered binary decision diagram. Branches may skip a test, but cannot reverse the order. The order can change the number of distinct remaining Boolean cofactors and therefore the size of the representation.