high performance computing on graphics processing units: hgpu.org

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.