GPU Acceleration of BCP Procedure for SAT Algorithms

Hironori Fujii, Noriyuki Fujimoto
Graduate School of Science Osaka Prefecture University, 1-1 Gakuencho, Nakaku, Sakai, Osaka 599-8531, Japan
The 2012 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA’12), 2012


   title={GPU Acceleration of BCP Procedure for SAT Algorithms},

   author={Fujii, H. and Fujimoto, N.},



Download Download (PDF)   View View   Source Source   



The satisfiability problem (SAT) is widely applicable and one of the most basic NP-complete problems. This problem has been required to be solved as fast as possible because of its significance, but it takes exponential time in the worst case to solve. Therefore, we aim to save the computation time by parallel computing on a GPU. We propose parallelization of BCP (Boolean Constraint Propagation) procedure, one of the most effective techniques for SAT, on a GPU. For a 2.93GHz Intel Core i3 CPU and an NVIDIA GeForce GTX480, our experiment shows that the GPU accelerates our SAT solver based on our BCPembedded divide and conquer algorithm 6.7 times faster than the CPU counterpart.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: