TAOCP 7.1.4 Exercise 265

Let $f$ be a Boolean function of variables $x_1,\dots,x_n$ given by a reduced ordered BDD.

Section 7.1.4: Binary Decision Diagrams

Exercise 265. ▶ [21] [21] Devise an algorithm that finds the mth smallest solution to f(x) = 1 in lexicographic order of x1 . . . xn, given m and the BDD for a Boolean function f of n variables. Your algorithm should take O(nB(f) + n2) steps.

Verified: no
Solve time: 2m05s


Solution

Let $f$ be a Boolean function of variables $x_1,\dots,x_n$ given by a reduced ordered BDD. For a node $v$ in the BDD, let $\operatorname{var}(v)$ be its variable index when $v$ is a branch node, and let $\operatorname{lo}(v),\operatorname{hi}(v)$ be its children. Sink nodes are $\bot$ and $\top$.

A lexicographic order on assignments $x_1\cdots x_n$ compares two assignments by the first coordinate in which they differ, with $0<1$. The task is to construct the $m$th assignment in this order among those satisfying $f(x)=1$.

The structure of the BDD ensures that every root-to-sink path corresponds to a unique assignment of the variables, since each variable is tested at most once and in increasing index order.

Counting satisfying assignments

For each node $v$, define $\operatorname{sat}(v)$ as the number of assignments to the variables from $\operatorname{var}(v)$ to $x_n$ that lead from $v$ to $\top$.

For sink nodes,

$$ \operatorname{sat}(\bot)=0,\qquad \operatorname{sat}(\top)=1. $$

For a branch node $v$ with $\operatorname{var}(v)=i$, suppose $\operatorname{lo}(v)$ and $\operatorname{hi}(v)$ have variables $j$ and $k$ respectively, where $j,k>i$. Between $i$ and $j-1$ there are $j-i-1$ variables not tested on the LO edge, and similarly $k-i-1$ variables on the HI edge. Each such skipped variable contributes a factor of $2$ for free assignment. Hence

$$ \operatorname{sat}(v)

2^{j-i-1}\operatorname{sat}(\operatorname{lo}(v)) + 2^{k-i-1}\operatorname{sat}(\operatorname{hi}(v)). $$

This recurrence applies uniformly when a child is a sink by treating its variable index as $n+1$.

Computing all values $\operatorname{sat}(v)$ bottom-up over the DAG visits each node once. Each computation involves additions and multiplications by powers of $2$ on integers of size at most $n$ bits, since $\operatorname{sat}(v)\le 2^n$. Using standard big-integer arithmetic, each node costs $O(n)$ time, so the total cost is $O(nB(f))$.

Selecting the $m$th lexicographic solution

Assume $m\le \operatorname{sat}(\text{root})$. The construction proceeds by following a single path from the root, determining $x_1,\dots,x_n$ sequentially.

At a node $v$ corresponding to variable $x_i$, define

$$ L = \operatorname{sat}(\operatorname{lo}(v)), \qquad R = \operatorname{sat}(\operatorname{hi}(v)). $$

The set of satisfying assignments under $v$ splits into those with $x_i=0$ followed by $L$ completions, and those with $x_i=1$ followed by $R$ completions. Lexicographic order places all assignments with $x_i=0$ before those with $x_i=1$.

If $m \le L$, then the desired assignment lies in the LO subtree and $x_i=0$ is fixed. If $m>L$, then $x_i=1$ and $m$ is replaced by $m-L$, continuing in the HI subtree.

When a chain of variables is skipped, the BDD semantics already accounts for all intermediate variables inside $\operatorname{sat}(\cdot)$, so no additional correction is needed during the descent.

When a sink node $\top$ is reached at some variable $x_i$, all remaining variables $x_i,\dots,x_n$ may be set to $0$, since any completion satisfies the function and lexicographic minimality is preserved. If $\bot$ is reached, no valid continuation exists, which cannot occur along a correct selection path.

The traversal performs one constant-time comparison per level plus one subtraction when moving to the HI branch. Each comparison involves integers of size $O(n)$ bits, so the traversal contributes $O(n^2)$ time.

Algorithm summary

Precompute $\operatorname{sat}(v)$ for all nodes $v$ in the BDD. Then start at the root and for $i=1$ to $n$, repeatedly choose $x_i=0$ if $m\le \operatorname{sat}(\operatorname{lo}(v))$, otherwise set $x_i=1$ and update $m\leftarrow m-\operatorname{sat}(\operatorname{lo}(v))$, descending accordingly. If a sink $\top$ is reached, fill remaining variables with $0$.

The preprocessing requires $O(nB(f))$ time, and the descent requires $O(n^2)$ time, giving total complexity $O(nB(f)+n^2)$.

This completes the proof. ∎