3-SAT on CUDA: Towards a Massively Parallel SAT Solver

Schönfeld F, Meyer Q, Stamminger M, Wanka R (2010)

Publication Type: Conference contribution

Publication year: 2010

Edited Volumes: Proceedings of the 2010 International Conference on High Performance Computing and Simulation, HPCS 2010

Conference Proceedings Title: Proc. High Performance Computing and Simulation Conference (HPSC)

Event location: Caen FR

DOI: 10.1109/HPCS.2010.5547116

Abstract

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. ©2010 IEEE.

Authors with CRIS profile

Quirin Meyer Chair of Visual Computing (LGDV) Marc Stamminger Chair of Visual Computing (LGDV) Rolf Wanka Professur für Informatik (Effiziente Algorithmen und Kombinatorische Optimierung)

How to cite

APA:

Schönfeld, F., Meyer, Q., Stamminger, M., & Wanka, R. (2010). 3-SAT on CUDA: Towards a Massively Parallel SAT Solver. In Proc. High Performance Computing and Simulation Conference (HPSC). Caen, FR.

MLA:

Schönfeld, Fabian, et al. "3-SAT on CUDA: Towards a Massively Parallel SAT Solver." Proceedings of the High Performance Computing and Simulation Conference (HPSC), Caen 2010.

BibTeX: Download