TAOCP 7.1.4 Exercise 172
A BDD is **skinny** if for each variable $x_j$ there is exactly one branch node labeled $j$, and at that node exactly one of the two outgoing edges, LO or HI, leads to a sink node.
Section 7.1.4: Binary Decision Diagrams
Exercise 172. [M28] [M28] How many skinny functions f(x1, . . . , xn) are also Horn functions? How many of them have the property that f and ¯f both satisfy Horn’s condition?
Verified: no
Solve time: 6m07s
Setup
A BDD is skinny if for each variable $x_j$ there is exactly one branch node labeled $j$, and at that node exactly one of the two outgoing edges, LO or HI, leads to a sink node. The other edge leads to a unique later branch node, so the structure is a single chain of tests in the fixed variable order $x_1,\dots,x_n$, with a terminal decision taken immediately at each level on one branch.
A Boolean function is monotone if replacing any input bit $0 \to 1$ cannot change the value from $1$ to $0$.
A Boolean function is read-once if it can be represented by a formula in which each variable appears exactly once.
A read-once function is regular in the sense of Section 7.1.4 if, after a suitable variable order $\pi$, its BDD is ordered and every variable corresponds to a single decision point with no reconvergence of subfunctions beyond that forced by reduction.
The task is to prove that a Boolean function is read-once and regular if and only if its BDD is skinny and monotone.
Solution
Assume first that a function $f(x_1,\dots,x_n)$ is read-once and regular. Then there exists a representation of $f$ as a formula in which each variable occurs exactly once. Fix an order consistent with that formula evaluation, which yields a linear progression of variable tests in which each variable is evaluated exactly once along every root-to-sink path.
In the corresponding BDD, each variable $x_j$ appears exactly once as a decision point, since a second occurrence would contradict the read-once property. Thus each variable corresponds to exactly one branch node, so the BDD has exactly one node labeled $j$ for each $j$, which is the defining structural condition for being skinny.
At each such node, the read-once property forces that one branch immediately determines the output independent of all later variables, since no variable can be reused downstream. Therefore, for each node, exactly one of LO or HI must lead directly to a sink node. If both edges led to further variables, the function value at that node would depend on multiple occurrences of a variable in some induced subfunction, contradicting read-once regularity. Hence the BDD is skinny.
Monotonicity follows from the structure of a skinny BDD together with regularity. Along any root-to-sink path, replacing any input assignment by increasing some $x_j$ from $0$ to $1$ moves the traversal either along the same variable level or to a subtree corresponding to a later stage in the fixed order. Since each variable appears exactly once, increasing an input can only move the evaluation toward a branch that is closer to or already at the $\top$ sink, never toward $\bot$, because the decision at each node depends only on a single unrepeated variable and no reversal mechanism exists through repeated testing. This implies that $f$ is monotone.
Now assume conversely that a Boolean function $f$ has a BDD that is skinny and monotone. Since the BDD is skinny, for each variable $x_j$ there is exactly one branch node labeled $j$. Hence along any root-to-sink path, each variable is tested at most once, so the induced representation is read-once.
The structure also forces regularity. The BDD is a single chain of decisions in the fixed variable order, since each variable appears exactly once and no variable can reappear later due to ordering. Reduction does not merge distinct subfunctions in a way that reintroduces variable reuse. Therefore the function is regular in the sense of having a consistent ordered BDD representation with unique variable occurrences.
It remains to verify that this representation is consistent with a read-once formula. Each branch node contributes either a literal condition $x_j$ or $\bar{x}_j$ depending on whether the HI or LO edge leads to $\top$. Since exactly one outgoing edge from each node leads to a sink, each variable contributes a single literal decision in a formula constructed by reading off the unique path structure of the BDD. No variable is reused, so the resulting expression is read-once.
Finally, monotonicity ensures compatibility of all sink assignments with the partial order on ${0,1}^n$. If a node assigns LO to $\bot$ and HI to $\top$, the local function is increasing in $x_j$. If the assignment were reversed, monotonicity would be violated. Thus all branch nodes must assign $0 \to \bot$ and $1 \to \top$, ensuring that the function is monotone and that the read-once structure is preserved globally.
Therefore a function is read-once and regular if and only if its BDD is skinny and monotone.
This completes the proof. ∎
Verification
Each variable appears at most once in a skinny BDD by definition, which enforces read-once evaluation along every path. The absence of multiple occurrences prevents any dependency duplication that would violate the read-once condition.
Monotonicity is consistent with the restriction that each decision node separates inputs in a single direction toward $\top$ or $\bot$ without reversal caused by re-encountering variables.
Conversely, any read-once function has a unique occurrence of each variable in its evaluation structure, forcing exactly one corresponding BDD node per variable, which matches the skinny condition.
Regularity follows because the ordered BDD representation induced by the read-once structure prevents reordering conflicts or repeated variable tests, matching the definition used in Section 7.1.4.
Notes
The equivalence hinges on the fact that “skinny” removes sharing and merging beyond the linear decision spine, so the BDD behaves like a decision chain rather than a dag. Monotonicity then fixes the orientation of each branch, eliminating ambiguity in sink assignment and ensuring that the read-once formula can be reconstructed uniquely from the BDD structure.