Community Branching for Parallel Portfolio SAT Solvers

摘要

Portfolio approach for parallel SAT solvers is known as the standard parallelisation 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, it is difficult to combine the search parameters properly in order to avoid overlaps of search spaces between the workers 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 the overlaps of the search spaces between the workers more vigorously than the existing method. We create a graph, where a vertex corresponds to a variable and an edge stands for a relation between two variables 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 show that we could speedup an existing parallel SAT solver with our proposal.