| Summary: | 碩士 === 國立臺灣大學 === 電子工程學研究所 === 99 === 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.
|
|---|
