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.

Exploiting Unexploited Computing Resources for Computational Logics

FORMISANO, Andrea;
2012

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11391/919147
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? ND
social impact