Document Open Access Logo

Migrating Solver State

Authors Armin Biere , Md Solimul Chowdhury , Marijn J. H. Heule , Benjamin Kiesl , Michael W. Whalen

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.27.pdf
  • Filesize: 1.34 MB
  • 24 pages

Document Identifiers

Author Details

Armin Biere
  • University of Freiburg, Germany
Md Solimul Chowdhury
  • Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA
  • Amazon Web Services, Inc., Pittsburgh, PA, USA
Benjamin Kiesl
  • Amazon Web Services, Inc., Munich, Germany
Michael W. Whalen
  • Amazon Web Services, Inc., Minneapolis, MN, USA
  • The University of Minnesota, Minneapolis, MN, USA

Funding

  • Chowdhury, Md Solimul: partially supported by NSF grant CCF-2015445.
  • Heule, Marijn J. H.: partially supported by NSF grant CCF-2015445.

Cite AsGet BibTex

Armin Biere, Md Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, and Michael W. Whalen. Migrating Solver State. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.27

Abstract

We present approaches to store and restore the state of a SAT solver, allowing us to migrate the state between different compute resources, or even between different solvers. This can be used in many ways, e.g., to improve the fault tolerance of solvers, to schedule SAT problems on a restricted number of cores, or to use dedicated preprocessing tools for inprocessing. We identify a minimum viable subset of the solver state to migrate such that the loss of performance is small. We then present and implement two different approaches to state migration: one approach stores the state at the end of a solver run whereas the other approach stores the state continuously as part of the proof trace. We show that our approaches enable the generation of correct models and valid unsatisfiability proofs. Experimental results confirm that the overhead is reasonable and that in several cases solver performance actually improves.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • SAT
  • SMT
  • Cloud Computing
  • Serverless Computing

