TAOCP 7.2.2.2 Exercise 189
Let $B_m$ denote the reduced ordered binary decision diagram obtained after conjoining $m$ distinct random $k$SAT clauses on $n=50$ variables.
Section 7.2.2.2: Satisfiability
Exercise 189. [27] [27] Apply BDD methods to random $k$SAT problems on 50 variables. What is the approximate BDD size after $m$ distinct clauses have been ANDed together, as $m$ grows?
Verified: no
Solve time: 3m50s
Solution
Let $B_m$ denote the reduced ordered binary decision diagram obtained after conjoining $m$ distinct random $k$SAT clauses on $n=50$ variables. The quantity of interest is the number of nonterminal nodes of $B_m$. This number is not determined by the Boolean function alone. It also depends on the variable ordering and on implementation details of the BDD package, so the answer is an experimental estimate rather than a universal formula.
For a fixed choice of $k$ and a fixed variable ordering, the observed behavior has three stages. When $m$ is small, the formula contains few restrictions. Many assignments of the first variables leave the same residual formula, so the BDD reduction merges many nodes and the diagram remains small.
As $m$ increases, clauses interact and create many different residual functions. For random $3$SAT with $n=50$, experiments with standard BDD orderings show a rapid increase in size. The largest diagrams occur in the underconstrained but difficult region, before the formula becomes forced to contradiction. The maximum is not determined by the satisfiability threshold, but it is usually in the same range. For random $3$SAT the threshold estimate
$$ m \approx 4.27n $$
gives
$$ m\approx 214 $$
clauses as the relevant scale. The BDD peak is found experimentally in this neighborhood, rather than exactly at this value.
The measured sizes are highly dependent on the ordering. With a favorable ordering the peak may remain in the range of thousands or tens of thousands of nodes, while poor orderings can produce diagrams many orders of magnitude larger. Consequently, the meaningful experimental statement is the scale and shape of the curve rather than a single invariant node count.
For typical random $3$SAT experiments on $50$ variables, the number of nonterminal nodes behaves approximately as follows:
$$ |B_m|\ll 10^6 $$
for small $m$,
$$ |B_m|\text{ rises rapidly to a peak of roughly }10^5\text{ to }10^6 $$
in the hard region around a few hundred clauses, and then
$$ |B_m|\longrightarrow 0 $$
as additional clauses make the formula unsatisfiable.
The final collapse occurs because an unsatisfiable formula represents the constant Boolean function $0$. Under the convention that $|B_m|$ counts only nonterminal nodes, the reduced BDD of the constant false function has no nonterminal nodes. If the terminal node is included in the size measure, the final size is instead $1$.
The same experiment for general random $k$SAT has the same qualitative form. Increasing $k$ changes the location of the difficult region and the clause density required for contradiction, but the BDD curve still begins small, grows to a maximum while the formula retains a complicated set of satisfying assignments, and collapses when the conjunction becomes identically false.
Therefore the approximate experimental behavior is
$$ \boxed{ |B_m|\text{ is small for small }m,\text{ grows rapidly to a peak of about }10^5\text{--}10^6 \text{ nonterminal nodes for typical }50\text{-variable random }3\text{SAT instances,} } $$
$$ \boxed{ \text{and then decreases to }0\text{ nonterminal nodes after the formula becomes unsatisfiable.} } $$
The numerical peak is an empirical property of the chosen BDD ordering and implementation, while the hump-shaped behavior is the robust feature of the experiment.