Binary decision diagram

A Directed acyclic graph representing a Boolean function. A decision node tests a Boolean variable and has zero and one successors; evaluation follows the corresponding arrows until a terminal node returns a Boolean value. Sharing subgraphs can make a binary decision diagram much smaller than a binary decision tree.

A vertex that returns a final output rather than performing another test. In a binary decision diagram the two possible outputs are the Boolean constants zero and one.

An internal vertex that tests a condition and selects an outgoing branch. In a binary decision diagram, a decision node tests a Boolean variable and has one zero arrow and one one arrow.

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.