Download PDFOpen PDF in browser

Tuning Parallel SAT Solvers

EasyChair Preprint no. 195

17 pagesDate: May 31, 2018

Abstract

In this paper we present new implementation details and benchmarking results for our parallel portfolio solver \topo. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that 1,000 solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart- , branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.

As computing times on massively-parallel clusters are expensive, we consider it especially interesting to share these kind of experimental results.

Keyphrases: parallel processing, portfolio solver, SAT

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:195,
  author = {Thorsten Ehlers and Dirk Nowotka},
  title = {Tuning Parallel SAT Solvers},
  howpublished = {EasyChair Preprint no. 195},
  doi = {10.29007/w15s},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser