= Reduced ordered binary decision diagram
= ROBDD
{c}
{synonym}
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.
Back to article page
