TAOCP 7.1.4 Exercise 60
Let $f$ and $g$ be reduced ordered BDDs over variables $x_1,\dots,x_n$ with fixed ordering.
Section 7.1.4: Binary Decision Diagrams
Exercise 60. [M22] [M22] Suppose f(x1, . . . , xn) and g(x1, . . . , xn) have the profiles (b0, . . . , bn) and (b′ 0, . . . , b′ n), respectively, and let their respective quasi-profiles be (q0, . . . , qn) and (q′ 0, . . . , q′ n). Show that their meld f ⋄g has B(f ⋄g) ≤n j=0(qjb′ j + bjq′ j −bjb′ j) nodes.
Verified: yes
Solve time: 2m42s
Let $f$ and $g$ be reduced ordered BDDs over variables $x_1,\dots,x_n$ with fixed ordering. For a node $u$, write $\ell(u)$ for its level (variable index), with sinks placed at level $0$. Let $b_j$ (resp. $b'j$) denote the number of nodes of $f$ (resp. $g$) at level $j$. Let $F{\le j}$ (resp. $G_{\le j}$) denote the set of nodes of $f$ (resp. $g$) whose levels are at most $j$, and let $q_j = |F_{\le j}|$, $q'j = |G{\le j}|$.
The meld $f \diamond g$ is constructed by the recursive rule (37), which forms a reduced BDD whose nodes correspond to distinct pairs of nodes $(u,v)$ from the original diagrams, with two pairs identified exactly when they induce the same subfunction under the recursion. Because both input BDDs are reduced and ordered, every node of the meld has a well-defined representation by a unique pair of canonical nodes $(u,v)$, and distinct meld nodes correspond to distinct such pairs.
For a meld node represented by $(u,v)$, define its level as
$$ L(u,v) = \max(\ell(u), \ell(v)). $$
This is consistent with the construction in (37), since the recursion proceeds at the first variable where at least one component BDD makes a decision, and sinks are treated as level $0$.
Fix $j \in {0,\dots,n}$. Let $M_j$ be the set of meld nodes of level $j$. By the discussion above, we may identify $M_j$ with a set of pairs $(u,v)$ such that $L(u,v)=j$. Hence
$$ |M_j| \le #{(u,v) : u \in F_{\le j},\ v \in G_{\le j},\ \max(\ell(u),\ell(v))=j}. $$
We now partition the admissible pairs according to which component attains level $j$. The condition $\max(\ell(u),\ell(v))=j$ is equivalent to
$$ (\ell(u)=j,\ \ell(v)\le j)\ \ \text{or}\ \ (\ell(v)=j,\ \ell(u)\le j), $$
with the overlap being the pairs where both $\ell(u)=j$ and $\ell(v)=j$.
Define
$$ B_j = {u \in f : \ell(u)=j}, \qquad B'_j = {v \in g : \ell(v)=j}. $$
Then $|B_j|=b_j$ and $|B'j|=b'j$, and also $|F{\le j}|=q_j$, $|G{\le j}|=q'_j$.
Hence the number of pairs with $\max(\ell(u),\ell(v))=j$ is bounded by the size of the union
$$ (F_{\le j}\times B'j)\ \cup\ (B_j\times G{\le j}). $$
Applying inclusion–exclusion gives
$$ |(F_{\le j}\times B'j)\cup(B_j\times G{\le j})| = |F_{\le j}\times B'j| + |B_j\times G{\le j}| - |B_j\times B'_j|. $$
Each term factors:
$$ |F_{\le j}\times B'_j| = q_j b'j,\quad |B_j\times G{\le j}| = b_j q'_j,\quad |B_j\times B'_j| = b_j b'_j. $$
Therefore,
$$ |M_j| \le q_j b'_j + b_j q'_j - b_j b'_j. $$
Finally, every meld node belongs to exactly one level $j$, so summing over all levels yields
$$ B(f \diamond g) = \sum_{j=0}^n |M_j| \le \sum_{j=0}^n \left(q_j b'_j + b_j q'_j - b_j b'_j\right). $$
This completes the proof. ∎