Community Branching for Parallel Portfolio SAT Solvers

ABSTRACT. Portfolio approach for parallel SAT solvers is known as the standard parallelization technique. In portfolio, diversification is one of the important factors in order to enable workers (solvers) to conduct a vast search. The diversification is implemented by setting different parameters for each worker in the state-of-the-art parallel portfolio SAT solvers. However, existing diversification can be insufficient because the combination of the parameters is limited, in which two or more workers can search same spaces. For this issue, we propose a novel diversification technique, called community branching. In this method, we assign a different set (or sets) of variables (called a community) to each worker and force them to select these variables as decision variables in early decision levels. In this manner, we can avoid overlaps of search spaces between the workers more intentionally than the existing method. We create a graph, where a vertex is corresponds to a variable and an edge stands for relations in a same clause, and we apply a modularity-based community detection algorithm to it. The variables in a community have strong relationships, and a distributed search for different communities can benefit the whole search. Experimental results shot that we could speedup the existing parallel SAT solvers with our proposal.