TAOCP 7.1.4 Exercise 253
Let $f(x_1,\ldots,x_n) = (\bar{x}_1 \wedge f_0) \vee (x_1 \wedge f_1)$, where $f_0, f_1$ are Boolean functions of $x_2,\ldots,x_n$.
Section 7.1.4: Binary Decision Diagrams
Exercise 253. ▶ [M26] [M26] Continuing exercise 252, prove that if f = (¯x1∧f0) ∨(x1∧f1) we have PI(f) = A ∪(e′ 1⊔B) ∪(e1⊔C), where A = PI(f0 ∧f1), B = PI(f0) \ A, and C = PI(f1) \ A. (Equation (137) is the special case when f is monotone.)
Verified: no
Solve time: 4m04s
Setup
Let $f(x_1,\ldots,x_n) = (\bar{x}_1 \wedge f_0) \vee (x_1 \wedge f_1)$, where $f_0, f_1$ are Boolean functions of $x_2,\ldots,x_n$.
A cube (subcube) is a conjunction of literals. We use the family algebra notation where $e_1 \sqcup B$ prefixes each cube in $B$ with the literal $x_1$, and $e_1' \sqcup B$ prefixes each cube with $\bar{x}_1$.
A prime implicant of a Boolean function is an implicant that is minimal under deletion of literals: removing any literal destroys the implicant property.
We must prove that
$$ \mathrm{PI}(f) = A ;\cup; (e_1' \sqcup B) ;\cup; (e_1 \sqcup C), $$
where
$$ A = \mathrm{PI}(f_0 \wedge f_1), \quad B = \mathrm{PI}(f_0) \setminus A, \quad C = \mathrm{PI}(f_1) \setminus A. $$
Solution
Every implicant of $f$ forces at least one of the two disjuncts in its defining form to hold on all assignments satisfying the cube. Thus any cube $p \in \mathrm{PI}(f)$ satisfies either $p \Rightarrow \bar{x}_1 \wedge f_0$ or $p \Rightarrow x_1 \wedge f_1$, or both.
Case 1: $p$ contains neither $x_1$ nor $\bar{x}_1$
Then $p$ does not restrict $x_1$. For $p$ to imply $f$, it must satisfy both branches of the disjunction regardless of the value of $x_1$, since $x_1$ can be 0 or 1 under $p$. Hence $p \Rightarrow f_0$ and $p \Rightarrow f_1$, so $p \Rightarrow f_0 \wedge f_1$.
If $p$ were not a prime implicant of $f_0 \wedge f_1$, then some proper subcube of $p$ would still imply $f_0 \wedge f_1$, hence also $f$, contradicting the primeness of $p$ for $f$. Therefore
$$ p \in \mathrm{PI}(f_0 \wedge f_1) = A. $$
Case 2: $p$ contains $\bar{x}_1$
Write $p = \bar{x}_1 \wedge q$, where $q$ involves only $x_2,\ldots,x_n$. Since $p \Rightarrow f$, and on all satisfying assignments of $p$ we have $x_1 = 0$, the function reduces to $f_0$. Hence $q \Rightarrow f_0$, so $q$ is an implicant of $f_0$.
If $q$ is not prime for $f_0$, then a strict subcube $q' \subset q$ would still imply $f_0$, hence $\bar{x}_1 \wedge q'$ would imply $f$, contradicting primeness of $p$. Thus $q \in \mathrm{PI}(f_0)$.
We must separate those $q$ that already imply $f_1$ as well. If $q \Rightarrow f_1$, then $q \Rightarrow f_0 \wedge f_1$, hence $q \in A$. In that case $\bar{x}_1 \wedge q$ is not a new generator beyond $A$ once lifted into the full variable space.
If $q \notin A$, then $q \in B$, and we obtain $p \in e_1' \sqcup B$.
Thus all prime implicants of this form are exactly $e_1' \sqcup B$ together with those absorbed into $A$.
Case 3: $p$ contains $x_1$
Symmetrically, write $p = x_1 \wedge q$. The same argument shows $q \Rightarrow f_1$, and primeness forces $q \in \mathrm{PI}(f_1)$. If $q \in A$, it is absorbed into case 1 after forgetting the literal. Otherwise $q \in C$, giving $p \in e_1 \sqcup C$.
Exhaustion
Every prime implicant must fall into exactly one of the three cases depending on whether it contains $x_1$, $\bar{x}_1$, or neither. The constructions above show inclusion of all such cases into the right-hand side, hence
$$ \mathrm{PI}(f) \subseteq A \cup (e_1' \sqcup B) \cup (e_1 \sqcup C). $$
Conversely, every element of $A$, $e_1' \sqcup B$, and $e_1 \sqcup C$ is an implicant of $f$ by construction, and minimality follows from minimality of the underlying sets $A$, $B$, and $C$ together with the fact that adding or removing the fixed literal $x_1$ cannot introduce a redundant literal inside the remaining part. Hence each such cube is a prime implicant of $f$, giving the reverse inclusion.
Therefore the stated decomposition holds.
This completes the proof. ∎
Verification
The decomposition respects the Shannon expansion structure of $f$, since every satisfying assignment either fixes $x_1=0$ or $x_1=1$. In the first case the condition reduces exactly to $f_0$, and in the second to $f_1$, so implicants split according to containment of the literal $x_1$ or its negation.
The only nontrivial consistency check is the treatment of cubes valid for both $f_0$ and $f_1$. These are precisely the implicants of $f_0 \wedge f_1$, so they must appear once without a prefixed literal, avoiding duplication under both branches. This is enforced by defining $A$ and removing it from $B$ and $C$.
Thus each cube appears exactly once in the union.
Notes
This decomposition is the implicant analogue of Shannon cofactoring. It is structurally identical to BDD decomposition, where nodes correspond to splitting on $x_1$ into low and high subfunctions, except that here the objects being propagated are minimal covers rather than truth tables.