OBDD, ordered binary decision diagram, ein binärer EntscheidungsgraphG = (V, E, index), der über Booleschen Variablen x₁,…, x_n definiert ist und für den \begin{eqnarray}index(u)\lt index(\upsilon )\end{eqnarray} für jede Kante (u, v) ∈ E gilt, bei der v kein Blatt ist. Hierbei ist < eine lineare Ordnung auf {x₁,…, x_n}. Die lineare Ordnung < wird Variablenordnung des OBDD genannt. In einem OBDD tritt auf jedem Pfad von der Wurzel zu einem Blatt jede Variable höchstens einmal auf, und zwar in der durch die Variablenordnung < vorgegebenen Reihenfolge.