The Compilability Thresholds of 2-CNF to OBDD

TL;DR

This paper establishes two thresholds for the size of OBDDs representing random 2-CNF formulas, showing polynomial size below 1/2 and above 1, but exponential size in between.

Contribution

It identifies and proves the existence of two specific thresholds in the compilability of 2-CNF formulas to OBDDs, linking them to known phase transitions.

Findings

Polynomial OBDD size for $oldsymbol{ ext{0} extless oldsymbol{ extdelta} extless extbf{1/2}}$ and $oldsymbol{ extdelta} extgreater extbf{1}$

Exponential OBDD size for $oldsymbol{ ext{1/2} extless extdelta extless extbf{1}}$

Thresholds coincide with known phase transitions in 2-CNF properties

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,\delta n)$, the uniform distribution over all 2-CNFs with $\delta n$ clauses and $n$ variables, with $\delta \geq 0$ a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in $n$ if $0 \leq \delta < 1/2$ or if $\delta > 1$. On the other hand, for $1/2 < \delta < 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 $\delta = 1/2$ and $\delta = 1$. Both are known thresholds for other CNF properties, namely, $\delta = 1$ is the satisfiability threshold for 2-CNF while $\delta = 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.