Reduced Ordered Binary Decision Diagram

Building an ROBDD

Let's trace the construction and reduction of an ROBDD for the Multiplexer function (x ? y : z) with variable order xyz. The function evaluates to y when x is true, and z when x is false.

1. First, we evaluate the function for all 8 possible assignments of (x, y, z).
2. We construct a full binary tree with variable x at the root, y at the next level, and z at the bottom level.
3. For the left sub-tree where x = false, the function value only depends on z. Thus, nodes at the y level on this side will have identical left and right children (because the value of y doesn't matter). These y nodes are eliminated.
4. For the right sub-tree where x = true, the function value only depends on y. The z nodes on this side will evaluate to the same terminal regardless of z, so they are eliminated.
5. Finally, identical subgraphs are merged. In the end, the graph is reduced to only 3 nonterminal nodes: one for x, one for y, and one for z.

Expected result: 3 Nonterminal nodes, 2 decisions for evaluating x=false, y=true, z=true (mask 3).

Interactive Experiment

You can experiment with different variable orders and functions using the interactive module athttps://riano.app/module/reduced-ordered-binary-decision-diagram.

1. Set Function to "Multiplexer".
2. Set Variable order to "xyz". Observe that the graph has 3 nonterminal nodes.
3. Change the Variable order to "zxy". Observe that the number of nonterminal nodes increases to 4.
4. Set Function to "Parity" and observe the symmetric structure.
5. Change Assignment mask to "3" (which sets x=false, y=true, z=true in xyz order depending on binary representation) and follow the highlighted path to the terminal node.

Limitations

While an ROBDD provides a canonical representation of a Boolean function for a fixed variable order, finding the optimal variable order that minimizes the number of nodes is an NP-hard problem. Additionally, some functions, such as integer multiplication, require an exponential number of nodes regardless of the chosen variable order.

Boundary case: Constant functions like "Zero" or "One" do not depend on any variables. Their ROBDD representation reduces entirely to a single terminal node, containing 0 nonterminals.

References

The original algorithm for constructing ROBDDs and manipulating them efficiently was detailed by R.E. Bryant:

• Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams (R.E. Bryant, 1992)