Download PDFOpen PDF in browserDPS: a Framework for Deterministic Parallel SAT SolversEasyChair Preprint 855315 pages•Date: August 2, 2022AbstractIn this study, we propose a new framework for easily constructing efficient deterministic parallel SAT solvers, providing the delayed clause exchange technique introduced in ManyGlucose. This framework allows existing sequential SAT solvers to be parallelized with just as little effort as in the non-deterministic parallel solver framework such as PaInleSS. We show experimentally that parallel solvers built using this framework have performance comparable to state-of-the-art non-deterministic parallel SAT solvers while ensuring reproducible behavior. Keyphrases: Clause exchange, Portfolio parallel SAT solver, Reproducible parallel SAT solving
|