Download PDFOpen PDF in browser

DPS: a Framework for Deterministic Parallel SAT Solvers

EasyChair Preprint 8553

15 pagesDate: August 2, 2022

Abstract

In 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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:8553,
  author    = {Hidetomo Nabeshima and Tsubasa Fukiage and Yuto Obitsu and Xiao-Nan Lu and Katsumi Inoue},
  title     = {DPS: a Framework for Deterministic Parallel SAT Solvers},
  howpublished = {EasyChair Preprint 8553},
  year      = {EasyChair, 2022}}
Download PDFOpen PDF in browser