Implementation of Parallel Boolean Satisfiability Solver by CUDA (Compute Unified Device Architecture)
Date Issued
2011
Date
2011
Author(s)
Lin, Kung-Ming
Abstract
Boolean satisfiability (SAT) problem plays a critical role in theoretical and industrial applications. With the advance of SAT solvers in the past 15 years, we are capable to solve fairly large-scale problems. To improve the performance of SAT solvers for much larger and harder SAT problems, parallelization of SAT solvers is gaining much attention in recent years. The state-of-the-art 4-to-8 threaded parallel SAT solvers are more powerful than single-threaded ones in recent international SAT solver competitions.
General-Purpose computation on Graphics Processing Units (GPGPU) is also emerging from massive parallel computing realm. To explore the concept of massive parallel SAT solvers, we have implemented the “CUDASAT”, a parallel CDCL-DPLL (Conflict Driven Clause Learning - Davis-Putnam-Logemann-Loveland) SAT solver with clause sharing on CUDA (Compute Unified Device Architecture) platform.
To the best of our knowledge, CUDASAT is the first of its kind. The experimental results demonstrated a downward trend in average searching events per solver while increasing the number of parallel solver. While the performance is not comparable to those state-of-the-art parallel SAT solvers, CUDASAT serves as a prototype of massive parallelization toward an affordable and alternative solution for SAT solving.
Subjects
Boolean satisfiability problem
satisfiability solver
parallel computing
SAT
CDCL
DPLL
GPGPU
CUDA
SDGs
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-100-R98943080-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):418e7d43825882de47a37e5229cc7577