TAOCP 7.1.4 Exercise 180

Exercise 180. [M27] [M27] Prove Theorem Y, using the hint given in the text.

Verified: yes
Solve time: 3m52s

We restate the intended theorem in a form that matches the BDD semantics used in Section 7.1.4.

Let $G$ be a binary decision diagram (BDD) with root $r$, terminal nodes $0$ and $1$, and each nonterminal node $v$ labeled by a variable $x_i$. Each outgoing edge of $v$ corresponds to assigning $x_i = 0$ or $x_i = 1$. A root-to-terminal path therefore induces a complete assignment, and it is called feasible if it ends in terminal $1$.

Theorem Y

Algorithm B enumerates exactly the root-to-$1$ paths of the BDD $G$, and outputs each such path once.

Proof

The proof follows the hint: we use induction on the structure of the BDD as explored by the recursion of Algorithm B, maintaining a precise invariant about the relationship between recursion state and BDD nodes.

Invariant

We maintain the following invariant for every recursive call of Algorithm B:

The call is associated with a node $v$ of the BDD together with a partial assignment $P$ such that $P$ is exactly the set of variable assignments recorded along the unique directed path from the root $r$ to $v$.

This invariant holds initially because the algorithm starts at $r$ with the empty assignment, which corresponds to the empty path.

Assume the invariant holds at a node $v$. If $v$ is a terminal node, the algorithm stops or outputs according to the terminal value, so the invariant is trivially preserved. If $v$ is a nonterminal node labeled $x_i$, then Algorithm B recursively follows each outgoing edge of $v$. Each such edge extends the path from $r$ to $v$ by one step, and correspondingly extends $P$ by assigning $x_i$. Hence every recursive call is again consistent with a unique root-to-current-node path, so the invariant is preserved.

Soundness

We show that every output produced by Algorithm B corresponds to a feasible solution, meaning a root-to-terminal $1$ path.

The algorithm outputs a solution only when it reaches terminal node $1$. By the definition of a BDD, any root-to-$1$ path encodes a complete assignment satisfying the represented constraints. Since, by the invariant, every output corresponds to a path in the BDD, every produced assignment is feasible.

Completeness

We show that every root-to-$1$ path in the BDD is generated by the algorithm.

Let $p$ be any root-to-$1$ path. We proceed by induction on the length of $p$.

At the root, the algorithm begins with the unique path of length zero. Suppose the algorithm has correctly followed the prefix of $p$ up to some node $v$. If $v$ is not terminal, the next edge of $p$ is either the 0-edge or the 1-edge leaving $v$. Algorithm B explicitly explores both outgoing edges of every nonterminal node, so it will recursively follow the edge that matches $p$. Thus the prefix of $p$ is extended step by step until terminal $1$ is reached. Therefore every root-to-$1$ path is generated.

This argument uses only the structural fact that Algorithm B explores all outgoing edges and does not require any additional pruning assumption.

Uniqueness

We show that no root-to-$1$ path is generated more than once.

Each execution path of the recursion corresponds to a sequence of deterministic choices of outgoing edges in the BDD. At every nonterminal node, Algorithm B branches into two distinct recursive calls, one for each outgoing edge. These branches form a recursion tree whose nodes are labeled by BDD nodes, but whose root-to-leaf paths correspond exactly to distinct sequences of edge choices.

Two different root-to-leaf recursion paths must differ at the first node where they choose different outgoing edges, hence they induce different assignments. Therefore no complete root-to-$1$ path can be produced twice.

This argument does not rely on memoization or on visiting each BDD node only once; it follows directly from the tree of recursive choices.

Conclusion

The invariant guarantees that recursion always follows valid BDD paths. Soundness follows because outputs occur only at terminal $1$. Completeness follows because all outgoing edges are explored recursively. Uniqueness follows because distinct recursion branches correspond to distinct edge sequences.

Therefore Algorithm B enumerates exactly the root-to-$1$ paths of the BDD, each exactly once, which establishes Theorem $Y$.