Document Open Access Logo

A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

Authors Ruben Götz , Michael Dörr , Dominik Schreiber

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.17.pdf
  • Filesize: 1.56 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Hardware → Theorem proving and SAT solving
Keywords
  • Satisfiability
  • Proofs
  • Distributed computing

Metrics

Abstract

Unsatisfiability proofs are valuable artifacts in propositional satisfiability (SAT) since they can provide correctness guarantees and thus complete trust in reported results. In powerful parallel and distributed clause-sharing SAT solvers, existing proof technology either funnels all solver threads' relevant reasoning steps into a single proof file, which leads to scalability problems for large setups and long running times, or checks proof information in parallel in real-time, which is fully scalable but leaves no persistent artifact. We suggest an alternative approach to achieve the best of both worlds. Specifically, we consider parallel proof files that are logged and also checked in parallel. To this end, we introduce PalRUP - an LRUP-based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components. In evaluations on up to 3072 cores, we observe that our approach allows for low-overhead proof logging during solving and substantially outscales prior proof producing approaches in terms of checking performance.

Cite As Get BibTex

Ruben Götz, Michael Dörr, and Dominik Schreiber. A Natively Parallel Proof Framework for Clause-Sharing SAT Solving. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.17

Author Details

Ruben Götz
  • Karlsruhe Institute of Technology, Germany
Michael Dörr
  • Karlsruhe Institute of Technology, Germany
Dominik Schreiber
  • Karlsruhe Institute of Technology, Germany

Funding

