An Efficient Hardware Implementation of a SAT Problem Solver on FPGA

A hardware analyzer for the Boolean satisfiability problem using a complete algorithm was developed for an Alter a DE2-70 Cyclone II FPGA board. In one clock cycle, all implications are computed, variables are assigned and all clauses are evaluated in parallel. Backtracking is done by means of a hardware stack occupying minimal memory resources. No memory is required to hold the potentially gigantic problem specification as a VHDL package is used by the HDL compiler to simplify the circuit (by propagating constants). Run-time comparisons were made using instances from the DIMACS suite with MiniSAT, one of the most efficient software solvers, revealing accelerations of up to 6.66, as well as with other state-of-the-art hardware SAT solvers where accelerations of 2 orders of magnitude were observed. Our approach demonstrates a high level of flexibility and scalability as the generated circuits have a very small FPGA footprint. The largest problem tested has 317 variables, 1264 clauses for a total of 3670 literals and occupies 20.47% of the FPGA used. Projections regarding circuit frequency and FPGA footprint for larger problems are also deduced to show the scalability of the approach.