Document Open Access Logo

Trusted Scalable SAT Solving with On-The-Fly LRAT Checking

Author Dominik Schreiber

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.25.pdf
  • Filesize: 1.12 MB
  • 19 pages

Document Identifiers

Author Details

Dominik Schreiber
  • Karlsruhe Institute of Technology, Germany

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 882500). 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.

Acknowledgements

The author thanks Marijn J. H. Heule, who inspired and encouraged this work; Florian Pollitt, Mathias Fleury, and Armin Biere who enabled this work with their enhancements to CaDiCaL [Pollitt et al., 2023]; Peter Sanders for helpful discussions and valuable remarks; Patrick Hegemann for double-checking cryptographic details; and all anonymous reviewers for their valuable feedback.

Cite AsGet BibTex

Dominik Schreiber. Trusted Scalable SAT Solving with On-The-Fly LRAT Checking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.25

Abstract

Recent advances have enabled powerful distributed SAT solvers to emit proofs of unsatisfiability, which renders them as trustworthy as sequential solvers. However, this mode of operation is still lacking behind conventional distributed solving in terms of scalability. We argue that the core limiting factor of such approaches is the requirement of a single, persistent artifact at the end of solving that is then checked independently (and sequentially). As an alternative, we propose a bottleneck-free setup that exploits recent advancements in producing and processing LRAT information to immediately check all solvers' reasoning on-the-fly during solving. In terms of clause sharing, our approach transfers the guarantee of a derived clause’s soundness from the sending to the receiving side via cryptographic signatures. Experiments with up to 2432 cores (32 nodes) indicate that our approach reduces the running time overhead incurred by proof checking by an order of magnitude, down to a median overhead of ≤ 42% over non trusted solving.

Subject Classification

ACM Subject Classification
  • Hardware → Theorem proving and SAT solving
  • Theory of computation → Automated reasoning
  • Computing methodologies → Distributed algorithms
Keywords
  • SAT solving
  • distributed algorithms
  • proofs

Metrics

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

Supplementary Materials