This work was partially funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation), project number 565407588 (Project: Propositional Proofs As Big Data). The authors gratefully acknowledge the Gauss Centre for Supercomputing e.V. (https://www.gauss-centre.eu) for funding this project by providing computing time on the GCS Super-computer SuperMUC-NG at Leibniz Supercomputing Centre (https://www.lrz.de). Some of this work was performed on the HoreKa supercomputer funded by the Ministry of Science, Research and the Arts Baden-Württemberg and by the Federal Ministry of Education and Research (Germany).

Acknowledgements

The authors wish to thank Jakob Nordström and Bart Bogaerts for a fruitful discussion at SAT'24 that provided the initial inspiration for the parallel checking approach presented in this paper.

Supplementary Materials

References

  1. Tomáš Balyo and Carsten Sinz. Parallel satisfiability. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_1.
  2. Anton Belov, Marijn J. H. Heule, and João Marques-Silva. MUS extraction using clausal proofs. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014, pages 48-57, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_5.
  3. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Proc. Computer Aided Verification (CAV), pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  4. Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2 edition, 2021. URL: https://doi.org/10.3233/faia336.
  5. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. Journal of Artificial Intelligence Research, 77:1539-1589, 2023. URL: https://doi.org/10.1613/jair.1.14296.
  6. Cayden Codel, Katalin Fazekas, Marijn J. H. Heule, and Ashlin Iser, editors. Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions, 2025. URL: https://doi.org/10.34726/10379.
  7. Luis Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Automated Deduction - CADE, pages 220-236. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  8. Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere. Certifying incremental SAT solving. In Nikolaj Bjørner, Marijn Heule, and Andrei Voronkov, editors, Proc. Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 100 of EPiC Series in Computing, pages 321-340. EasyChair, 2024. URL: https://doi.org/10.29007/pdcc.
  9. Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere. Incremental inprocessing rules beyond resolution. In Joint Proceedings of the 23rd International Workshop on Satisfiability Modulo Theories (SMT’25) and of the 16th Pragmatics of SAT International Workshop (POS’25), co-located with the 28th International Conference on Theory and Applications of Satisfiability Testing (SAT’25), Glasgow, UK, 2025. Google Scholar
  10. Mathias Fleury and Armin Biere. Scalable proof producing multi-threaded SAT solving with Gimsatul through sharing instead of copying clauses. In Proc. Pragmatics of SAT, 2022. URL: https://doi.org/10.48550/arXiv.2207.13577.
  11. Rohan Fossé and Laurent Simon. On the non-degeneracy of unsatisfiability proof graphs produced by SAT solvers. In Proc. Principles and Practice of Constraint Programming (CP), pages 128-143. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_9.
  12. Nils Froleyks, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT competition 2020. Artificial Intelligence, 301:103572, 2021. URL: https://doi.org/10.1016/j.artint.2021.103572.
  13. Ruben Götz, Michael Dörr, and Dominik Schreiber. PalRUP-Check. Software, DFG-56540758, (visited on 2026-07-01). URL: https://github.com/rubenGoetz/PalRUP-Check
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26960
  14. Ruben Götz, Michael Dörr, and Dominik Schreiber. rubenGoetz/SAT26_experimental_data. Dataset, (visited on 2026-07-01). URL: https://github.com/rubenGoetz/SAT26_experimental_data
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26962
  15. Marijn J. H. Heule. Schur number five. In AAAI Conference on Artificial Intelligence, volume 32, 2018. URL: https://doi.org/10.1609/aaai.v32i1.12209.
  16. Marijn J. H. Heule and Armin Biere. Compositional propositional proofs. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 444-459. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_31.
  17. Marijn J. H. Heule, Warren Hunt, and Nathan Wetzler. Trimming while checking clausal proofs. In Proc. Formal Methods in Computer-Aided Design (FMCAD), pages 181-188. IEEE, 2013. URL: https://doi.org/10.1109/fmcad.2013.6679408.
  18. Marijn J. H. Heule, Oliver Kullmann, and Victor Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In Proc. Theory and Applications of Satisfiability Testing (SAT), pages 228-245. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  19. Marijn J. H. Heule, Norbert Manthey, and Tobias Philipp. Validating unsatisfiability results of clause sharing parallel SAT solvers. In Proc. Pragmatics of SAT, pages 12-25, 2014. URL: https://doi.org/10.29007/6vwg.
  20. George Katsirelos, Ashish Sabharwal, Horst Samulowitz, and Laurent Simon. Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers. In Proc. AAAI Conference on Artificial Intelligence, volume 27, pages 481-488, 2013. URL: https://doi.org/10.1609/aaai.v27i1.8660.
  21. Boris Konev and Alexei Lisitsa. Computer-aided proof of erdős discrepancy properties. Artificial Intelligence, 224:103-118, 2015. URL: https://doi.org/10.1016/j.artint.2015.03.004.
  22. João Marques-Silva, Inês Lynce, and Sharad Malik. CDCL SAT solving. In Handbook of Satisfiability, pages 131-153. IOS Press, 2021. URL: https://doi.org/10.3233/faia200987.
  23. Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, and Michael W. Whalen. Unsatisfiability proofs for distributed clause-sharing SAT solvers. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 348-366, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_18.
  24. Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, and Michael W. Whalen. Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers. Journal of Automated Reasoning, 69, 2025. URL: https://doi.org/10.1007/s10817-025-09725-w.
  25. Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, and Clark Barrett. Proof-stitch: Proof combination for divide and conquer SAT solvers. In Proc. Formal Methods in Computer-Aided Design (FMCAD), pages 84-88, 2022. URL: https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_14.
  26. Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT checking than solving with CaDiCaL. In Proc. Theory and Applications of Satisfiability Testing (SAT), pages 21:1-21:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.21.
  27. Peter Sanders. Fast priority queues for cached memory. Journal of Experimental Algorithmics (JEA), 5:7-es, 2000. URL: https://doi.org/10.1145/351827.384249.
  28. Peter Sanders and Tim Niklas Uhl. Engineering a distributed-memory triangle counting algorithm. In 2023 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pages 702-712, 2023. URL: https://doi.org/10.1109/IPDPS54959.2023.00076.
  29. Dominik Schreiber. Trusted Scalable SAT Solving with on-the-fly LRAT Checking. In Theory and Applications of Satisfiability Testing (SAT), pages 25:1-25:19, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.25.
  30. Dominik Schreiber, Katalin Fazekas, Mathias Fleury, and Armin Biere. Real-time proof checking for distributed incremental SAT solving. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2026. URL: https://doi.org/10.1007/978-3-032-22752-2_18.
  31. Dominik Schreiber, Niccolò Rigi-Luperti, and Armin Biere. Streamlining distributed SAT solver design. In Theory and Applications of Satisfiability Testing (SAT), 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.27.
  32. Dominik Schreiber and Peter Sanders. MallobSat: Scalable SAT Solving by Clause Sharing. Journal of Artificial Intelligence Research (JAIR), 80:1437-1495, 2024. URL: https://doi.org/10.1613/jair.1.15827.
  33. Dominik Schreiber, Peter Sanders, Niccolò Rigi-Luperti, and Ruben Götz. Mallob. Software, (visited on 2026-07-01). URL: https://github.com/domschrei/mallob
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26961
  34. Laurent Simon. Post mortem analysis of SAT solver proofs. In Proc. Pragmatics of SAT, pages 26-40, 2014. URL: https://doi.org/10.29007/gpp8.
  35. Bernardo Subercaseaux and Marijn J. H. Heule. The packing chromatic number of the infinite square grid is 15. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 389-406, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_20.
  36. Yong Kiam Tan, Marijn JH 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.
  37. Yong Kiam Tan, Magnus O Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. Journal of Functional Programming, 29:e2, 2019. URL: https://doi.org/10.1017/s0956796818000229.
  38. Yong Kiam Tan, Dominik Schreiber, Johannes Åman Pohjola, and Magnus O Myreen. Verified real-time proof checking for large-scale SAT solving. Under review, 2026. Google Scholar
  39. Yakir Vizel, Georg Weissenbacher, and Sharad Malik. Boolean satisfiability solvers and their applications in model checking. In IEEE, volume 103, pages 2021-2035, 2015. URL: https://doi.org/10.1109/JPROC.2015.2455034.
  40. Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko. Towards compositional hardware model checking certification. In Proc. Formal Methods in Computer-Aided Design (FMCAD), pages 44-54, 2023. URL: https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_12.
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