ManySAT: a Parallel SAT Solver

Abstract

In this paper, ManySAT a new portfolio-based parallel SAT solver is thoroughly described. The design of ManySAT benefits from the main weaknesses of modern SAT solvers: their sensitivity to parameter tuning and their lack of robustness. ManySAT uses a portfolio of complementary sequential algorithms obtained through careful variations of the standard DPLL algorithm. Additionally, each sequential algorithm shares clauses to improve the overall performance of the whole system. This contrasts with most of the parallel SAT solvers generally designed using the divide-and-conquer paradigm. Experiments on many industrial SAT instances, and the first rank obtained by ManySAT in the parallel track of the 2008 SAT-Race clearly show the potential of our design philosophy.