Accelerating Boolean Satisfiability on an FPGA.

In this chapter, we propose an FPGA-based SAT approach in which the traversal of the implication graph as well as conflict clause generation is performed in hardware, in parallel. In our approach, clause literals are stored in the FPGA slices. In order to solve large SAT instances, we heuristically partition the clauses into a number of `bins,΄ each of which can fit in the FPGA. This is done in a preprocessing step. [ABSTRACT FROM AUTHOR]