In recent years, Parallel SAT solvers have leveraged with the so called Parallel Portfolio architecture. In this setting, a collection of independent Conflict-Directed Clause Learning (CDCL) algorithms compete and cooperate through Clause Sharing. However, when the number of cores increases, systematic clause sharing between CDCLs can slow down the search performance. Previous work has shown how the efficiency of the approach can be improved through controlling dynamically the amount of information shared by the cores [Hamadi et al., IJCAI09], specifically the allowed length of the shared clauses. In the present paper, a new approach is used to control the cooperation topology (pairs of units able to exchange clauses). This approach, referred to as Bandit Ensemble for parallel SAT Solving (BESS), relies on a multi-armed bandit formalization of the cooperation choices. BESS is empirically validated on the recent 2012 SAT challenge benchmark.
