A parallel approach to solving satisfiability problems on graphics processing units using neural networks

Abstract

Graphics Processing Units (GPUs) have become popular for parallelization of general purpose applications recently. GPUs are composed of huge number of powerful processors in a readily available package. The Satis ability Problem (SAT) is one of the earliest NP-complete problems. The solution to SAT has various application areas, including automated theorem proving, circuit design, arti cial intelligence, and software veri cation. Although many algorithms exist to experimentally solve SAT, they are not believed to be e cient on all SAT instances. In this thesis, we propose a novel GPU based parallel approach using neural networks as the algorithm selection mechanism to solve the SAT.We demonstrate speedups of up to 3 times on benchmarks by choosing the correct algorithms (solvers) to solve sub problems to reach the nal result in our system.