7746

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
BibTeX

Download Download (PDF)   View View   Source Source   

1866

views

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...

Recent source codes

* * *

* * *

HGPU group © 2010-2025 hgpu.org

All rights belong to the respective authors

Contact us:

contact@hpgu.org