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

Beitrag bei einer Tagung


Details zur Publikation

Autor(en): Schönfeld F, Meyer Q, Stamminger M, Wanka R
Titel Sammelwerk: Proceedings of the 2010 International Conference on High Performance Computing and Simulation, HPCS 2010
Jahr der Veröffentlichung: 2010
Tagungsband: Proc. High Performance Computing and Simulation Conference (HPSC)


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.



FAU-Autoren / FAU-Herausgeber

Meyer, Quirin
Lehrstuhl für Informatik 9 (Graphische Datenverarbeitung)
Stamminger, Marc Prof. Dr.
Lehrstuhl für Informatik 9 (Graphische Datenverarbeitung)
Wanka, Rolf Prof. Dr.
Professur für Informatik (Effiziente Algorithmen und Kombinatorische Optimierung)


Zitierweisen

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: 

Zuletzt aktualisiert 2018-23-11 um 06:06