An Efficient SAT Solving Algorithm Using Pseudo-Conflict Learning and Heterogeneous Computing

The Propositional Satisfiability Problem (SAT) is one of the most fundamental NP-complete problems. In this paper, a high-performance and heterogeneous SAT solving algorithm is presented. This algorithm, called CUDA-WSat-PcL, uses Pseudo-conflict Learning with a WalkSAT algorithm and exploits a massively parallel architecture on a Graphics Processing Unit (GPU) together with a conventional CPU on NVIDIA's Compute Unified Device Architecture (CUDA) platform. Our experimental results reveal that the heterogeneous and parallelized implementation finds the results up to 25 times faster than our sequential implementation. Additionally, our profiling results show that the improvements depend solely on instance size.