Exploiting Unexploited Computing Resources for Computational Logics

We present an investigation of the use of GPGPU techniques to par- allelize 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, includ- ing the use of a predominantly data-parallel architecture, like NVIDIA’s CUDA platform, for the execution of relatively “heavy” threads, associated to tradition- ally sequential computations (e.g., unit propagation), non-deterministic computa- tions (e.g., variable splitting), and meta-heuristics to guide search. Experimenta- tion 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.