An FPGA Solver for Very Large SAT Problems

WSAT and its variants are one of the best performing stochastic local search algorithms for the satisfiability (SAT) problem. In this paper, we propose an FPGA solver for very large SAT problems based on a WSAT algorithm. In our solver, parallel and multi-thread processing are combined (1) to fully utilize parallel accesses to external memory banks, and (2) to enhance the utilization of internal memory banks by fully utilizing their dual-port accesses, in order to solve very large problems on the pipelined circuit. Our solver on Xilinx XC2V6000 can solve problems up to K variables and K clauses, which is more than ten times larger than previous solvers on the same size FPGA.