3-SAT on CUDA: Towards a massively parallel SAT solver

Quirin Meyer, Fabian Schonfeld, Marc Stamminger, Rolf Wanka
Department of Computer Science, University of Erlangen-Nuremberg, Germany
International Conference on High Performance Computing and Simulation (HPCS), 2010


   title={3-SAT on CUDA: Towards a massively parallel SAT solver},

   author={Meyer, Q. and Scho?nfeld, F. and Stamminger, M. and Wanka, R.},

   booktitle={High Performance Computing and Simulation (HPCS), 2010 International Conference on},





Download Download (PDF)   View View   Source Source   



This work presents the design and implementation of a massively parallel 3-SAT solver, specifically targeting random problem instances. Our approach is deterministic and features very little communication overhead and basically no load-balancing cost at all. In the context of most current parallel SAT solvers running only on a handful of cores, we implemented our solver on Nvidia’s CUDA platform, utilizing more than 200 parallel streaming processors, and employing several millions of threads to work through single problem instances. As most common sequential solver techniques had to be discarded, our approach is additionally supported by a new set of global heuristics, designed specifically to be easily exploited by the underlying thread parallelism.
No votes yet.
Please wait...

Recent source codes

* * *

* * *

HGPU group © 2010-2023 hgpu.org

All rights belong to the respective authors

Contact us: