Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures

Abstract

Effectively parallelizing SAT solving is an open and important issue. The current state-of-the-art is based on parallel portfolios. This technique relies on running multiple solvers on the same instance in parallel. As soon one instance finishes the entire run stops. Several succesful systems even use plain parallel portfolio (PPP), where the individual solvers do not exchange any information. This paper contains a thorough experimental evaluation which shows that PPP can improve wall-clock running time because memory access is still local, respectively the memory system can hide the latency of memory access. In particular, there does not seem as much cache congestion as one might imagine. We also present some limits on the scalibility of PPP. Thus this paper gives one argument why PPP solvers are a good fit for todays multi-core architectures.