Binary decision diagram

Definition

Let $x_1, \dots, x_n$ be Boolean variables. A binary decision diagram over $x_1, \dots, x_n$ is a finite acyclic directed graph with one root such that:

1. each terminal node has no outgoing edge and carries a label $0$ or $1$;
2. each other node $v$ carries a variable index $i(v) \in \set{1, \dots, n}$ and has exactly two outgoing edges, to its low child and its high child.

It represents the Boolean function $f \colon \set{0, 1}^n \to \set{0, 1}$ defined as follows. For $a \in \set{0, 1}^n$, start at the root. At each non-terminal node $v$, move to its high child if $a_{i(v)} = 1$ and to its low child if $a_{i(v)} = 0$. Then $f(a)$ is the label of the terminal node reached.

The diagram is ordered if $i(u) < i(v)$ whenever $v$ is a non-terminal node reached from a non-terminal node $u$ by a directed path of positive length. An ordered diagram is reduced if no non-terminal node has equal low and high children, and no two distinct terminal nodes have the same label. It must also have no two distinct non-terminal nodes with the same index, the same low child and the same high child.