The goal of this project was to solve the Boolean Satisfiability Problem (SAT) by implementing an exhaustive search method for a binary quadratic system of equations on FPGA hardware. We first used Python to construct a proof-of-concept CDCL solver for quadratic Boolean systems, which we named the Frankenstein algorithm. Additionally, we drafted look up tables (LUTs) that analyzed two equations and defined variables based on one, two, or three term differences between the pair of equations. These LUTs were created because for these equations, the terms that differ have a limited number of solutions, so some variables can be defined early. We also created an algorithm that determines the decision order for variables based on their frequency and the current state of the solver. After that, the team worked on converting the Python code to Verilog. Our group successfully implemented the LUTs and some of Frankenstein in Verilog and System Verilog, with one additional module created in VHDL. Although SAT is a continuous research problem, our group created a solid foundation that leaves plenty of room for future groups to expand on.

• 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

• Mao, Xinyun
• David, Samuel
• Eben, Joshua
• Hunter, Patrick

Subject

• Security
• Computing

Publisher

• Worcester Polytechnic Institute

Identifier

• 121748
• E-project-042524-141459

Keyword

• Boolean SAT
• FPGA
• MQP
• Look Up Table
• CDCL

Advisor

• Doroz, Yarkin
• Mus, Koksal

Year

• 2024

Date created

• 2024-04-25

Resource type

• Major Qualifying Project

Major

• Electrical & Computer Engineering
• Computer Science

Source

• E-project-042524-141459

Rights statement

• In Copyright