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

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 Satisability Problem (SAT) is one of the earliest NP-complete problems. The solution to SAT has various application areas, including automated theorem proving, circuit design, artificial intelligence, and software verification. Although many algorithms exist to experimentally solve SAT, they are not believed to be efficient 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 final result in our system.