Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design

The Boolean Satisfiability (SAT) problem is the key problem in computer theory and application. Field-programmable gate array (FPGA) has been addressed frequently to accelerate the SAT solving process in the last few years owing to its parallelism and flexibility. We have proposed a novel SAT solver based on an improved local search algorithm on the reconfigurable hardware platform. The new software preprocessing procedure and hardware architecture are involved to solve large-scale SAT problems instances. As compared with the past solvers, the proposed solver has the following advantages: the preprocessing technology can strongly improve the efficiency of solver; the strategy of strengthening the variable selection can avoid the same variable flipped continuously and repeatedly. It reduces the possibility of search falling into local minima. The experimental results indicate that the solver can solve problems of up to 32K variables/128K clauses without off-chip memory banks, and has better performance than previous works.