Improving Search Space Splitting for Parallel SAT Solving

The last two decades progresses have led Propositional Satisfiability (SAT) to be a competitive practical approach to solve a wide range of industrial and academic problems. Thanks to these advances, the size and difficulty of the SAT instances have grown significantly. The demand for more computational power led to the creation of new computer architectures and paradigms composed by multiple machines connected by a network to act as one machine, like clusters and grids. However, extra computing power is not coming anymore from higher processor frequencies, but rather from a growing number of computing cores and processors. It becomes clear that exploiting this new architecture is essential for the evolution of SAT solvers. Search space splitting is probably the most commonly used strategy to explore the parallelism provided by the search space. However, it is not clear how to find the relevant set of variables to divide the search space. This paper extends a method based on the VSIDS heuristic to find the initial set of partition variables. A drawback of search space splitting is load balancing. To overcome this problem, we propose the use of a hybrid approach between search space splitting and portfolio. Preliminary results show that both these techniques improve the performance of the solver and reveal that combining search space splitting and portfolio approaches can lead to better results.