high performance computing on graphics processing units: hgpu.org

The Boolean satisfiability problem, abbreviated as SAT, is the backbone of many applications in VLSI design automation and verification. Over the years, many SAT solvers, both complete and incomplete, have been developed. Complete solvers are usually based on the DPLL (Davis–Putnam–Logemann–Loveland) algorithm, which is a backtracking algorithm. Industrial strength problems are very large and make DPLL based solvers impractical for some applications. In such cases, local search algorithms that try to find a solution within a stipulated time can be used. These algorithms look at SAT problem as an optimization problem. They start with an initial random solution and explore a certain search space by iteratively making local changes to the solution using a greedy, heuristic algorithm to find a global optimum. Over the past few years, heterogeneous devices such as Graphics Processing Units (GPU) and Field Programmable Gate Arrays (FPGA) have been used to accelerate the SAT problem and handle large SAT instances. There has been a growing interest in exploiting the parallel and pipeline processing power of FPGAs for various applications. New process technologies have allowed for more logic blocks, memory elements, and faster FPGAs, making it a perfect candidate for parallel computing. This thesis presents a local search algorithm Walksat, implemented on the Xilinx Alveo U250 Accelerator card. The entire solver has been developed using the OpenCL framework. On-chip memory available on the FPGA has been exploited to a great extent and the solver can handle SAT problems of up to 98,000 variables and 401,800 clauses. We have also analyzed the performance of our solver against the state of the art complete and incomplete solvers.