TAOCP 7.1.4 Exercise 35
Let $G$ be the given FBDD with node set $V(G)$.
Section 7.1.4: Binary Decision Diagrams
Exercise 35. ▶ [22] [22] A free binary decision diagram (FBDD) is a binary decision diagram such as 2 3 4 4 1 3 ⊥ ⊤ ⊥ ⊤ where the branch variables needn’t appear in any particular order, but no variable is allowed to occur more than once on any downward path from the root. (An FBDD is “free” in the sense that every path in the dag is possible: No branch constrains another.) a) Design an algorithm to verify that a supposed FBDD is really free. b) Show that it’s easy to compute the reliability polynomial F(p1, . . . , pn) of a Bool- ean function f(x1, . . . , xn), given (p1, . . . , pn) and an FBDD that defines f, and to compute the number of solutions to f(x1, . . . , xn) = 1.
Verified: yes
Solve time: 2m09s
Solution
Let $G$ be the given FBDD with node set $V(G)$. Each non-sink node $u$ carries a variable index $V(u)\in{1,\dots,n}$ and has two successors $\mathrm{LO}(u)$ and $\mathrm{HI}(u)$; sink nodes are $\bot,\top$.
a) Verification that the FBDD is free
A downward path is free if no variable appears twice along it. This is equivalent to requiring that for every node $v$ and every root-to-$v$ path, the set of variables encountered on that path contains $V(v)$ at most once.
Define a state attached to each reachable configuration $(v,S)$ where $v\in V(G)$ and $S\subseteq {1,\dots,n}$ is the set of variables already encountered on the path from the root to $v$. The transition relation is determined by edges: from a non-sink node $u$ with label $i=V(u)$, every state $(u,S)$ induces a successor state $(w,S\cup{i})$ for each $w\in{\mathrm{LO}(u),\mathrm{HI}(u)}$ provided $i\notin S$.
The FBDD is free if and only if no reachable state violates the constraint $i\notin S$ when visiting a node labeled $i$.
We perform a graph reachability computation on the expanded state space. Initialize with $(r,\varnothing)$ where $r$ is the root. Maintain a worklist of states. For each extracted state $(u,S)$, if $u$ is a sink, continue. Otherwise let $i=V(u)$. If $i\in S$, the structure is not free. Otherwise propagate to $(\mathrm{LO}(u),S\cup{i})$ and $(\mathrm{HI}(u),S\cup{i})$.
Because $G$ is acyclic, the number of reachable states is finite and bounded by $|V(G)|\cdot 2^n$. Each transition updates a bitset by one insertion operation $S\cup{i}$. The algorithm accepts exactly when no violation state is reached, which occurs precisely when no root-to-sink path repeats a variable. This completes the verification criterion.
This completes part (a). ∎
b) Reliability polynomial and counting solutions
Let $F(p_1,\dots,p_n)$ be the probability that $f(x_1,\dots,x_n)=1$ under independent random variables with $\Pr[x_i=1]=p_i$.
For each node $u$, define a function $R(u,S)$ as the probability that evaluation starting at $u$ yields $\top$, conditioned on the variables in $S$ already being fixed along the path above $u$. As in part (a), $S$ records exactly the set of variables already encountered; free paths ensure consistency.
For sinks,
$$ R(\top,S)=1,\qquad R(\bot,S)=0. $$
For a non-sink node $u$ with $i=V(u)$, conditional on reaching $u$ with history $S$ (so $i\notin S$),
$$ R(u,S)=(1-p_i),R(\mathrm{LO}(u),S\cup{i})+p_i,R(\mathrm{HI}(u),S\cup{i}). $$
The value of the Boolean function is obtained at the root:
$$ F(p_1,\dots,p_n)=R(r,\varnothing). $$
The computation is performed by memoization over all reachable pairs $(u,S)$; acyclicity ensures termination, and identical subproblems are shared. This yields an evaluation proportional to the number of reachable states.
For counting solutions, define $C(u,S)$ as the number of assignments consistent with history $S$ that make the subfunction at $u$ evaluate to $1$. For sinks,
$$ C(\top,S)=2^{n-|S|},\qquad C(\bot,S)=0, $$
since a path reaching $\top$ leaves exactly the variables not in $S$ free.
For a non-sink node $u$ with $i=V(u)$, each extension fixes $x_i$ and leaves the remaining variables outside $S\cup{i}$ free, hence
$$ C(u,S)=C(\mathrm{LO}(u),S\cup{i})+C(\mathrm{HI}(u),S\cup{i}). $$
Again the required count is $C(r,\varnothing)$.
Both evaluations use the same state space $(u,S)$ as in part (a), and the recurrence is well-defined because each transition strictly advances along the DAG and strictly enlarges $S$. ∎