Document Open Access Logo

Automated Reencoding Meets Graph Theory

Authors Benjamin Przybocki , Bernardo Subercaseaux , Marijn J. H. Heule

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.29.pdf
  • Filesize: 1.21 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Graph theory
Keywords
  • SAT solving
  • CNF encodings
  • BVA
  • Rectifier networks

Metrics

Abstract

Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can be constructed by an idealized BVA algorithm. Based on this insight, we prove new results about the behavior and limitations of BVA and its interaction with other preprocessing techniques. We show that idealized BVA, plus some minor additional preprocessing (e.g., equivalent literal substitution), can reencode any 2-CNF formula with n variables into an equivalent 2-CNF formula with (lg(3)/4 + o(1)) n²/(lg n) clauses. Furthermore, we show that without the additional preprocessing the constant factor worsens from lg(3)/4 ≈ 0.396 to 1, and that no reencoding method can achieve a constant below 0.25. On the other hand, for the at-most-one constraint on n variables, we prove that idealized BVA cannot reencode this constraint using fewer than 3n-6 clauses, a bound that we prove is achieved by actual implementations. In particular, this shows that the product encoding for at-most-one, which uses 2n+o(n) clauses, cannot be constructed by BVA regardless of the heuristics used. Finally, our graph-theoretic characterization of BVA allows us to leverage recent work in algorithmic graph theory to develop a drastically more efficient implementation of BVA that achieves a comparable clause reduction on random monotone 2-CNF formulas.

Cite As Get BibTex

Benjamin Przybocki, Bernardo Subercaseaux, and Marijn J. H. Heule. Automated Reencoding Meets Graph Theory. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.29

Author Details

Benjamin Przybocki
  • Carnegie Mellon University, Pittsburgh, PA, USA
Bernardo Subercaseaux
  • Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

All authors were supported by NSF grant DMS-2434625.
  • Przybocki, Benjamin: Przybocki was supported by the NSF Graduate Research Fellowship Program under Grant No. DGE-2140739.

References

  1. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. A parametric approach for smaller and better encodings of cardinality constraints. In Christian Schulte, editor, Principles and Practice of Constraint Programming, pages 80-96, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  2. Peter Allen. Almost every 2-SAT function is unate. Israel J. Math., 161:311-346, 2007. URL: https://doi.org/10.1007/s11856-007-0081-z.
  3. József Balogh, Dingding Dong, Bernard Lidický, Nitya Mani, and Yufei Zhao. Nearly all k-SAT functions are unate. In Proceedings of the 55th Annual ACM Symposium on Theory of Computing, STOC 2023, pages 958-962, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3564246.3585123.
  4. Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023. Google Scholar
  5. Armin Biere. exactly one clauses · Issue #39 · arminbiere/kissat - github.com. https://github.com/arminbiere/kissat/issues/39#issuecomment-1686043817, 2023. [Accessed 06-06-2025].
  6. Armin Biere. cadical/src/factor.cpp at master · arminbiere/cadical - github.com. https://github.com/arminbiere/cadical/blob/master/src/factor.cpp, 2026. [Accessed 06-02-2026].
  7. Jingchao Chen. A new SAT encoding of the at-most-one constraint. Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation, page 8, 2010. Google Scholar
  8. Dmitry Chistikov, Szabolcs Iván, Anna Lubiw, and Jeffrey Shallit. Fractional coverings, greedy coverings, and rectifier networks. In Heribert Vollmer and Brigitte Vallée, editors, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017), volume 66 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:14. Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.23.
  9. Vijay Ganesh and Moshe Y. Vardi. On the Unreasonable Effectiveness of SAT Solvers, pages 547-566. Cambridge University Press, 2021. URL: https://doi.org/10.1017/9781108637435.032.
  10. Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective auxiliary variables via structured reencoding. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:19. Dagstuhl, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.11.
  11. Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Helsinki, Finland, 2024. Google Scholar
  12. Marijn J. H. Heule, Matti Järvisalo, and Armin Biere. Efficient CNF simplification based on binary implication graphs. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011, pages 201-215. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_17.
  13. Marijn J. H. Heule and Manfred Scheucher. Happy ending: An empty hexagon in every set of 30 points. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 61-80, Cham, 2024. Springer Nature Switzerland. Google Scholar
  14. Szabolcs Iván, Ádám D. Lelkes, Judit Nagy-György, Balázs Szörényi, and György Turán. Biclique coverings, rectifier networks and the cost of ε-removal. In Helmut Jürgensen, Juhani Karhumäki, and Alexander Okhotin, editors, Descriptional Complexity of Formal Systems, pages 174-185, Cham, 2014. Springer International Publishing. Google Scholar
  15. Stasys Jukna. Computational Complexity of Graphs. In Advances in Network Complexity, chapter 5, pages 99-153. John Wiley & Sons, Ltd, 2013. URL: https://doi.org/10.1002/9783527670468.ch05.
  16. Stasys Jukna and Igor Sergeev. Complexity of linear boolean operators. Found. Trends Theor. Comput. Sci., 9(1):1-123, 2013. URL: https://doi.org/10.1561/0400000063.
  17. Markus Kirchweger, Tomáš Peitl, Bernardo Subercaseaux, and Stefan Szeider. From the finite to the infinite: Sharper asymptotic bounds on Norin’s conjecture via SAT, 2025. URL: https://doi.org/10.48550/arXiv.2511.08386.
  18. Andrew Krapivin, Benjamin Przybocki, Nicolás Sanhueza-Matamala, and Bernardo Subercaseaux. Optimal and efficient partite decompositions of hypergraphs, 2025. URL: https://doi.org/10.48550/arXiv.2511.11855.
  19. Oleg Lupanov. On rectifier and switching-and-rectifier circuits. Doklady Academii nauk SSSR, 111, 1956. Available at https://web.vu.lt/mif/s.jukna/boolean/lupanov56.pdf, thanks to Stasys Jukna.
  20. Norbert Manthey, Marijn J. H. Heule, and Armin Biere. Automated reencoding of boolean formulas. In Haifa Verification Conference, pages 102-117. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-39611-3_14.
  21. Éduard Ivanovich Nechiporuk. The topological principles of self-correction. Problemy Kibernet., 21:5-102, 1969. Available in Russian at https://web.vu.lt/mif/s.jukna/boolean/Russians/Nechiporuk-1969a.pdf, thanks to Stasys Jukna.
  22. Benjamin Przybocki, Bernardo Subercaseaux, and Marijn J. H. Heule. Automated reencoding meets graph theory, 2026. URL: https://doi.org/10.48550/arXiv.2603.27774.
  23. Long Qian, Eric Wang, Bernardo Subercaseaux, and Marijn J. H. Heule. Unfolding boxes with local constraints. In Automated Deduction – CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings, pages 736-754, Berlin, Heidelberg, 2025. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-99984-0_38.
  24. Bernardo Subercaseaux. Asymptotically smaller encodings for graph problems and scheduling, 2025. (ModRef workshop). URL: https://doi.org/10.48550/arXiv.2506.14042.
  25. Bernardo Subercaseaux and Marijn J. H. Heule. The packing chromatic number of the infinite square grid is 15. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, volume 13993 of Lecture Notes in Computer Science, pages 389-406. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_20.
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