Migrating Solver State
Migrating Solver State
复制标题
DOI：
10.4230/lipics.sat.2022.27
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Armin Biere;M. S. Chowdhury;Marijn J. H. Heule;B. Kiesl;M. Whalen
中科院分区：
文献类型：
--
作者：
Armin Biere;M. S. Chowdhury;Marijn J. H. Heule;B. Kiesl;M. Whalen
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.
