Efficient Implementation of Parallel SAT Solver Based Stochastic Local Search

Over the years, the Boolean Satisfiability problem (SAT) has gained increased interest, which can be attributed to the huge range of applications where it can be used. SAT solvers are entities that try to find a solution for SAT problems in a time efficient manner. The main types of SAT solvers are: Davis-Putnam-Logemann-Loveland procedure (DPLL) based solvers, Stochastic Local Search (SLS) solvers, and Parallel SAT solvers. In this book, we propose a new solver that combines the use of all three types together. Firstly, a DPLL solver will be run sequentially to select the splitting variables. Then, the search space will be divided and given to multiple SLS solvers that will work in parallel to find a solution for the SAT problem in question. The SLS solver used in this work will be probSAT. In our investigation, we have chosen to split the search space into two parts. Each part will run three instances of probSAT solver in parallel. As our solver combines DPLL and SLS SAT solving, and competitive and cooperative parallel approaches, we have called it MixedSAT. The results obtained from our proposed approach show higher speed in 29% of the simulated instances in comparison to pprobSAT solver. This time enhancement is very important in many applications since it shortens the CPU time and saves expenses.