An FPGA solver for WSAT algorithms

WSAT and its variants are one of the best performing stochastic local search algorithms for the satisfiability (SAT) problem. In this paper, we propose a new FPGA solver for WSAT algorithms. The features of our solver are (1) high parallelism by small size units to evaluate clauses in each instance of the SAT problem, (2) multi-thread execution to achieve high performance, and (3) fast data-downloading for each instance. We implemented the solver for problems up to 256 variables and 1024 clauses on XC2V6000, and it used 45% of slices and live block RAMs. Our implementation shows higher performance over previous SAT solvers on FPGAs.