TAOCP 7.1.4 Exercise 61
Let $f$ and $g$ be Boolean functions with respective BDDs.
Section 7.1.4: Binary Decision Diagrams
Exercise 61. ▶ [M27] [M27] If α and β are nodes of the respective BDDs for f and g, prove that in-degree(α ⋄β) ≤in-degree(α) · in-degree(β) in the melded BDD f ⋄g. (Imagine that the root of a BDD has in-degree 1.)
7.1.4 BINARY DECISION DIAGRAMS 263
Verified: no
Solve time: 5m32s
Setup
Let $f$ and $g$ be Boolean functions with respective BDDs. Let $\alpha$ be a node in the BDD of $f$ and $\beta$ a node in the BDD of $g$. In the melded BDD for $f \diamond g$, nodes are formed as pairs $\alpha \diamond \beta$ of compatible nodes, and directed edges arise from simultaneous traversal of the LO and HI structure in the two component BDDs, respecting the variable ordering.
For a node $v$ in a directed acyclic graph, $\mathrm{in\text{-}degree}(v)$ denotes the number of incoming edges to $v$. The goal is to prove
$$ \mathrm{in\text{-}degree}(\alpha \diamond \beta) \le \mathrm{in\text{-}degree}(\alpha),\mathrm{in\text{-}degree}(\beta). $$
The root is assumed to have in-degree $1$, consistent with the convention for BDDs.
Solution
Consider any incoming edge in the melded BDD that ends at the node $\alpha \diamond \beta$. Such an edge originates at some node of the form $\alpha' \diamond \beta'$, where there is a valid transition in the $f$-BDD from $\alpha'$ to $\alpha$ and simultaneously a valid transition in the $g$-BDD from $\beta'$ to $\beta$, using the same branch type (LO or HI) determined by the same variable comparison in the ordered structure.
Thus every incoming edge to $\alpha \diamond \beta$ determines uniquely an ordered pair consisting of one incoming edge to $\alpha$ and one incoming edge to $\beta$. Specifically, the projection of the melded edge onto the first component is an edge $\alpha' \to \alpha$ in the BDD of $f$, and the projection onto the second component is an edge $\beta' \to \beta$ in the BDD of $g$.
Define the mapping that sends each incoming edge $e$ of $\alpha \diamond \beta$ to the pair $(e_f, e_g)$ consisting of its component edges in the two original BDDs. This mapping is injective because distinct incoming edges in the melded structure differ in at least one endpoint node, hence differ in at least one of their projected component edges.
The image of this injection lies in the Cartesian product of the sets of incoming edges to $\alpha$ and to $\beta$. Therefore the number of incoming edges to $\alpha \diamond \beta$ cannot exceed the number of such pairs:
$$ \mathrm{in\text{-}degree}(\alpha \diamond \beta) \le \mathrm{in\text{-}degree}(\alpha),\mathrm{in\text{-}degree}(\beta). $$
This completes the proof. ∎
Verification
Each incoming edge in the melded BDD is determined by a unique predecessor pair $(\alpha' \diamond \beta')$ together with a unique choice of branch consistent in both component BDDs. Projection onto each coordinate yields a valid incoming edge in the respective original BDDs.
Distinct melded edges cannot project to the same pair of component edges, since the source node in the product structure is uniquely determined by its components. Hence the injection into the Cartesian product is valid, and no overcounting occurs.
The inequality follows directly from counting the size of the image set.
Notes
The argument remains valid even if reduction rules are applied after forming the product structure, since merging identical nodes can only decrease in-degree and never increase it.