DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.13

The Compilability Thresholds of 2-CNF to OBDD

Authors: Alexis de Colnet, Alfons Laarman, and Joon Hyung Lee

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract

We prove the existence of two thresholds regarding the compilability of random 2-CNF formulas to OBDDs. The formulas are drawn from F₂(n,δn), the uniform distribution over all 2-CNFs with δ n clauses and n variables, with δ ≥ 0 a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in n if 0 ≤ δ < 1/2 or if δ > 1. On the other hand, for 1/2 < δ < 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 δ = 1/2 and δ = 1. Both are known thresholds for other CNF properties, namely, δ = 1 is the satisfiability threshold for 2-CNF while δ = 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.

Cite as

Alexis de Colnet, Alfons Laarman, and Joon Hyung Lee. The Compilability Thresholds of 2-CNF to OBDD. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{decolnet_et_al:LIPIcs.SAT.2026.13,
  author =	{de Colnet, Alexis and Laarman, Alfons and Lee, Joon Hyung},
  title =	{{The Compilability Thresholds of 2-CNF to OBDD}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.13},
  URN =		{urn:nbn:de:0030-drops-263190},
  doi =		{10.4230/LIPIcs.SAT.2026.13},
  annote =	{Keywords: Knowledge Compilation, OBDD, Random CNF, Phase Transition}
}

Search Results

Documents authored by Lee, Joon Hyung

The Compilability Thresholds of 2-CNF to OBDD

Abstract

Cite as

Thanks for your feedback!

Could not send message