Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. Intl. Workshop on Pragmatics of SAT (POS'13)
Original Kurzfassung:
Effectively parallelizing SAT solving is an open and important issue. The current stateof 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 improvement
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.