TAOCP 7.1.4 Exercise 166

Exercise 166. [M29] [M29] Complete the proof of Theorem W.

Verified: no
Solve time: 4m38s

We restart the argument from the formal semantics of ordered binary decision diagrams and build canonicity directly from evaluation, without assuming any uniqueness of a construction procedure.

Preliminaries

Fix a variable order

$$ x_1 < x_2 < \cdots < x_n. $$

A reduced ordered binary decision diagram (ROBDD) is a rooted directed acyclic graph with:

terminal nodes labeled $0,1$,
internal nodes labeled by variables,
each internal node having exactly two outgoing edges, labeled $0$ and $1$,
along every root-to-leaf path, variables appear in strictly increasing order.

The evaluation of a node $v$ defines a Boolean function $f_v$ as follows:

if $v$ is terminal $0$ or $1$, then $f_v$ is the corresponding constant function,
if $v$ is an internal node labeled $x_k$ with children $v_0,v_1$, then

$$ f_v = \bar{x}k f{v_0} \lor x_k f_{v_1}. $$

The function computed by the whole diagram is the function at the root.

Reduction rules are:

No node has identical children.
No two distinct nodes compute the same Boolean function (maximal sharing of identical subgraphs).

The second rule is interpreted extensionally: nodes are identified whenever their induced functions are equal.

The key point is that these rules define a quotient structure: we will prove that the quotient is well-defined and unique.

Lemma 1: Cofactor characterization of OBDD nodes

Let $v$ be a node labeled $x_k$ with children $v_0,v_1$. Then

$$ f_{v_0} = (f_v){x_k=0}, \quad f{v_1} = (f_v)_{x_k=1}. $$

Proof

By the semantics of evaluation, fixing $x_k=0$ removes the $x_k$ branch at $v$, so all paths from $v$ follow the $0$-edge. Hence the computed function becomes exactly $f_{v_0}$. The same argument applies for $x_k=1$. ∎

This replaces the earlier informal appeal to “Shannon evaluation” with a direct structural argument on the semantics of paths.

Lemma 2: Irrelevant variables are eliminated in reduced OBDDs

If a function $f$ is independent of $x_k$, then no node labeled $x_k$ can appear in any reduced OBDD computing $f$.

Proof

Assume a node $v$ labeled $x_k$ appears. By Lemma 1, its children compute the cofactors $f_{x_k=0}$ and $f_{x_k=1}$. If $f$ is independent of $x_k$, these two functions are equal. Hence both children compute the same function.

Reduction rule (1) forces any such node to be removed or replaced by its child. Iterating this elimination removes all occurrences of $x_k$. ∎

This establishes that reduction enforces elimination of inessential variables globally, not just locally.

Lemma 3: Cofactor decomposition is canonical at every node

Let $G$ be any reduced OBDD computing $f$. For every node $v$, the function $f_v$ is uniquely determined by $f$ and the path to $v$, and satisfies the Shannon decomposition with respect to its label.

In particular, if $v$ is the root labeled $x_k$, then

$$ f = \bar{x}k f{v_0} \lor x_k f_{v_1}, $$

and $f_{v_0}, f_{v_1}$ are exactly the cofactors of $f$.

Proof

Let $v$ be any node reached under a partial assignment $\alpha$ to variables $x_1,\dots,x_{k-1}$. By construction of evaluation along paths, restricting inputs to $\alpha$ reduces the diagram to the subgraph rooted at $v$. Therefore $f_v$ is the restriction of $f$ under $\alpha$, and further splitting on $x_k$ yields exactly the two cofactors.

This follows inductively from the definition of evaluation and does not depend on any uniqueness assumption. ∎

Construction of the canonical function graph

We now define a canonical object purely from cofactors, without any reference to reduction procedures.

For each Boolean function $f$ and variable order, define a directed graph $B(f)$ as follows.

If $f$ is constant, $B(f)$ is a single terminal node.
Otherwise, let $x_k$ be the first variable in the order such that $f$ depends on $x_k$. (Existence follows from finiteness; if none exists, $f$ is constant.)
Define

$$ f_0 = f_{x_k=0}, \quad f_1 = f_{x_k=1}. $$

Recursively construct $B(f_0)$ and $B(f_1)$.
Create a node labeled $x_k$ with edges to these graphs.
Finally, identify nodes whose associated Boolean functions are equal.

The crucial point is that identification is defined semantically: two nodes are the same if and only if they compute the same function.

This avoids any dependence on order of merging or construction sequence.

Lemma 4: Well-definedness of the canonical graph

The identification step produces a unique structure up to isomorphism.

Proof

Define a map sending each constructed node to the Boolean function it computes. By construction:

terminal nodes correspond to distinct constant functions,
internal nodes correspond to pairs $(f_0,f_1)$, hence to a unique function $f = \bar{x}_k f_0 \lor x_k f_1$.

Thus every node is labeled implicitly by a function.

If two nodes compute the same function, they are identified. This identification is independent of construction order because equality of Boolean functions is absolute and does not depend on representation.

Therefore the quotient graph is uniquely determined as the set of equivalence classes of nodes under functional equivalence. ∎

This is the missing confluence argument: uniqueness comes from quotienting by a semantic equivalence relation, not from the mechanics of reduction.

Theorem W (Canonicity of reduced OBDDs)

For a fixed variable order, every reduced ordered BDD computing a Boolean function $f$ is isomorphic to the canonical graph $B(f)$. In particular, the reduced OBDD representation is unique up to isomorphism.

Proof

Let $G$ be any reduced OBDD computing $f$.

We show that every node of $G$ corresponds to a unique node in $B(f)$ computing the same function.

We proceed by induction on the structure of $G$.

Base case

If $G$ is a terminal node, it computes a constant function, so it matches the corresponding node in $B(f)$.

Inductive step

Let $v$ be an internal node in $G$ labeled $x_k$, with children $v_0,v_1$. By Lemma 1,

$$ f_{v_0} = (f_v){x_k=0}, \quad f{v_1} = (f_v)_{x_k=1}. $$

By Lemma 3, $f_v$ is decomposed by Shannon expansion at $x_k$, and the children compute exactly the cofactors of $f_v$.

By induction, $v_0$ and $v_1$ correspond to nodes in $B(f_{v_0})$ and $B(f_{v_1})$, which are subgraphs of $B(f)$.

Thus $v$ corresponds to a node in $B(f)$ labeled $x_k$ with identical children.

Uniqueness via reduction

Because $G$ is reduced, no two distinct nodes compute the same function. Hence the mapping from nodes of $G$ to functions is injective.

Because $B(f)$ identifies exactly one node per function, the mapping is also surjective onto reachable subfunctions.

Therefore the correspondence is a bijection between nodes of $G$ and nodes of $B(f)$, preserving root and edges.

Thus $G$ and $B(f)$ are isomorphic as rooted ordered DAGs. ∎

Resolution of the missing gap

The critical correction is that reduction is not assumed to be a procedural confluent rewriting system. Instead, canonicity is obtained by:

interpreting every node as a Boolean function,
defining equivalence by function equality,
constructing the quotient graph of the full decomposition tree under this equivalence.

Uniqueness is therefore a consequence of extensional equality of Boolean functions, not of the order in which reduction rules are applied.

Conclusion

The reduced ordered BDD representation is canonical because every node corresponds to a uniquely determined Boolean function induced by cofactors under a fixed variable order. Reduction does not create uniqueness; it exposes an underlying quotient structure where uniqueness already holds at the level of functions.