Lazy clause exchange policy for parallel SAT solvers

Abstract

Managing learnt clauses among a parallel, memory shared, SAT solver is a crucial but difficult task. Based on some statistical experiments made on learnt clauses, we propose a simple parallel version of Glucose that uses a lazy policy to exchange clauses between cores. This policy does not send a clause when it is learnt, but later, when it has a chance to be useful locally. We also propose a strategy for clauses importation that put them in "probation" before a potential entry in the search, thus limiting the negative impact of high importation rates, both in terms of noise and decreasing propagation speed. © 2014 Springer International Publishing Switzerland.