Communication in Massively-Parallel SAT Solving
Thorsten Ehlers, Dirk Nowotka, Philipp Sieweck · 2014
The exchange of learnt clauses is a key feature in parallel SAT solving. We present an approach based on a communication graph. Each solver thread corresponds to a node in this graph. Communication between two solvers is allowed if the respective nodes are connected by an edge. This yields another dimension in controlling the amount of communication. We show results for this approach, gaining significant speedups for up to 256 parallel solvers.