Massively Parallel Local Search for SAT

Parallel portfolio-based algorithms have become a standard methodology for both complete and incomplete solvers for SAT solving. In this methodology several algorithms explore the search space in parallel, either independently or cooperatively with some communication between the solvers. Unlike previous work where parallel algorithms are limited to few cores (usually up to 16 cores), this work studies the performance of parallel local search for SAT with a large degree of parallelism, up to 256 cores, and compares various cooperation strategies. The strategy with the best performance consists in considering small groups of solvers (e.g. 4 or 8) sharing information and performing no inter-group communication.