DPS: a Framework for Deterministic Parallel SAT Solvers

EasyChair Preprint no. 8553

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

@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 no. 8553},

  year = {EasyChair, 2022}}