DROPS

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.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}
}

Document

DOI: 10.4230/DagSemProc.10111.5

FITE - Future Integrated Testing Environment

Authors: Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser, and Michael W. Whalen

Published in: Dagstuhl Seminar Proceedings, Volume 10111, Practical Software Testing : Tool Automation and Human Factors (2010)

Abstract

It is a well known fact that the later software errors are discovered during the development process, the more costly they are to repair. Recently, automatic tools based on static and dynamic analysis have become widely used in industry to detect errors, such as null pointer dereferences, array indexing errors, assertion violations, etc. However, these techniques are typically applied late in the development cycle, and thus, the errors detected by such approaches are expensive to repair. Additionally, these techniques can suffer from scalability and presentation issues due to the fact that they are applied late in the development cycle. To address these issues we suggest that code should be continuously analyzed from an early stage of development, preferably as the code is written. This will allow developers to get instant feedback to repair errors as they are introduced, rather than later when it is more expensive. This analysis should also be incremental in nature to allow better scaling. Additionally, the presentation of errors in static and dynamic analysis tools can be improved due to the small increment of code being analyzed.

Cite as

Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser, and Michael W. Whalen. FITE - Future Integrated Testing Environment. In Practical Software Testing : Tool Automation and Human Factors. Dagstuhl Seminar Proceedings, Volume 10111, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{godefroid_et_al:DagSemProc.10111.5,
  author =	{Godefroid, Patrice and Mariani, Leonardo and Polini, Andrea and Tillmann, Nikolai and Visser, Willem and Whalen, Michael W.},
  title =	{{FITE - Future Integrated Testing Environment}},
  booktitle =	{Practical Software Testing : Tool Automation and Human Factors},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10111},
  editor =	{Mark Harman and Henry Muccini and Wolfram Schulte and Tao Xie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10111.5},
  URN =		{urn:nbn:de:0030-drops-26191},
  doi =		{10.4230/DagSemProc.10111.5},
  annote =	{Keywords: Incremental analysis, incremental testing, human factors, static analysis, model checking}
}

Search Results

Documents authored by Whalen, Michael W.

Migrating Solver State

Abstract

Cite as

FITE - Future Integrated Testing Environment

Abstract

Cite as

Thanks for your feedback!

Could not send message