Cache Performance Study of Portfolio-Based Parallel CDCL SAT Solvers
This addresses performance bottlenecks in parallel SAT solvers, which are critical for research and industry applications, but is incremental as it builds on existing solver designs.
The study identified cache contention as a key factor limiting the scalability of parallel SAT solvers, and found that physically sharing the clause database between threads can improve performance for certain search types.
Parallel SAT solvers are becoming mainstream. Their performance has made them win the past two SAT competitions consecutively and are in the limelight of research and industry. The problem is that it is not known exactly what is needed to make them perform even better; that is, how to make them solve more problems in less time. Also, it is also not know how well they scale in massive multi-core environments which, predictably, is the scenario of comming new hardware. In this paper we show that cache contention is a main culprit of a slowing down in scalability, and provide empirical results that for some type of searches, physically sharing the clause Database between threads is beneficial.