TAOCP 7.1.4 Exercise 5
Let $G$ be the BDD of $f(x_1,\dots,x_n)$, and construct a transformed directed acyclic graph $G'$ by interchanging the LO and HI pointers of every branch node and swapping the two sinks $\bot \leftrig...
Section 7.1.4: Binary Decision Diagrams
Exercise 5. [20] [20] If you take the BDD for f(x1, . . . , xn) and interchange the LO and HI pointers of every node, and if you also swap the two sinks ⊥↔⊤, what do you get?
Verified: no
Solve time: 3m14s
Solution
Let $G$ be the BDD of $f(x_1,\dots,x_n)$, and construct a transformed directed acyclic graph $G'$ by interchanging the LO and HI pointers of every branch node and swapping the two sinks $\bot \leftrightarrow \top$.
Define a mapping $T$ from nodes of $G$ to nodes of $G'$ by recursion on the structure of the graph. For a sink node, set $T(\bot)=\top$ and $T(\top)=\bot$. For a branch node $v$ with variable label $V(v)$ and children $\mathrm{LO}(v)$ and $\mathrm{HI}(v)$, define
$$ T(v) = \bigl(V(v),, T(\mathrm{HI}(v)),, T(\mathrm{LO}(v))\bigr). $$
For each node $v$ of $G$, let $f_v$ denote the Boolean function computed by the sub-BDD rooted at $v$, and let $g_v$ denote the Boolean function computed by the sub-BDD rooted at $T(v)$ in $G'$. The claim is that for every node $v$,
$$ g_v = \neg f_v. $$
The proof proceeds by induction on the structure induced by the variable ordering.
For a sink node $v=\bot$, the function $f_v$ is constantly $0$. The transformed node is $T(v)=\top$, so $g_v$ is constantly $1$, hence $g_v=\neg f_v$. The same argument holds with roles reversed when $v=\top$.
Let $v$ be a branch node labeled $x_i$. The Shannon decomposition in the BDD gives
$$ f_v = (x_i=0 \rightarrow f_{\mathrm{LO}(v)}) ;;\text{and};; (x_i=1 \rightarrow f_{\mathrm{HI}(v)}). $$
Thus
$$ f_v = (\neg x_i \wedge f_{\mathrm{LO}(v)}) \vee (x_i \wedge f_{\mathrm{HI}(v)}). $$
By definition of the transformation,
$$ g_v = (\neg x_i \wedge g_{\mathrm{HI}(v)}) \vee (x_i \wedge g_{\mathrm{LO}(v)}). $$
By the induction hypothesis, $g_{\mathrm{LO}(v)} = \neg f_{\mathrm{LO}(v)}$ and $g_{\mathrm{HI}(v)} = \neg f_{\mathrm{HI}(v)}$, hence
$$ g_v = (\neg x_i \wedge \neg f_{\mathrm{HI}(v)}) \vee (x_i \wedge \neg f_{\mathrm{LO}(v)}). $$
Taking complements in the expression for $f_v$ yields
$$ \neg f_v = \neg\bigl((\neg x_i \wedge f_{\mathrm{LO}(v)}) \vee (x_i \wedge f_{\mathrm{HI}(v)})\bigr) $$
and by De Morgan’s law,
$$ \neg f_v = (x_i \vee \neg f_{\mathrm{LO}(v)}) \wedge (\neg x_i \vee \neg f_{\mathrm{HI}(v)}). $$
Distributing and using $x_i \wedge \neg x_i = 0$ and $x_i \vee \neg x_i = 1$ reduces this expression to
$$ \neg f_v = (\neg x_i \wedge \neg f_{\mathrm{HI}(v)}) \vee (x_i \wedge \neg f_{\mathrm{LO}(v)}), $$
which matches $g_v$.
Thus $g_v = \neg f_v$ holds for all nodes reachable from the root, in particular for the root node $r$, so the function represented by $G'$ is $\neg f$.
The construction preserves ordering since variable labels are unchanged, and it preserves reduction conditions since it only permutes pointers and swaps sinks without creating new node triples. The resulting BDD is therefore a valid reduced ordered BDD for $\neg f$.
This completes the proof. ∎