FPGA Accelerated SAT Solver
Pubblico DepositedContenuto scaricabile
open in viewerThe 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
- Subject
- Publisher
- Identifier
- 121748
- E-project-042524-141459
- Parola chiave
- Advisor
- Year
- 2024
- Date created
- 2024-04-25
- Resource type
- Major
- Source
- E-project-042524-141459
- Rights statement
Relazioni
- In Collection:
Articoli
Elementi
Thumbnail | Titolo | Visibilità | Embargo Release Date | Azioni |
---|---|---|---|---|
FPGA_SAT_Solver_MQP_Report.pdf | Pubblico | Scaricare |
Permanent link to this page: https://digital.wpi.edu/show/k35698655