1 Search Results for "Kiesl, Benjamin"

Document
DOI: 10.4230/LIPIcs.SAT.2022.27
Migrating Solver State

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

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{biere_et_al:LIPIcs.SAT.2022.27,
  author =	{Biere, Armin and Chowdhury, Md Solimul and Heule, Marijn J. H. and Kiesl, Benjamin and Whalen, Michael W.},
  title =	{{Migrating Solver State}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{27:1--27:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.27},
  URN =		{urn:nbn:de:0030-drops-167015},
  doi =		{10.4230/LIPIcs.SAT.2022.27},
  annote =	{Keywords: SAT, SMT, Cloud Computing, Serverless Computing}
}
  • Refine by Author
  • 1 Biere, Armin
  • 1 Chowdhury, Md Solimul
  • 1 Heule, Marijn J. H.
  • 1 Kiesl, Benjamin
  • 1 Whalen, Michael W.

  • Refine by Classification
  • 1 Theory of computation

  • Refine by Keyword
  • 1 Cloud Computing
  • 1 SAT
  • 1 SMT
  • 1 Serverless Computing

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

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