Document Open Access Logo

Problem Partitioning via Proof Prefixes

Authors Zachary Battleman , Joseph E. Reeves , Marijn J. H. Heule

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.3.pdf
  • Filesize: 1.14 MB
  • 18 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.3.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Satisfiability solving
  • parallel computing
  • problem partitioning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Satisfiability solvers have been instrumental in tackling hard problems, including mathematical challenges that require years of computation. A key obstacle in efficiently solving such problems lies in effectively partitioning them into many, frequently millions of subproblems. Existing automated partitioning techniques, primarily based on lookahead methods, perform well on some instances but fail to generate effective partitions for many others.
This paper introduces a powerful partitioning approach that leverages prefixes of proofs derived from conflict-driven clause-learning solvers. This method enables non-experts to harness the power of massively parallel SAT solving for their problems. We also propose a semantically-driven partitioning technique tailored for problems with large cardinality constraints, which frequently arise in optimization tasks. We evaluate our methods on diverse benchmarks, including combinatorial problems and formulas from SAT and MaxSAT competitions. Our results demonstrate that these techniques outperform existing partitioning strategies in many cases, offering improved scalability and efficiency.

Cite As Get BibTex

Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule. Problem Partitioning via Proof Prefixes. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.3

Author Details

Zachary Battleman
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Joseph E. Reeves
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

Supported by the National Science Foundation (NSF) under grant CCF-2415773 and funding from AFRL and DARPA under Agreement FA8750-24-9-1000.
  • Reeves, Joseph E.: Supported in part by a fellowship award under contract FA9550-21-F-0003 through the National Defense Science and Engineering Graduate (NDSEG) Fellowship Program, sponsored by the Air Force Research Laboratory (AFRL), the Office of Naval Research (ONR) and the Army Research Office (ARO).

Supplementary Materials

References

  1. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing (SAT), pages 167-180. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_18.
  2. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. MaxSAT Evaluation 2018 Benchmarks. https://helda.helsinki.fi/items/7c51d9bd-20e8-428f-8926-b2bbf151dc4c, 2018. Accessed: 2025-04-02.
  3. Olivier Bailleux and Yacine Boufkhad. Efficient cnf encoding of boolean cardinality constraints. In Francesca Rossi, editor, Principles and Practice of Constraint Programming (CP), pages 108-122, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-45193-8_8.
  4. Armin Biere. Cadical, lingeling, plingeling, treengeling and yalsat entering the sat competition 2018. Proceedings of SAT Competition, 14:316-336, 2017. Google Scholar
  5. Armin Biere and Andreas Fröhlich. Evaluating CDCL variable scoring schemes. In Theory and Applications of Satisfiability Testing (SAT), volume 9340 of LNCS, pages 405-422, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_29.
  6. Joshua Brakensiek, Marijn J. H. Heule, John Mackey, and David Narváez. The resolution of keller’s conjecture. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 48-65, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-51074-9_4.
  7. Shawn T. Brown, Paola Buitrago, Edward Hanna, Sergiu Sanielevici, Robin Scibek, and Nicholas A. Nystrom. Bridges-2: A Platform for Rapidly-Evolving and Data Intensive Research, pages 1-4. Association for Computing Machinery, New York, NY, USA, 2021. URL: https://doi.org/10.1145/3437359.3465593.
  8. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. URL: https://doi.org/10.1145/368273.368557.
  9. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Theory and Applications of Satisfiability Testing (SAT), volume 3569 of LNCS, pages 61-75. Springer, 2005. URL: https://doi.org/10.1007/11499107_5.
  10. Jon William Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania, USA, 1995. Google Scholar
  11. Youssef Hamadi, Said Jabbour, and Lakhdar Sais. Manysat: a parallel sat solver. Journal on Satisfiability, Boolean Modelling and Computation, 6(4):245-262, 2010. URL: https://doi.org/10.3233/SAT190070.
  12. Marijn J. H. Heule. Schur number five. In AAAI Conference on Artificial Intelligence, 2018. Google Scholar
  13. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In Theory and Applications of Satisfiability Testing (SAT), volume 9710 of LNCS, pages 228-245. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  14. Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding cdcl sat solvers by lookaheads. In Kerstin Eder, João Lourenço, and Onn Shehory, editors, Hardware and Software: Verification and Testing, pages 50-65, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  15. 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. URL: https://doi.org/10.1007/978-3-031-57246-3_5.
  16. Marijn J. H. Heule and Hans van Maaren. Look-Ahead Based SAT Solvers, volume 185 of FAIA, chapter 5, pages 155-184. IOS Press, February 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-155.
  17. Matti Järvisalo, Jeremias Berg, Ruben Martins, and Andreas Niskanen. MaxSAT Evaluation 2023 Benchmarks. https://maxsat-evaluations.github.io/2023/benchmarks.html, 2023. Accessed: 2024-08-13.
  18. Oliver Kullmann. Fundaments of Branching Heuristics, volume 185 of FAIA, chapter 7, pages 205-244. IOS Press, February 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-205.
  19. Chu-Min Li, Fan Xiao, Mao Luo, Felip Manyà, Zhipeng Lü, and Yu Li. Clause vivification by unit propagation in CDCL SAT solvers. Artificial Intelligence, 279(C), February 2020. URL: https://doi.org/10.1016/J.ARTINT.2019.103197.
  20. Jia Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Theory and Applications of Satisfiability Testing (SAT), volume 9710 of LNCS, pages 123-140, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_9.
  21. Joao Marques-Silva, Mikoláš Janota, Alexey Ignatiev, and Antonio Morgado. Efficient model based diagnosis with maximum satisfiability. In International Joint Conference on Artificial Intelligence (IJCAI), IJCAI'15, pages 1966-1972. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/279.
  22. João Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability, pages 131-153. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-131.
  23. Antonio Morgado, Alexey Ignatiev, and Joao Marques-Silva. Mscg: Robust core-guided maxsat solving: System description. Journal on Satisfiability, Boolean Modeling and Computation, 9:129-134, December 2015. Google Scholar
  24. Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Modulo based cnf encoding of cardinality constraints and its application to maxsat solvers. In Tools with Artificial Intelligence (ICTAI), pages 9-17, 2013. URL: https://doi.org/10.1109/ICTAI.2013.13.
  25. Joseph E Reeves, Joao Filipe, Min-Chien Hsu, Ruben Martins, and Marijn JH Heule. The impact of literal sorting on cardinality constraint encodings. In Conference on Artificial Intelligence (AAAI). AAAI Press, 2025. Google Scholar
  26. Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant. From Clauses to Klauses. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification (CAV), volume 14681 of Lecture Notes in Computer Science, pages 110-132. Springer, 2024. Google Scholar
  27. Joseph E Reeves, Benjamin Kiesl-Reiter, and Marijn JH Heule. Propositional proof skeletons. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 329-347. Springer, 2023. Google Scholar
  28. R.K.Guy. A combinatorial problem. Nabla (Bulletin of the Malaysian Mathematical Society), 7, 1960. Google Scholar
  29. Dominik Schreiber and Peter Sanders. Scalable sat solving in the cloud. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021, pages 518-534, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-80223-3_35.
  30. Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Principles and Practice of Constraint Programming (CP), volume 3709 of LNCS, pages 827-831, 2005. URL: https://doi.org/10.1007/11564751_73.
  31. Mate Soos, Raghav Kulkarni, and Kuldeep S Meel. : gazing in the black box of sat solving. In Theory and Applications of Satisfiability Testing (SAT), pages 371-387. Springer, 2019. Google Scholar
  32. Bernardo Subercaseaux and Marijn Heule. Toward optimal radio colorings of hypercubes via sat-solving. In Ruzica Piskac and Andrei Voronkov, editors, Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 94 of EPiC Series in Computing, pages 386-404. EasyChair, 2023. URL: https://doi.org/10.29007/QRMP.
  33. 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, pages 389-406, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-30823-9_20.
  34. Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, and Ruben Martins. Automated mathematical discovery and verification: Minimizing pentagons in the plane. In Andrea Kohlhase and Laura Kovács, editors, Intelligent Computer Mathematics, pages 21-41, Cham, 2024. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-66997-2_2.
  35. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. Verified propagation redundancy and compositional UNSAT checking in CakeML. International Journal on Software Tools for Technology Transfer, 25(2):167-184, 2023. URL: https://doi.org/10.1007/S10009-022-00690-Y.
  36. Ed Wynn. A comparison of encodings for cardinality constraints in a SAT solver. ArXiv, abs/1810.12975, 2018. URL: https://arxiv.org/abs/1810.12975.
  37. Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel. Explaining SAT Solving Using Causal Reasoning. In Meena Mahajan and Friedrich Slivovsky, editors, Theory and Applications of Satisfiability Testing (SAT), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.SAT.2023.28.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact