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 improvements consisted in elaborating on existing algorithms. On the side of the complete solvers this led to more efficient branching heuristics and the use of watched literals for unit propagation; incomplete solvers on the other hand have benefited from using random walks and from integrating evolutionary algorithms into the search process. Another line of research has combined these developments by creating hybrid solvers. More recently, the rapid development of parallel architectures has led to improvements in the implementation of algorithms as well, both on the side of complete as on the side of incomplete solvers. Up until now this work has been limited mostly to grids or multicore CPU’s. Recent advances such as the OpenCL framework however, make it possible to also exploit the processing power of today’s GPU’s, and do so together with the CPU. Our goal is to take advantage of this, by implementing a parallel version of a hybrid algorithm that has been proven remarkably succesful in the class of locally inconsistent SAT problems. By parallelizing local search, our solver will be competitive on consistent problems as well. The workload of the hybrid algorithm will be split between the GPU and CPU, the former performing a massively parallel local search and the latter an adapted version of MiniSAT, a popular complete solver. We present here the results for a first simplified implementation, and for simulations of the final solver.