Section 7.1.4: Binary Decision Diagrams

Exercise 104. ▶ [21] [21] Devise an efficient way to decide whether f ≤g or f ≥g or f ∥g, where f ∥g means that f and g are incomparable, given the BDDs for f and g.

Verified: no
Solve time: 4m06s

---

Solution

Let $f$ and $g$ be Boolean functions represented by reduced ordered binary decision diagrams with sink nodes $\bot,\top$ and with variable ordering $x_1 < \cdots < x_n$. The relations $f \le g$, $f \ge g$, and $f \parallel g$ are pointwise comparisons, interpreted as

$f \le g$ iff for every assignment $\mathbf{x}$, $f(\mathbf{x}) \le g(\mathbf{x})$ in ${0,1}$, with $\bot=0$ and $\top=1$.

The key observation is that $f \le g$ fails exactly when there exists an assignment such that $f=1$ and $g=0$. Hence

$$ f \nleq g ;;\Longleftrightarrow;; f \land \neg g \text{ is satisfiable.} $$

Similarly,

$$ g \nleq f ;;\Longleftrightarrow;; g \land \neg f \text{ is satisfiable.} $$

Thus the comparison reduces to two satisfiability tests on BDDs constructed implicitly from $(f,g)$.

Define a recursive predicate $\mathrm{SAT}(u,v,\sigma)$, where $u$ is a node of $f$, $v$ is a node of $g$, and $\sigma \in {0,1}$ indicates whether $v$ is complemented ($\sigma=1$ means interpret $g$ as $\neg g$ below $v$). The intended meaning is that $\mathrm{SAT}(u,v,\sigma)=\text{true}$ iff there exists an assignment consistent with the BDD paths from $u$ and $v$ such that the value of $f$ at $u$ equals $1$ and the value of $g$ at $v$ equals $\sigma$.

The terminal interpretation is determined first. If $u=\bot$, then $f=0$ and no assignment contributes to $f=1$, so the result is false. If $u=\top$, then $f=1$ is fixed, and satisfiability depends only on whether $(v,\sigma)$ can realize value $0$ for $g$ when $\sigma=0$ or value $1$ when $\sigma=1$. This is captured by interpreting complemented sinks so that the pair $(\top,v,\sigma)$ is satisfiable exactly when the Boolean condition $1 \land (\sigma \oplus g(v)) = 1$ can be achieved along some consistent path.

For internal nodes, let $V(u)=i$ and $V(v)=j$. If $i<j$, the next variable is $x_i$ in $f$ alone, so both outgoing edges of $v$ are followed while branching on $u$:

$$ \mathrm{SAT}(u,v,\sigma)

\mathrm{SAT}(\mathrm{LO}(u),v,\sigma);\lor;\mathrm{SAT}(\mathrm{HI}(u),v,\sigma). $$

If $j<i$, the symmetric rule applies:

$$ \mathrm{SAT}(u,v,\sigma)

\mathrm{SAT}(u,\mathrm{LO}(v),\sigma);\lor;\mathrm{SAT}(u,\mathrm{HI}(v),\sigma). $$

If $i=j$, both variables are tested simultaneously and consistency of assignments is preserved by pairing corresponding branches:

$$ \mathrm{SAT}(u,v,\sigma)

\mathrm{SAT}(\mathrm{LO}(u),\mathrm{LO}(v),\sigma);\lor;\mathrm{SAT}(\mathrm{HI}(u),\mathrm{HI}(v),\sigma). $$

Memoization over all pairs $(u,v)$ and both values of $\sigma$ ensures that each pair is evaluated once, since the BDD ordering guarantees acyclicity in the product graph of states. Hence the recursion terminates over a finite state space bounded by the Cartesian product of node sets.

Define two satisfiability predicates:

$$ A = \mathrm{SAT}(f,g,1), \qquad B = \mathrm{SAT}(g,f,1), $$

where $A$ detects existence of an assignment with $f=1$ and $g=0$, and $B$ detects existence of an assignment with $g=1$ and $f=0$.

The logical relations follow directly. If $A$ is false, no assignment satisfies $f=1$ and $g=0$, so $f \le g$. If $B$ is false, then $g \le f$. If both are false, equality holds pointwise. If both are true, there exist assignments witnessing both $f \nleq g$ and $g \nleq f$, which forces incomparability.

The decision procedure is therefore:

$$ f \le g \iff \neg A,\qquad g \le f \iff \neg B, $$

and

$$ f \parallel g \iff A \land B. $$

This reduces comparison of BDDs to two reachability tests in the product DAG of node pairs, using only local consistency with the variable ordering and memoized recursion over shared subproblems. ∎

Verification

The state space of the recursion consists of pairs of BDD nodes together with a binary flag for complementation, and each transition follows exactly one variable level consistent with the ordering constraint of reduced ordered BDDs, so no cycle can occur.

A satisfying path in $\mathrm{SAT}(f,g,1)$ produces a full assignment along which $f=1$ and $g=0$, since the construction enforces agreement with LO and HI branches whenever variables are fixed. Conversely, any assignment with $f=1$ and $g=0$ traces a unique path in both BDDs that is accepted by the recursion, so satisfiability equivalence holds in both directions.

The symmetry of the construction under exchange of $f$ and $g$ yields correctness of the dual predicate $B$, since all rules remain invariant under swapping the arguments.

The classification into $\neg A$, $\neg B$, and $A \land B$ covers exactly the three possibilities of a partial order on Boolean functions under pointwise comparison, so no case is omitted.

This completes the proof. ∎

Notes

The same decision can be implemented more compactly by building the BDD for $f \land \neg g$ using standard Apply operations and then testing reachability of $\top$. The product-recursion method avoids explicit construction and runs in time proportional to the number of reachable pairs of BDD nodes, which is bounded by $|f| \cdot |g|$ in the worst case but is typically much smaller due to shared subgraphs.