Student Work

FPGA Accelerated SAT Solver

Public Deposited

Downloadable Content

open in viewer

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. The goal of this part was to implement an exhaustive search method for a binary quadratic system of equations as a proof of concept, as well as creating a lookup table to store the solutions to two binary quadratic equations that were similar to each other besides two variables. For a lookup-table, recursion-based approach for equations that were similar to each other, a table was created through simulations created using the hardware description languages Verilog and SystemVerilog to find solutions for those similar equations that were differing in a combination of two variables, with different combinations of linear and quadratic terms accounted for. For the future verification of produced solutions via an improved recursive search, a low-resource utilization method of exhaustive searching has been developed and implemented on upgraded hardware that can be scaled up both in terms of linear terms present, as well as the number of equations, with a method of displaying via a terminal being developed in the future. All of the code from the Vivado project can be found in the Appendix.

  • 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
Publisher
Identifier
  • E-project-121323-122335
  • 115085
Keyword
Advisor
Year
  • 2023
Date created
  • 12/13/2023
Resource type
Major
Source
  • E-project-121323-122335
Rights statement
Last modified
  • 2024-02-08

Relations

In Collection:

Items

Items

Permanent link to this page: https://digital.wpi.edu/show/vt150p925