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

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 as one instance finishes, the entire run stops. Several successful systems even use Plain Parallel Portfolio (PPP), where the individual solvers do not exchange any information. This paper contains a thorough experimental evaluation of PPP, which shows that PPP can improve wall-clock runtime. This improve-ment is due to the fact that memory access is still local and the memory system can hide the latency of memory access, respectively. In particular, there does not seem as much cache congestion as one might imagine. We further present some limits on the scalability of PPP and finally give one argument why PPP solvers are a good fit for todays multi-core architectures.