FPGA Accelerated SAT Solver

Gray, Andrew

Student Work

FPGA Accelerated SAT Solver

Public Deposited

This project is a part of a larger project with the goal of implementing algorithms to solve systems of binary quadratic equations using a recursive search on FPGAs. Our goal was to implement an exhaustive search method for a binary quadratic system of equations as a proof of concept, as well as expanding upon a modified GRASP (Generic Search Algorithm for the Satisfiability Problem) algorithm created in Python to improve the speed and reduce complexity of the decision making. Look up tables (LUTs) created by the group covered cases for two equations with one, two, or three differences between them. The tables and modules for the project are written in Verilog and SystemVerilog, with one additional module created in VHDL. Some work was also completed in Python. For future use, the exhaustive solver can easily be upgraded to scale the number of terms and solution size. The CDCL (Conflict Driven Clause Learning) is still a work in progress at the time of this paper. Although Boolean Satisfiability problem is a never-ending research problem, our group did make improvements in the solving that could be expanded upon by further research and improvements.

This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.

Creator