Exploring Limits of Parallelism in FPGA-based Boolean Satisfiability

A two-part SAT solver using a complete algorithm was developed and used to characterize the impact of eliminating memory bottleneck from SAT solving. The first is a VHDL model that describes the hardware needed to implement the solver whereas the second is a software simulator counterpart. Comparisons between the two versions of the solver revealed accelerations of 3 orders of magnitude of the hardware version over the software version. Comparisons were also made with other state-of-the-art hardware SAT solvers where accelerations were observed. Tests were also performed with the MiniSAT software solver which revealed more than acceptable run-times. Circuit frequency projections were also used to approximate problem execution times.