CUD@SAT: SAT Solving on GPUs

Alessandro Dal Pal’u, Agostino Dovier, Andrea Formisano, Enrico Pontelli
Dip. di Matematica e Informatica, Universita degli Studi di Udine, Via delle Scienze 206, 33100 Udine,Italy
Universita degli Studi di Udine, 2014


   title={CUD@SAT: SAT Solving on GPUs},

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



Download Download (PDF)   View View   Source Source   Source codes Source codes




The parallel computing power offered by Graphical Processing Units (GPUs) has been recently exploited to support general purpose applications-by exploiting the availability of general API and the SIMT-style parallelism present in several classes of problems (e.g., numerical simulations, matrix manipulations) – where relatively simple computations need to be applied to all items in large sets of data. This paper investigates the use of GPUs in parallelizing a class of search problems, where the combinatorial nature leads to large parallel tasks and relatively less natural symmetries. Specifically, the investigation focuses on the well-known Satisfiability Testing (SAT) problem and on the use of the NVIDIA CUDA architecture, one of the most popular platforms for GPU computing. The paper explores ways to identify strong sources of GPU-style parallelism from SAT solving. The paper describes experiments with different design choices and evaluates the results. The outcomes demonstrate the potential for this approach, leading to one order of magnitude of speedup using a simple NVIDIA platform.
No votes yet.
Please wait...

Recent source codes

* * *

* * *

HGPU group © 2010-2024 hgpu.org

All rights belong to the respective authors

Contact us: