TAOCP 7.1.4 Exercise 10
Let $f$ and $f'$ be Boolean functions represented by reduced ordered BDDs.
Section 7.1.4: Binary Decision Diagrams
Exercise 10. ▶ [21] [21] Given two BDDs that define Boolean functions f and f ′, represented sequen- tially as in (8) and (10), design an algorithm that tests f = f ′.
Verified: no
Solve time: 4m12s
Solution
Let $f$ and $f'$ be Boolean functions represented by reduced ordered BDDs. Let their roots be nodes $u_0$ and $v_0$. Each node $u$ has fields $V(u)$, $LO(u)$, $HI(u)$, and each sink is either $\bot$ or $\top$.
Equality $f = f'$ holds exactly when the two BDDs induce the same function on every assignment $(x_1,\dots,x_n)$. Because each reduced ordered BDD is canonical for a fixed variable ordering, this is equivalent to structural isomorphism of the two rooted DAGs with sinks preserved.
Define a predicate $\operatorname{Eq}(u,v)$ that holds when the subfunctions represented by nodes $u$ and $v$ are identical.
The comparison proceeds by simultaneous descent through corresponding nodes, with memoization to prevent repeated work on shared subgraphs.
For any pair $(u,v)$, if this pair has been processed previously, the stored result is returned. Otherwise the computation distinguishes cases according to whether $u$ and $v$ are sinks or branch nodes.
When both $u$ and $v$ are sinks, $\operatorname{Eq}(u,v)$ holds exactly when they are the same sink symbol, since $\bot \neq \top$ and these are the only possible terminal values.
When exactly one of $u$ and $v$ is a sink, the functions differ on some assignment, since a sink represents a constant function while a branch node depends on at least one variable by the ordering property, so $\operatorname{Eq}(u,v)$ fails.
When both are branch nodes, equality of the functions forces equality of the queried variable, since otherwise one node tests a variable that the other does not test at the corresponding decision point, contradicting ordered structure. Thus $V(u)=V(v)$ is required. Under this condition, the function values agree exactly when both cofactors agree, so $\operatorname{Eq}(u,v)$ holds exactly when both $\operatorname{Eq}(LO(u),LO(v))$ and $\operatorname{Eq}(HI(u),HI(v))$ hold.
Let $\mathcal{M}$ be a table initially empty that stores already evaluated pairs.
Define the procedure $\operatorname{Equal}(u,v)$ as follows.
If $(u,v)\in \mathcal{M}$, return the stored value.
If $u=\bot$ and $v=\bot$, return true.
If $u=\top$ and $v=\top$, return true.
If exactly one of $u,v$ is in ${\bot,\top}$, return false.
If $V(u)\neq V(v)$, return false.
Compute
$$ t_0 := \operatorname{Equal}(LO(u),LO(v)), \quad t_1 := \operatorname{Equal}(HI(u),HI(v)). $$
Store $(u,v)\mapsto (t_0 \wedge t_1)$ in $\mathcal{M}$ and return this value.
The algorithm terminates because each recursive call descends strictly along the partial order induced by increasing variable indices, a consequence of the ordering restriction that every arc goes from a node with smaller index to one with larger index.
Correctness follows by induction on the structure of reachable pairs $(u,v)$. For sink pairs the result is correct by direct evaluation of constants. For branch pairs, assume correctness for all strict descendants. If $f_u$ and $f_v$ are the functions represented at $u$ and $v$, then for any assignment with current variable $x_{V(u)}$, the BDD semantics decompose evaluation into the two cofactors determined by $LO$ and $HI$. Equality of functions holds exactly when both cofactors are equal functions, and by the induction hypothesis this is equivalent to the recursive conditions returning true.
Every pair of nodes is evaluated at most once because membership in $\mathcal{M}$ prevents recomputation. Hence the number of recursive expansions is proportional to the number of reachable pairs of nodes in the product graph of the two BDDs. Since each node has at most two outgoing edges, the traversal examines at most a constant number of edges per pair, so the total work is linear in the size of the combined reachable subgraphs.
Thus the algorithm decides whether $f=f'$ by testing structural equivalence of their reduced ordered BDDs under simultaneous traversal.
This completes the proof. ∎