References

  1. Jean-Philippe Aumasson and Daniel J. Bernstein. SipHash: a fast short-input PRF. In International Conference on Cryptology in India, pages 489-508. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-34931-7_28.
  2. 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.
  3. Anton Belov, Marijn J. H. Heule, and João Marques-Silva. MUS extraction using clausal proofs. In Theory and Applications of Satisfiability Testing (SAT), volume 8561, pages 48-57. Springer, Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_5.
  4. Dirk Beyer. Automatic verification of C and Java programs: SV-COMP 2019. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 133-155. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17502-3_9.
  5. Armin Biere. Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In SAT Competition, volume 2013, page 1, 2013. URL: https://fmv.jku.at/papers/Biere-SAT-Competition-2013-Lingeling.pdf.
  6. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart, and incrementality. Journal of automated reasoning, 61:333-365, 2018. URL: https://doi.org/10.1007/s10817-018-9455-7.
  7. Bart Bogaerts, Jakob Nordström, Andy Oertel, and Cagrı Uluç Yıldırımoglu. Crafted benchmark formulas requiring symmetry breaking and/or parity reasoning. In SAT Competition, page 67, 2023. URL: https://researchportal.helsinki.fi/files/269128852/sc2023_proceedings.pdf.
  8. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Theory and Applications of Satisfiability Testing (SAT), pages 44-57. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_6.
  9. Mark Alexander Burgess, Charles Gretton, Josh Milthorpe, Luke Croak, Thomas Willingham, and Alwen Tiu. Dagster: Parallel structured search with case studies. In Pacific Rim Int. Conf. Artificial Intelligence, pages 75-89. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-20862-1_6.
  10. Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Code-level model checking in the software development workflow. In ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice, pages 11-20, 2020. URL: https://doi.org/10.1145/3377813.3381347.
  11. Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal methods in system design, 19:7-34, 2001. URL: https://doi.org/10.1023/A:1011276507260.
  12. Cayden R. Codel, Joseph E. Reeves, and Randal E. Bryant. Pigeon hole and mutilated chessboard with mixed constraint encodings and symmetry-breaking. In SAT Competition, page 72, 2023. URL: https://researchportal.helsinki.fi/files/269128852/sc2023_proceedings.pdf.
  13. Byron Cook. Automated reasoning’s scientific frontiers. https://www.amazon.science/blog/automated-reasonings-scientific-frontiers, 2021. Amazon Science.
  14. Luis Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Automated Deduction - CADE 26, pages 220-236, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  15. Adnan Darwiche and Knot Pipatsrisawat. Complete algorithms. In Handbook of Satisfiability, pages 101-132. IOS Press, 2021. URL: https://doi.org/10.3233/faia200987.
  16. Daniel DeFreez, Antara Bhowmick, Ignacio Laguna, and Cindy Rubio-González. Detecting and reproducing error-code propagation bugs in MPI implementations. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 187-201, 2020. URL: https://doi.org/10.1145/3332466.3374515.
  17. Thorsten Ehlers, Dirk Nowotka, and Philipp Sieweck. Communication in massively-parallel SAT solving. In International Conference on Tools with Artificial Intelligence (ICTAI), pages 709-716. IEEE, 2014. URL: https://doi.org/10.1109/ictai.2014.111.
  18. Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of SAT. Communications of the ACM, 66(6):64-72, 2023. URL: https://doi.org/10.1145/3560469.
  19. Mathias Fleury and Armin Biere. Scalable proof producing multi-threaded SAT solving with Gimsatul through sharing instead of copying clauses. In Pragmatics of SAT, 2022. Google Scholar
  20. 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.
  21. Edgar N. Gilbert, F. Jessie MacWilliams, and Neil J. A. Sloane. Codes which detect deception. Bell System Technical Journal, 53(3):405-424, 1974. URL: https://doi.org/10.1002/j.1538-7305.1974.tb02751.x.
  22. Marijn J. H. Heule. The DRAT format and DRAT-trim checker. CoRR, abs/1610.06229, 2016. URL: https://doi.org/10.48550/arXiv.1610.06229.
  23. Marijn J. H. Heule, Warren Hunt, and Nathan Wetzler. Trimming while checking clausal proofs. In Formal Methods in Computer-Aided Design, pages 181-188. IEEE, 2013. URL: https://doi.org/10.1109/fmcad.2013.6679408.
  24. Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Nathan Wetzler. Efficient, verified checking of propositional proofs. In International Conference on Interactive Theorem Proving, pages 269-284, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_18.
  25. Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In Haifa Verification Conference, pages 50-65. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-34188-5_8.
  26. Marijn J. H. Heule, Norbert Manthey, and Tobias Philipp. Validating unsatisfiability results of clause sharing parallel SAT solvers. In Pragmatics of SAT, pages 12-25, 2014. URL: https://doi.org/10.29007/6vwg.
  27. Alexey Ignatiev, António Morgado, and João Marques-Silva. On tackling the limits of resolution in SAT solving. In Theory and Applications of Satisfiability Testing (SAT), pages 164-183. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_11.
  28. George Katsirelos, Ashish Sabharwal, Horst Samulowitz, and Laurent Simon. Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers. In AAAI Conference on Artificial Intelligence, volume 27, pages 481-488, 2013. URL: https://doi.org/10.1609/aaai.v27i1.8660.
  29. Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn JH Heule. Extended resolution simulates DRAT. In International Joint Conference on Automated Reasoning, pages 516-531. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_34.
  30. Peter Lammich. Efficient verified (UN)SAT certificate checking. Journal of Automated Reasoning, 64(3):513-532, 2020. URL: https://doi.org/10.1007/s10817-019-09525-z.
  31. Xavier Leroy. The CompCert C verified compiler: Documentation and user’s manual. Technical report, Inria, 2023. URL: https://inria.hal.science/hal-01091802v11.
  32. Ziqing Luo, Manchun Zheng, and Stephen F. Siegel. Verification of MPI programs using CIVL. In 24th European MPI Users' Group Meeting, pages 1-11, 2017. URL: https://doi.org/10.1145/3127024.3127032.
  33. Norbert Manthey, Tobias Philipp, and Christoph Wernhard. Soundness of inprocessing in clause sharing SAT solvers. In Theory and Applications of Satisfiability Testing (SAT), pages 22-39. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_4.
  34. João Marques-Silva and Karem A. Sakallah. Robust search algorithms for test pattern generation. In IEEE International Symposium on Fault Tolerant Computing, pages 152-161. IEEE, 1997. URL: https://doi.org/10.1109/ftcs.1997.614088.
  35. João Marques-Silva and Karem A. Sakallah. Boolean satisfiability in electronic design automation. In Annual Design Automation Conference (DAC), pages 675-680, 2000. URL: https://doi.org/10.1145/337292.337611.
  36. 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. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_18.
  37. 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, 2024. In preparation. Google Scholar
  38. Alexander Nadel. Solving huge instances with Intel(R) SAT solver. In Theory and Applications of Satisfiability Testing (SAT). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.17.
  39. Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT checking than solving with CaDiCaL. In Theory and Applications of Satisfiability Testing (SAT). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.21.
  40. Peter Sanders and Dominik Schreiber. Decentralized online scheduling of malleable NP-hard jobs. In European Conference on Parallel Processing (Euro-Par), pages 119-135. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-12597-3_8.
  41. André Schidler and Stefan Szeider. SAT-based decision tree learning for large data sets. In AAAI Conference on Artificial Intelligence, volume 35, pages 3904-3912, 2021. URL: https://doi.org/10.1609/aaai.v35i5.16509.
  42. Dominik Schreiber. Lilotane: A lifted SAT-based approach to hierarchical planning. Journal of Artificial Intelligence Research (JAIR), 70:1117-1181, 2021. URL: https://doi.org/10.1613/jair.1.12520.
  43. Dominik Schreiber. Scalable SAT Solving and its Application. PhD thesis, Karlsruhe Institute of Technology, 2023. URL: https://doi.org/10.5445/IR/1000165224.
  44. Dominik Schreiber and Peter Sanders. Scalable SAT solving in the cloud. In Theory and Applications of Satisfiability Testing (SAT), pages 518-534. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_35.
  45. Dominik Schreiber and Peter Sanders. MallobSat: Scalable SAT solving by clause sharing. Journal of Artificial Intelligence Research (JAIR), 2024. In press. Google Scholar
  46. Bianca Schroeder, Eduardo Pinheiro, and Wolf-Dietrich Weber. DRAM errors in the wild: a large-scale field study. ACM SIGMETRICS Performance Evaluation Review, 37(1):193-204, 2009. URL: https://doi.org/10.1145/2492101.1555372.
  47. Laurent Simon. Post mortem analysis of SAT solver proofs. In Pragmatics of SAT, pages 26-40, 2014. URL: https://doi.org/10.29007/gpp8.
  48. Carsten Sinz, Wolfgang Blochinger, and Wolfgang Küchlin. PaSAT - parallel SAT-checking with lemma exchange: Implementation and applications. Electronic Notes in Discrete Mathematics, 9:205-216, 2001. URL: https://doi.org/10.1016/s1571-0653(04)00323-3.
  49. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Theory and Applications of Satisfiability Testing (SAT), pages 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  50. Yong Kiam Tan, Marijn J. H. Heule, and Magnus Myreen. Verified LRAT and LPR proof checking with cake_lpr. In SAT Competition, page 89, 2023. URL: https://researchportal.helsinki.fi/files/269128852/sc2023_proceedings.pdf.
  51. Anh Vo, Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, and Rajeev Thakur. Formal verification of practical MPI programs. ACM Sigplan Notices, 44(4):261-270, 2009. URL: https://doi.org/10.1145/1594835.1504214.
  52. Sean Weaver and Marijn J. H. Heule. Constructing minimal perfect hash functions using SAT technology. In AAAI Conference on Artificial Intelligence, volume 34, pages 1668-1675, 2020. URL: https://doi.org/10.1609/aaai.v34i02.5529.
  53. Lihao Xu and Cheng Huang. Computation-efficient multicast key distribution. IEEE Transactions on Parallel and Distributed Systems, 19(5):577-587, 2008. URL: https://doi.org/10.1109/TPDS.2007.70759.
  54. Xindi Zhang, Zhihan Chen, and Shaowei Cai. PRS: A new parallel/distributed framework for SAT. In SAT Competition, pages 39-40, 2023. URL: https://researchportal.helsinki.fi/files/269128852/sc2023_proceedings.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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