ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 12:00 - 12:30 at SUN I - SAT and SMT II Chair(s): Armin Biere

Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are two main approaches. First, portfolio launches multiple solvers in parallel, and the first to find a solution ends the computation. The second one, divide-and-conquer (D&C) splits the search space, each solver being in charge of a particular subspace. However although D&C based approaches seem to be the natural way to work in parallel, portfolio ones experimentally provide better performances. An explanation resides on the difficulties to use the CNF problem to compute an a priori good search space partitioning (i.e., all parallel solver will process their subspaces in a similar time). To avoid this, dynamic load balancing of the space search is implemented. Unfortunately, this is difficult to compare load balancing strategies since state-of-the-art SAT solvers appropriately dealing with these aspects are hardly adaptable to various strategies than the ones they have been designed for. This paper aims at providing a way to overcome this problem by proposing an implementation and evaluation of different types of divide-and-conquer inspired from the literature. These are relying on the Painless framework, which provide concurrent facilities to elaborate such parallel SAT solvers. Comparison of the various strategies are then discussed.