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 …