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

Clear

$82.00

Volume 10

Issue 1

Volume 2

Volume 3

Special issue: Resilience in breaking the cycle of children’s environmental health disparities
Edited by I Leslie Rubin, Robert J Geller, Abby Mutic, Benjamin A Gitterman, Nathan Mutic, Wayne Garfinkel, Claire D Coles, Kurt Martinuzzi, and Joav Merrick

eBook

Digitally watermarked, DRM-free.
Immediate eBook download after purchase.

Product price
Additional options total:
Order total:

Quantity:

Details

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)

List of Figures

List of Tables

List of Algorithms

Acknowledgments

Chapter 1. Introduction

Chapter 2. Related Work

Chapter 3. Approach and Methodology

Chapter 4. Experimental Results

Chapter 5. Conclusions and Recommendations for Future Work

References

You have not viewed any product yet.