Cache Performance Study of Portfolio-Based Parallel CDCL SAT Solvers

TL;DR

This paper investigates cache contention in parallel CDCL SAT solvers, revealing its impact on scalability and demonstrating that sharing clause databases can improve performance in certain search scenarios.

Contribution

It identifies cache contention as a key factor limiting scalability and empirically shows benefits of shared clause databases in parallel SAT solving.

Findings

Cache contention significantly affects parallel solver scalability.

Sharing clause databases can improve performance for some search types.

Empirical results highlight the importance of cache management in parallel SAT solvers.

Abstract

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.