Sat Solving Using FPGA-Based Heterogeneous Computing

We present a heterogeneous computing solution to the Boolean satisfiability (SAT) problem. Our field-programmable gate array (FPGA)-based implementation for accelerating the common case computation within a SAT solver utilizes most of the FPGA resources and it seamlessly integrates with our software host. Algorithms and data structures were redesigned to maximize the strengths of customized computing and generalizable optimizations are proposed to maximize throughput, minimize communication latencies, and compact hardware memory. We are significantly faster than state-of-the-art SAT solvers in software and hardware.