Tuning Parallel SAT Solvers

Authors: Thorsten Ehlers and Dirk Nowotka

Paper Information

Title:Tuning Parallel SAT Solvers
Authors:Thorsten Ehlers and Dirk Nowotka
Proceedings:POS FLoC USB Stick
Editors: Daniel Le Berre and Matti Järvisalo
Keywords:SAT, Portfolio Solver, Parallel Processing

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.

Talk:Jul 07 09:00 (Session 23L: Tuning solvers and applications)