Parallelization of SAT Algorithms on GPUs

Carlos Costa
Instituto Superior Tecnico
Technical report, INESC-ID / Instituto Superior Tecnico, Technical University of Lsibon (UTL), 2013

   title={Parallelization of SAT Algorithms on GPUs},

   author={Costa, Carlos},



Download Download (PDF)   View View   Source Source   



The Boolean Satisfability Problem is one of the most important problems in computer science with applications spanning many areas of research. Despite this importance and the extensive study and improvements that have been made, no efficient solution to the problem has been found to the date. During the last years, nVidia introduced CUDA, a platform which lets developers take advantage of the great computing power of the GPUs, that was once unavailable to use. In this work, we propose a methodology of using GPUs to accelerate the resolution of the SAT problem. Since the problem does not map well the GPU paradigm, we will explain our approach, which uses both the GPU and the CPU to solve the parts that suit them the best. We also propose developing a novel SAT solver, capable of solving current benchmark problems, as well as most industry problems.
VN:F [1.9.22_1171]
Rating: 0.0/5 (0 votes cast)

* * *

* * *

Follow us on Twitter

HGPU group

1666 peoples are following HGPU @twitter

Like us on Facebook

HGPU group

339 people like HGPU on Facebook

* * *

Free GPU computing nodes at hgpu.org

Registered users can now run their OpenCL application at hgpu.org. We provide 1 minute of computer time per each run on two nodes with two AMD and one nVidia graphics processing units, correspondingly. There are no restrictions on the number of starts.

The platforms are

Node 1
  • GPU device 0: nVidia GeForce GTX 560 Ti 2GB, 822MHz
  • GPU device 1: AMD/ATI Radeon HD 6970 2GB, 880MHz
  • CPU: AMD Phenom II X6 @ 2.8GHz 1055T
  • RAM: 12GB
  • OS: OpenSUSE 13.1
  • SDK: nVidia CUDA Toolkit 6.5.14, AMD APP SDK 3.0
Node 2
  • GPU device 0: AMD/ATI Radeon HD 7970 3GB, 1000MHz
  • GPU device 1: AMD/ATI Radeon HD 5870 2GB, 850MHz
  • CPU: Intel Core i7-2600 @ 3.4GHz
  • RAM: 16GB
  • OS: OpenSUSE 12.3
  • SDK: AMD APP SDK 3.0

Completed OpenCL project should be uploaded via User dashboard (see instructions and example there), compilation and execution terminal output logs will be provided to the user.

The information send to hgpu.org will be treated according to our Privacy Policy

HGPU group © 2010-2015 hgpu.org

All rights belong to the respective authors

Contact us: