Exploiting unexploited computing resources for computational logics


We present an investigation of the use of GPGPU techniques to parallelize the execution of a satisfiability solver, based on the traditional DPLL procedure-which, in spite of its simplicity, still represents the core of the most competitive solvers. The investigation tackles some interesting problems, including the use of a predominantly data-parallel architecture like NVIDIA’s CUDA platform for the execution of relatively ‘heavy’ Threads associated to traditionally sequential computations (e.g. unit propagation), non-deterministic computations (e.g. variable splitting) and meta-heuristics to guide search. Experimentation confirms the potential for significant speedups from the use of GPGPUs even with relatively simple modifications to the structure of the DPLL procedures-which should facilitate the porting of such ideas to other DPLL-based solvers.

CEUR Workshop Proceedings