Parallelization of stochastic algorithm for boolean satisfiability on GPGPU architecture

摘要

Boolean satisfiability problem (SAT) is an NP-complete decision problem for determining whether there exists a variable assignment making a Boolean expression satisfiable (TRUE). SAT has been the cornerstone for various Computer Engineering applications. Numerous algorithms for solving SAT exist with varying degrees of completeness and complexity. A class of SAT algorithms based on stochastic local search (SLS) is generally easier to implement than backtracking search procedures. This paper discusses cwSAT, a parallel implementation of an SLS procedure, WalkSAT, on a GPGPU architecture. The performance of cwSAT is compared with that of WalkSAT using 200 benchmarks in Random class of SAT11 Competition. Experimental results showed that cwSAT can find satisfiable assignments for over 99% of the benchmarks while the average improvement of cwSAT is approximately 33% to 98% over WalkSAT.