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 , the uniform distribution over all 2-CNFs with clauses and variables, with a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in if or if . On the other hand, for , with high probability, the random -CNF admits only OBDDs of size exponential in . It is no coincidence that the two ``compilability thresholds'' are and . Both are known thresholds for other CNF properties, namely, is the satisfiability threshold for 2-CNF while is the treewidth threshold, i.e., the point where the treewidth of the primal graph jumps from constant to linear in 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