Exploiting Unexploited Computing Resources for Computational Logics

Alessandro Dal Palu, Agostino Dovier, Andrea Formisano, Enrico Pontelli
Universita di Parma
9th Italian Convention on Computational Logic (CILC 2012), 2012


   title={Exploiting Unexploited Computing Resources for Computational Logics},

   author={Dal Palu, Alessandro and Dovier, Agostino and Formisano, Andrea and Pontelli, Enrico},



Download Download (PDF)   View View   Source Source   



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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2018 hgpu.org

All rights belong to the respective authors

Contact us: