Parallel hybrid SAT solving using OpenCL

Sander Beckers, Gorik De Samblanx, Floris De Smedt, Toon Goedeme, Lars Struyf, Joost Vennekens
EAVISE, Lessius – Campus De Nayer, Sint-Katelijne-Waver, Belgium
BNAIC, 2012


   title={Parallel hybrid SAT solving using OpenCL},

   author={Beckers, Sander and De Samblanx, Gorik and De Smedt, Floris and Goedeme, Toon and Struyf, Lars and Vennekens, Joost},



Download Download (PDF)   View View   Source Source   



In the last few decades there have been substantial improvements in approaches for solving the Boolean satisfiability problem. Many of these consisted in elaborating on existing algorithms, both on the side of complete solvers as in the area of incomplete solvers. Besides the improvements to existing solving methods, however, recent evolutions in SAT solving take the form of combining several solvers into one, resulting in parallel solvers and so-called hybrid solvers. Our goal is to combine both approaches, by presenting a parallel hybrid solver. The parallelism exists on two levels: we run a complete solver on the CPU concurrently with an incomplete solver on the GPU, where the latter in turn consists of a massively parallel local search algorithm. We implemented our approach using the OpenCL framework, and present preliminary experimental results.
No votes yet.
Please wait...

Recent source codes

* * *

* * *

HGPU group © 2010-2024 hgpu.org

All rights belong to the respective authors

Contact us: