Efficient Implementation of Parallel SAT Solver Based Stochastic Local Search


Sa’ed Abed
Computer Engineering Department, College of Engineering and Petroleum, Kuwait University, Kuwait

Salam I. Nachawi
Mohammad Al-Shayeji

Series: Computer Science, Technology and Applications
BISAC: COM014000

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.
(Imprint: Novinka)



Table of Contents

List of Figures

List of Tables

List of Algorithms


Chapter 1. Introduction

Chapter 2. Related Work

Chapter 3. Approach and Methodology

Chapter 4. Experimental Results

Chapter 5. Conclusions and Recommendations for Future Work



Senior and graduate (Master and Ph. D.) Students.
Research groups in the Verification and Formal methods area.


SAT solvers, SLS, Parallel SAT, Parallel SLS, CPU time

Additional information