The Compilability Thresholds of 2-CNF to OBDD

Abstract

We prove the existence of two thresholds regarding the compilability of random 2-CNF formulas to OBDDs. The formulas are drawn from ${\mathcal{F}}_2(n,\hat{I}´n)$, the uniform distribution over all 2-CNFs with $\hat{I}´n$ clauses and $n$ variables, with $\hat{I}´\ge 0$ a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in $n$ if $0\le \hat{I}´<1/2$ or if $\hat{I}´>1$. On the other hand, for $1/2<\hat{I}´<1$, with high probability, the random $2$-CNF admits only OBDDs of size exponential in $n$. It is no coincidence that the two ``compilability thresholds'' are $\hat{I}´=1/2$ and $\hat{I}´=1$. Both are known thresholds for other CNF properties, namely, $\hat{I}´=1$ is the satisfiability threshold for 2-CNF while $\hat{I}´=1/2$ is the treewidth threshold, i.e., the point where the treewidth of the primal graph jumps from constant to linear in $n$ with high probability.

This version fixes Definition 14 and Definition 18 and correct the lower bound in Theorem 9. Extended version with proofs of the paper accepted at SAT'26