An FPGA Solver for 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 large SAT problems based on a WSAT algorithm. In hardware solvers, it is very important to solve large problems efficiently. In previous hardware solvers, all clauses are evaluated in parallel using the evaluators of the same number as the clauses to achieve high performance. In our solver, (1) only the clauses whose values will be changed are evaluated in parallel to minimize the circuit size, and (2) four independent tries are executed at the same time on the pipelined circuit to achieve high performance. Our FPGA solver can solve much larger problems than previous works with less hardware resources, and shows higher performance. The solver on XC2V6000 can solve problems up to 2000 variables and 8500 clauses.