TAOCP 7.1.4 Exercise 45
We restart the construction from the actual BDD network underlying (33)–(34), where each module corresponds to a node of an ordered decision diagram and therefore represents a Boolean subfunction dete...
Section 7.1.4: Binary Decision Diagrams
Exercise 45. [22] [22] Give precise specifications for the Boolean modules that compute the three- in-a-row function as in (33) and (34), and show that the network is well defined.
Verified: no
Solve time: 2m55s
We restart the construction from the actual BDD network underlying (33)–(34), where each module corresponds to a node of an ordered decision diagram and therefore represents a Boolean subfunction determined by a suffix of the input together with a finite amount of “memory” carried by the path.
Let the input variables be $x_1,\dots,x_n$. The three-in-a-row function outputs $1$ iff somewhere in the sequence there is a block $x_i=x_{i+1}=x_{i+2}\in{0,1}$. Equivalently, it is the OR over all positions $i$ of the predicate
$$ (x_i=x_{i+1}=x_{i+2}=0)\ \lor\ (x_i=x_{i+1}=x_{i+2}=1). $$
In an ordered BDD, we cannot directly “look ahead” to $x_{i+1},x_{i+2}$ inside a single module without encoding that information into the state of subsequent modules. The correct network therefore augments the BDD nodes with a finite state describing the last two bits seen and whether a triple has already been detected.
Module specification
For each level $i \in {1,\dots,n+1}$, define Boolean modules indexed by a state
$$ s = (a,b,t) \in {0,1}^2 \times {0,1}, $$
where $a$ is the most recent bit seen (at position $i-1$), $b$ is the second most recent bit (at position $i-2$), and $t$ is a flag indicating whether a three-in-a-row occurrence has already been found in positions $1,\dots,i-1$.
We define a module $M_{i,a,b,t}$ to represent the Boolean function of the suffix $(x_i,\dots,x_n)$ under the assumption that the incoming state at level $i$ is $(a,b,t)$.
At the terminal level $i=n+1$, no input remains, so we define
$$ M_{n+1,a,b,t} = t. $$
This expresses that the function outputs $1$ exactly if a triple has already been detected.
Transition specification
For $i \le n$, each module $M_{i,a,b,t}$ performs a Shannon expansion on $x_i$, consistent with the ordered BDD construction in (33)–(34).
Let the updated state after reading $x_i$ be
$$ \mathrm{next}(a,b,t;x_i) = (x_i, a, t'), $$
where the new flag $t'$ is defined by detecting whether the newly formed triple is monochromatic:
$$ t' = t \ \lor\ (a=b=x_i). $$
Then the module specification is
$$ M_{i,a,b,t} = (\neg x_i \wedge M_{i+1,b,0,t'}) \ \lor\ (x_i \wedge M_{i+1,b,1,t'}). $$
Here the two successors correspond exactly to the BDD edges labeled by $x_i=0$ and $x_i=1$. The second component of the state shifts as required, and the first component records the current input bit.
Correspondence with the three-in-a-row function
This network computes the required function because along any evaluation path the state $(a,b,t)$ maintains the invariant that $t=1$ iff a triple of equal consecutive bits has already occurred in the processed prefix. The update rule ensures that whenever $x_{i-2}=x_{i-1}=x_i$, the flag becomes $1$ and remains $1$ thereafter since it is carried unchanged into all successors.
Thus at level $n+1$, the output $M_{n+1,a,b,t}=t$ is $1$ exactly when a three-in-a-row occurs anywhere in the input.
Well-definedness of the network
The network is well defined because each module $M_{i,a,b,t}$ is defined purely in terms of modules $M_{i+1,\cdot,\cdot,\cdot}$ at the next index level and the input variable $x_i$. There are no backward references to any module with index $\le i$, so the dependency graph is strictly layered by the index $i$.
Since $i$ decreases strictly along every dependency chain, every computation path has length at most $n$. At level $n+1$, all modules are constant Boolean functions, so recursion terminates.
Furthermore, for each fixed $(i,a,b,t)$, the defining equation assigns exactly one Boolean function in terms of already specified successor modules, so there is no ambiguity or multiple assignment.
Therefore the collection ${M_{i,a,b,t}}$ forms a finite layered acyclic network, and hence it is well defined.
This gives a precise specification of the Boolean modules corresponding to the ordered BDD construction of the three-in-a-row function and establishes that the resulting network is well defined.