A Dynamic Moldable Job Scheduling Based Parallel SAT Solver

In a shared cluster facility scheduling of parallel jobs is an important factor that can affect the performance and turnaround time of the submitted jobs. To solve hard tree search problems, we have designed the Dynamic Moldable Tree Search (DMTS) framework. The DMTS framework allows existing serial tree search applications to run in parallel with very little development effort. The DMTS framework is designed to run on parallel computing infrastructures, including clusters, computational grids, and clouds. Target applications for the DMTS framework are hard tree search problems such as Boolean satisfiability (SAT) problems. SAT is amongst the most important problems in theoretical computer science. In this paper we present a parallel Dynamic Moldable SAT (DMSAT) solver. DMSAT runs on top of the DMTS framework. DMSAT is a parallel version of miniSat; miniSat is one of the most widely used open source SAT solvers. We compare the performance of DMSAT with PMSAT and miniSat. Our experimental results show that the dynamic moldable model of DMSAT perform much better than the other SAT solvers. In SAT race competitions all those problems that are not solved by a SAT solver within 1200 seconds are marked as unsolvable. DMSAT is also able to solve hard SAT problems that were not solvable by miniSat in the past SAT races.