Document Open Access Logo

The Compilability Thresholds of 2-CNF to OBDD

Authors Alexis de Colnet , Alfons Laarman , Joon Hyung Lee

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.13.pdf
  • Filesize: 0.95 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Randomness, geometry and discrete structures
Keywords
  • Knowledge Compilation
  • OBDD
  • Random CNF
  • Phase Transition

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.SAT.2026.13

Author Details

Alexis de Colnet
  • Leiden University, The Netherlands
Alfons Laarman
  • Leiden University, The Netherlands
Joon Hyung Lee
  • Leiden University, The Netherlands

Funding

de Colnet and Laarman are supported by the Netherlands Organization for Scientific Research (NWO/OCW) as part of Quantum Limits (project number SUMMIT.1.1016).
  • Lee, Joon Hyung: Lee is supported by the Dutch Research Council (NWO) as part of the project Boosting the Search for New Quantum Algorithms with AI (BoostQA), file number NGF.1623.23.033, under the research programme Quantum Technologie 2023.

References

  1. Dimitris Achlioptas. Random Satisfiabiliy. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 437-462. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200993.
  2. Dimitris Achlioptas, Amin Coja-Oghlan, Max Hahn-Klimroth, Joon Lee, Noëla Müller, Manuel Penschuck, and Guangyan Zhou. The number of satisfying assignments of random 2-SAT formulas. Random Structures & Algorithms, 58(4):609-647, 2021. URL: https://doi.org/10.1002/rsa.20993.
  3. Peter Allen. Almost every 2-SAT function is unate. Israel Journal of Mathematics, 161(1):311-346, 2007. URL: https://doi.org/10.1007/s11856-007-0081-z.
  4. Antoine Amarilli, Florent Capelli, Mikaël Monet, and Pierre Senellart. Connecting Knowledge Compilation Classes and Width Parameters. Theory Comput. Syst., 64(5):861-914, 2020. URL: https://doi.org/10.1007/S00224-019-09930-2.
  5. László Babai, Péter Hajnal, Endre Szemerédi, and György Turán. A lower bound for read-once-only branching programs. Journal of Computer and System Sciences, 35(2):153-162, 1987. URL: https://doi.org/10.1016/0022-00008790010-9.
  6. Andreas Basse-O'Connor, Tobias Lindhardt Overgaard, and Mette Skjøtt. On the Regularity of Random 2-SAT and 3-SAT. arXiv preprint arXiv:2504.11979, 2025. URL: https://doi.org/10.48550/arXiv.2504.11979.
  7. Hans L. Bodlaender. A Partial k-Arboretum of Graphs with Bounded Treewidth. Theor. Comput. Sci., 209(1-2):1-45, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00228-4.
  8. Beate Bollig and Ingo Wegener. Improving the Variable Ordering of OBDDs Is NP-Complete. IEEE Trans. Computers, 45(9):993-1002, 1996. URL: https://doi.org/10.1109/12.537122.
  9. Beate Bollig and Ingo Wegener. A very simple function that requires exponential size read-once branching programs. Inf. Process. Lett., 66(2):53-57, April 1998. URL: https://doi.org/10.1016/S0020-0190(98)00042-8.
  10. Vasek Chvátal and Bruce A. Reed. Mick Gets Some (the Odds Are on His Side). In 33rd Annual Symposium on Foundations of Computer Science, Pittsburgh, Pennsylvania, USA, October 24-27, 1992, pages 620-627. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/SFCS.1992.267789.
  11. Adnan Darwiche and Pierre Marquis. A Knowledge Compilation Map. J. Artif. Intell. Res., 17:229-264, 2002. URL: https://doi.org/10.1613/JAIR.989.
  12. Alexis de Colnet and Stefan Mengel. Characterizing tseitin-formulas with short regular resolution refutations. J. Artif. Intell. Res., 76:265-286, 2023. URL: https://doi.org/10.1613/JAIR.1.13521.
  13. Paul Erdös and Alfréd Rényi. On the evolution of random graphs. Publ. Math. Inst. Hungar. Acad. Sci, 5(1):17-61, 1960. Google Scholar
  14. Andrea Ferrara, Guoqiang Pan, and Moshe Y. Vardi. Treewidth in verification: Local vs. global. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, Lecture Notes in Computer Science, pages 489-503. Springer, 2005. URL: https://doi.org/10.1007/11591191_34.
  15. Luke Friedman and Yixin Xu. Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams. In Andrei A. Bulatov and Arseny M. Shur, editors, Computer Science - Theory and Applications - 8th International Computer Science Symposium in Russia, CSR 2013, Ekaterinburg, Russia, June 25-29, 2013. Proceedings, volume 7913 of Lecture Notes in Computer Science, pages 127-138. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38536-0_11.
  16. Alan Frieze and Michał Karoński. Introduction to random graphs. Cambridge University Press, 2015. URL: https://doi.org/10.1017/CBO9781316339831.
  17. Andreas Goerdt. A Threshold for Unsatisfiability. J. Comput. Syst. Sci., 53(3):469-486, 1996. URL: https://doi.org/10.1006/JCSS.1996.0081.
  18. Rahul Gupta, Subhajit Roy, and Kuldeep S. Meel. Phase Transition Behavior in Knowledge Compilation. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 358-374. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_21.
  19. Anna Gál. A simple function that requires exponential size read-once branching programs. Information Processing Letters, 62(1):13-16, 1997. URL: https://doi.org/10.1016/S0020-0190(97)00041-0.
  20. Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight bounds for tseitin formulas. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, Haifa, Israel, August 2-5, 2022, LIPIcs, pages 6:1-6:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.6.
  21. Svante Janson, Tomasz Luczak, and Andrzej Rucinski. Random graphs. Wiley-Interscience series in discrete mathematics and optimization. Wiley, 2000. URL: https://doi.org/10.1002/9781118032718.
  22. Donald E. Knuth. The Art of Computer Programming. Volume 4, Fascicle 6. Satisfiability. Addison-Wesley, 2015. Google Scholar
  23. Choongbum Lee, Joonkyung Lee, and Sang-il Oum. Rank-width of random graphs. Journal of Graph Theory, 70(3):339-347, 2012. URL: https://doi.org/10.1002/jgt.20620.
  24. Mette Marie Skjøtt Rasmussen. Fixing Variables in Random Satisfiability Problems. PhD thesis, Aarhus University, 2025. URL: https://data.math.au.dk/publications/phd/2025/math-phd-2025-mmsr.pdf.
  25. Igor Razgon. Classification of OBDD size for monotone 2-cnfs. In Petr A. Golovach and Meirav Zehavi, editors, 16th International Symposium on Parameterized and Exact Computation, IPEC 2021, Lisbon, Portugal, September 8-10, 2021, LIPIcs, pages 25:1-25:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.IPEC.2021.25.
  26. Marko Samer and Stefan Szeider. Fixed-Parameter Tractability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 693-736. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201000.
  27. Claude E. Shannon. The Synthesis of Two-Terminal Switching Circuits. Bell System Technical Journal, 28(1):59-98, 1949. URL: https://doi.org/10.1002/j.1538-7305.1949.tb03624.x.
  28. Martin Vatshelle. New Width Parameters of Graphs. PhD thesis, Bergen Universtiy, 2012. URL: https://hdl.handle.net/1956/6166.
  29. Ingo Wegener. On the complexity of branching programs and decision trees for clique functions. J. ACM, 35(2):461-471, 1988. URL: https://doi.org/10.1145/42282.46161.
  30. Ingo Wegener. Branching Programs and Binary Decision Diagrams. SIAM, 2000. URL: https://doi.org/10.1137/1.9780898719789.
  31. Stanislav Zák. An Exponential Lower Bound for One-Time-Only Branching Programs. In Michal Chytil and Václav Koubek, editors, Mathematical Foundations of Computer Science 1984, Praha, Czechoslovakia, September 3-7, 1984, Proceedings, Lecture Notes in Computer Science, pages 562-566. Springer, 1984. URL: https://doi.org/10.1007/BFB0030340.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact