English

The Compilability Thresholds of 2-CNF to OBDD

Data Structures and Algorithms 2026-05-20 v2 Discrete Mathematics Combinatorics Probability

Abstract

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

Cite

@article{arxiv.2603.15463,
  title  = {The Compilability Thresholds of 2-CNF to OBDD},
  author = {Alexis de Colnet and Alfons Laarman and Joon Hyung Lee},
  journal= {arXiv preprint arXiv:2603.15463},
  year   = {2026}
}

Comments

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

R2 v1 2026-07-01T11:22:34.000Z