2026-07-20T06:17:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26319 2026-07-16T10:50:11Z ddc:004 open_access

The Compilability Thresholds of 2-CNF to OBDD de Colnet, Alexis Laarman, Alfons Lee, Joon Hyung Knowledge Compilation OBDD Random CNF Phase Transition 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexis de Colnet and Alfons Laarman and Joon Hyung Lee 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.13 urn:nbn:de:0030-drops-263190 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.13 eng https://creativecommons.org/licenses/by/4.0/legalcode