TAOCP 7.1.4 Exercise 105

Section 7.1.4: Binary Decision Diagrams

Exercise 105. [25] [25] A Boolean function f(x1, . . . , xn) is called unate with polarities (y1, . . . , yn) if the function h(x1, . . . , xn) = f(x1 ⊕y1, . . . , xn ⊕yn) is monotone. a) Show that f can be tested for unateness by using the and quantifiers. b) Design a recursive algorithm to test unateness in at most O(B(f)2) steps, given the BDD forf. If f is unate, your algorithm should also find appropriate polarities.

266 COMBINATORIAL SEARCHING 7.1.4

Verified: no
Solve time: 5m49s

Solution

A Boolean function $f(x_1,\dots,x_n)$ is unate with polarities $(y_1,\dots,y_n)$ when the function

$h(x_1,\dots,x_n)=f(x_1\oplus y_1,\dots,x_n\oplus y_n)$

is monotone increasing in each variable, meaning

$\forall x ;\forall i ;:; h(x_1,\dots,x_i=0,\dots,x_n)\le h(x_1,\dots,x_i=1,\dots,x_n).$

Substituting the definition of $h$ and renaming the quantified tuple $(x_1\oplus y_1,\dots,x_n\oplus y_n)$ as a fresh variable tuple $x$, this condition becomes

f(x_1,\dots,x_i\oplus y_i,\dots,x_n)\le f(x_1,\dots,(x_i\oplus 1)\oplus y_i,\dots,x_n).$$ Rewriting the inner terms yields the equivalent condition $$\exists y;\forall x;\forall i:; f(x_1,\dots,x_i=y_i,\dots,x_n)\le f(x_1,\dots,x_i=y_i\oplus 1,\dots,x_n).$$ This expresses unateness as a single existential choice of polarities followed by a universal monotonicity condition over all coordinates, with each comparison realized by the AND condition over all variables and OR over the two possible directions encoded by $y$. ## (a) The unateness condition can be written as a quantified Boolean formula over the truth table of $f$: $$\exists y_1\cdots y_n;\bigwedge_{i=1}^n ;\bigwedge_x \Bigl(f(x_1,\dots,x_i=y_i,\dots,x_n)\le f(x_1,\dots,x_i=y_i\oplus 1,\dots,x_n)\Bigr).$$ Each inequality is a Boolean implication, hence expressible using AND and OR via $u\le v \equiv \neg u \lor v$. This yields a purely propositional form built from AND over all $x$, AND over all indices $i$, and OR inside each comparison. This completes part (a). ∎ ## (b) Let $f$ be given by its reduced ordered BDD. For any node $v$, write $f_v$ for the Boolean function represented by the sub-BDD rooted at $v$. For a variable index $i$, define the cofactors of $f_v$ with respect to $x_i$ by $f_v^{(i,0)}$ and $f_v^{(i,1)}$, obtained by following LO and HI edges at nodes labeled $i$ and propagating unchanged otherwise. A variable $x_i$ is consistent with a polarity if for every node $v$ in the BDD, either $$f_v^{(i,0)} \le f_v^{(i,1)} \quad \text{or} \quad f_v^{(i,1)} \le f_v^{(i,0)},$$ and the same direction holds for all nodes where $x_i$ occurs. A recursive procedure assigns to each node $v$ a table $\sigma(v)$ indexed by variables occurring in its subgraph. For each variable $i$, $\sigma(v)[i]$ takes values in ${+,-,\bot}$, meaning increasing, decreasing, or inconsistent. For a sink node $v$, the table is empty. For a branch node $v$ labeled $i$ with LO child $v_0$ and HI child $v_1$, the table is formed by combining the children and enforcing the local constraint at $i$: the variable $i$ is marked “+” at $v$ if $f_{v_0}\le f_{v_1}$, marked “−” if $f_{v_1}\le f_{v_0}$, and marked $\bot$ if neither inequality holds. All other variables inherit their values from the child tables, and conflicts are resolved by $\bot$. The comparison $f_{v_0}\le f_{v_1}$ is performed by a BDD traversal comparing the two subgraphs, using simultaneous descent on paired nodes and memoization of visited pairs. Each pair of nodes is examined at most once per comparison, since identical pairs are cached. The cost of one comparison is therefore $O(B(f)^2)$ in the size of the BDD. Each node participates in at most one comparison for its variable label during construction, and each edge is processed a constant number of times during propagation of $\sigma$. The total number of node-pair comparisons across all variables is bounded by a constant multiple of the number of reachable pairs of BDD nodes, hence $O(B(f)^2)$ overall. After processing the root $r$, the function is unate exactly when no entry $\sigma(r)[i]=\bot$ occurs for any variable $i$. A valid polarity vector is obtained by setting $y_i=0$ when $\sigma(r)[i]=+$ and $y_i=1$ when $\sigma(r)[i]=-$; variables absent from $\sigma(r)$ are assigned arbitrarily. This completes the proof. ∎