TAOCP 7.1.4 Exercise 246

Exercise 246. [M21] [M21] Prove Theorem S, assuming that (137) is true.

Verified: no
Solve time: 6m30s

Solution

Let $G=(V,E)$ be a graph, and let $f$ be a monotone Boolean function on $V$ expressed in family algebra as in Section 7.1.4, with ZDD representation. Let (137) denote the fundamental decomposition identity for monotone families into prime clauses and their complements, namely the representation of $f$ as an intersection of implications generated by its prime implicants, together with the dual ZDD decomposition over choice of a variable $x\in V$:

$$ f = f_{x=0} ;\cup; (x \cap f_{x=1}), $$

together with the corresponding ZDD splitting rule for families,

$$ F = F_0 ;\uplus; (x \cap F_1), $$

where $\uplus$ denotes disjoint union of families of sets that differ by the presence of $x$.

Theorem S asserts that the ZDD construction algorithm for monotone families, which recursively applies (137) along a fixed variable ordering, produces a reduced ordered ZDD whose nodes are in one-to-one correspondence with the prime implicants (equivalently, with the elements of $\mathrm{PI}(f)^\sharp$ as defined in exercise 245).

To prove this, the argument proceeds by structural induction on the variable order and by showing equivalence of two constructions: the semantic decomposition of $f$ by (137), and the syntactic ZDD construction that merges identical subfamilies under reduction.

Let $x_1<\dots<x_n$ be the fixed ordering. For each prefix $x_1,\dots,x_k$, let $f^{(k)}$ denote the restriction of $f$ obtained by assigning values to the first $k$ variables. The ZDD construction maintains at level $k$ the family of residual monotone subfunctions $f^{(k)}$, each representing all extensions consistent with partial assignments.

Assume (137) holds for every monotone function on fewer than $n$ variables. Consider the decomposition at variable $x_1$. By monotonicity, every set in $f$ either excludes $x_1$, contributing to $f_{x_1=0}$, or includes $x_1$, contributing to $x_1 \cap f_{x_1=1}$. These two parts are disjoint because inclusion of $x_1$ changes membership of the element $x_1$ itself.

The ZDD construction therefore introduces a node labeled $x_1$ whose low child encodes $f_{x_1=0}$ and whose high child encodes $f_{x_1=1}$. This construction is well-defined because both subfamilies are monotone and depend only on variables $x_2,\dots,x_n$, so the induction hypothesis applies.

Assume two distinct nodes at the same variable level represent identical subfamilies. Then they correspond to identical monotone functions on the remaining variables. By the inductive hypothesis, such functions have identical ZDDs. The reduction rule of ZDDs merges nodes with identical $(V,\mathrm{LO},\mathrm{HI})$ triples, so no duplication survives. This establishes uniqueness of representation at each level.

Now consider termination at sinks. If a subfamily contains only the empty set, it corresponds to $\bot$, and if it contains only the empty extension after full inclusion constraints, it corresponds to $\top$ under the monotone interpretation. These are exactly the two terminal cases of (137), since repeated application eventually eliminates all variables, producing either the empty family or the full closure.

To connect this with prime clauses, let $P\in \mathrm{PI}(f)$ be a prime implicant. By definition, $P$ is minimal such that every superset of $P$ lies in $f$. In the ZDD, following high-branches exactly along elements of $P$ and low-branches elsewhere produces a unique root-to-1 path, since any deviation from including all elements of $P$ violates monotonicity or minimality. Conversely, every accepting path corresponds to a minimal set of high-branch choices, since any redundant inclusion would contradict reduction of the ZDD or violate minimality in the induced family.

Thus every accepting path corresponds to a unique prime implicant, and every prime implicant induces exactly one accepting path. Therefore nodes correspond exactly to the decomposition structure generated by (137), and reduction ensures that no additional structure remains beyond these equivalence classes.

Finally, since every recursive decomposition step is justified by (137), and since uniqueness and minimality follow from monotonicity and ZDD reduction, the constructed diagram is the canonical reduced ordered ZDD for $f$. This establishes that the algorithm computes exactly $\mathrm{PI}(f)^\sharp$ as its node set representation.

This completes the proof. ∎