Distributed SAT solving engine

Abstract

The boolean satisfiability problem (SAT) is one of the typical NP-complete problems that have found considerable industrial applications in the past decades. Significant theoretical and practical efforts has been devoted to the research in this particular problem. Recently, with the major architectural shift from increasing processor power to increasing number of processors, and the development of cloud computing, there is an emerging need to paral- lelize these solvers to run on a loose distributed system where minimal synchronization and communication overhead is desirable. It is an important challenge to improve performance when the number of processors increase. Moreover, the parallel solver should be able to scale accordingly when the number of processors is significant. In this report, we first present multiple aspects of the algorithm implemented in modern state-of-the-art solvers and advances in parallel SAT solving. Based on the analysis of cur- rent research, we then propose optimizations on splitting strategies aimed for the distributed environment. A protocol of sharing relevant information between processes was also designed and implemented using the hybrid of Message Passing Interface (MPI) and POSIX threads. Moreover, two different approaches on load balancing on long-running jobs are proposed and implemented. Experimental data show that we can achieve good speedup and scalabil- ity by combining the new communication protocol combined with improved strategies and heuristics.