Metrics

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

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 399-404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  2. Gilles Audemard and Laurent Simon. Lazy clause exchange policy for parallel SAT solvers. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 197-205. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_15.
  3. AWS Lambda system description. https://aws.amazon.com/lambda/. Accessed: 2022-02-06.
  4. Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. A flexible proof format for SAT solver-elaborator communication. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/lmcs-18(2:3)2022.
  5. Tomáš Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2021. Google Scholar
  6. Tomáš Balyo, Nils Froleyks, Marijn J.H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Finland, 2020. Google Scholar
  7. Tomáš Balyo, Peter Sanders, and Carsten Sinz. HordeSat: A massively parallel portfolio SAT solver. In Marijn Heule and Sean Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015, pages 156-172, Cham, 2015. Springer International Publishing. Google Scholar
  8. Armin Biere. CaDiCaL at the SAT Race 2019. In Marijn Heule, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Race 2019 - Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Series of Publications B, pages 8-9. University of Helsinki, 2019. Google Scholar
  9. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  10. Armin Biere and Andreas Fröhlich. Evaluating CDCL restart schemes. In Daniel Le Berre and Matti Järvisalo, editors, Proceedings of Pragmatics of SAT 2015 and 2018, volume 59 of EPiC Series in Computing, pages 1-17. EasyChair, 2019. Google Scholar
  11. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. URL: http://dblp.uni-trier.de/db/series/faia/faia185.html.
  12. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in SAT solving. Handbook of Satisfiability, 336:391-435, 2021. Google Scholar
  13. Randal E. Bryant and Marijn J. H. Heule. Dual proof generation for quantified boolean formulas with a bdd-based solver. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 433-449. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_25.
  14. Xi Cheng, Min Zhou, Xiaoyu Song, Ming Gu, and Jiaguang Sun. Parallelizing SMT solving: Lazy decomposition and conciliation. Artificial Intelligence, 257:127-157, 2018. URL: https://doi.org/10.1016/j.artint.2018.01.001.
  15. Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, and Moshe Y. Vardi. Benefits of bounded model checking at an industrial setting. In CAV, pages 436-453. Springer, 2001. URL: https://doi.org/10.1007/3-540-44585-4_43.
  16. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 61-75. Springer, 2005. URL: https://doi.org/10.1007/11499107_5.
  17. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  18. Katalin Fazekas, Armin Biere, and Christoph Scholl. Incremental inprocessing in SAT solving. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 136-154. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_9.
  19. Sadjad Fouladi, Francisco Romero, Dan Iter, Qian Li, Shuvo Chatterjee, Christos Kozyrakis, Matei Zaharia, and Keith Winstein. From laptop to lambda: Outsourcing everyday jobs to thousands of transient functional containers. In Proceedings of the 2019 USENIX Conference on Usenix Annual Technical Conference, USENIX ATC '19, pages 475-488, USA, 2019. USENIX Association. Google Scholar
  20. Carla P. Gomes and Bart Selman. Algorithm portfolios. Artif. Intell., 126(1-2):43-62, 2001. URL: http://dblp.uni-trier.de/db/journals/ai/ai126.html#GomesS01.
  21. Youssef Hamadi, Saïd Jabbour, and Lakhdar Sais. ManySAT: a parallel SAT solver. J. Satisf. Boolean Model. Comput., 6(4):245-262, 2009. URL: https://doi.org/10.3233/sat190070.
  22. Paul H Hargrove and Jason C Duell. Berkeley lab checkpoint/restart (BLCR) for linux clusters. Journal of Physics: Conference Series, 46(1):067, 2006. Google Scholar
  23. Maximilian Heisinger, Mathias Fleury, and Armin Biere. Distributed cube and conquer with paracooba. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020, pages 114-122, Cham, 2020. Springer International Publishing. Google Scholar
  24. Marijn J. H. Heule. Schur number five. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), pages 6598-6606. AAAI Press, 2018. URL: https://www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/16952.
  25. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. J. Autom. Reason., 64(3):533-554, 2020. URL: https://doi.org/10.1007/s10817-019-09516-0.
  26. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016, pages 228-245, Cham, 2016. Springer International Publishing. Google Scholar
  27. 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
  28. Marijn J. H. Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, volume 8562 of Lecture Notes in Computer Science, pages 91-106. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08587-6_7.
  29. Marijn J.H. Heule. Proofs of unsatisfiability. Handbook of Satisfiability, 336:635-668, 2021. Google Scholar
  30. Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Grid-based SAT solving with iterative partitioning and clause learning. In Jimmy Lee, editor, Principles and Practice of Constraint Programming - CP 2011, pages 385-399, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  31. Antti E. J. Hyvärinen and Christoph M. Wintersteiger. Parallel satisfiability modulo theories. In Youssef Hamadi and Lakhdar Sais, editors, Handbook of Parallel Constraint Reasoning, pages 141-178. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_5.
  32. Antti Eero Johannes Hyvärinen, Tommi A. Junttila, and Ilkka Niemelä. Partitioning SAT instances for distributed solving. In Christian G. Fermüller and Andrei Voronkov, editors, LPAR (Yogyakarta), volume 6397 of Lecture Notes in Computer Science, pages 372-386. Springer, 2010. URL: http://dblp.uni-trier.de/db/conf/lpar/lpar2010y.html#HyvarinenJN10.
  33. Franjo Ivančić, Zijiang Yang, Malay K. Ganai, Aarti Gupta, and Pranav Ashar. Efficient SAT-based bounded model checking for software verification. Theoretical Computer Science, 404(3):256-274, 2008. URL: https://doi.org/10.1016/j.tcs.2008.03.013.
  34. Matti Järvisalo and Armin Biere. Reconstructing solutions after blocked clause elimination. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 340-345. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_30.
  35. Matti Järvisalo, Armin Biere, and Marijn Heule. Blocked clause elimination. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 129-144. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_10.
  36. Matti Järvisalo, Marijn J.H. Heule, and Armin Biere. Inprocessing rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 355-370. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  37. Oliver Kullmann. On a generalization of extended resolution. Discret. Appl. Math., 96-97:149-176, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00037-2.
  38. Ludovic Le Frioux, Souheib Baarir, Julien Sopena, and Fabrice Kordon. Painless: A framework for parallel SAT solving. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 233-250, Cham, 2017. Springer International Publishing. Google Scholar
  39. Jia Hui Liang. Machine Learning for SAT Solvers. PhD thesis, University of Waterloo, December 2018. Google Scholar
  40. Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, and Zhipeng Lü. An effective learnt clause minimization approach for CDCL SAT solvers. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 703-711. ijcai.org, 2017. URL: https://doi.org/10.24963/ijcai.2017/98.
  41. Norbert Manthey. The mergesat solver. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 387-398. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_27.
  42. Saeed Nejati, Zack Newsham, Joseph Scott, Jia Hui Liang, Catherine Gebotys, Pascal Poupart, and Vijay Ganesh. A propagation rate based splitting heuristic for divide-and-conquer solvers. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 251-260, Cham, 2017. Springer International Publishing. Google Scholar
  43. Alex Ozdemir, Haoze Wu, and Clark Barrett. SAT solving in the serverless cloud. In 2021 Formal Methods in Computer Aided Design (FMCAD), pages 241-245, 2021. URL: https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_33.
  44. 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. Google Scholar
  45. Tobias Schubert, Matthew Lewis, and Bernd Becker. Pamiraxt: Parallel SAT solving with threads and message passing. J. Satisf. Boolean Model. Comput., 6(4):203-222, 2009. URL: https://doi.org/10.3233/sat190068.
  46. Nathan Wetzler, Marijn J.H. Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  47. Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo Moura. A concurrent portfolio approach to SMT solving. In Proceedings of the 21st International Conference on Computer Aided Verification, CAV '09, pages 715-720, Berlin, Heidelberg, 2009. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-02658-4_60.
  48. Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res., 32:565-606, 2008. URL: http://dblp.uni-trier.de/db/journals/jair/jair32.html#XuHHL08.
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