FPGA-based SAT solver architecture with near-zero synthesis and layout overhead

Boolean satisfiability (SAT) has shown itself to be a promising application for configurable computing and an interesting testbed for new configurable computing compilation techniques. In this work we have developed a new and novel SAT solver architecture that addresses three fundamental hurdles that remain before reconfigurable-hardware-based acceleration of SAT can be widely used. These hurdles are: first, the time overhead for compiling the instance-specific circuit to hardware; secondly, the limited sophistication of the hardware algorithm; and thirdly, the slow clock speeds. The main enabling idea in our work is to implement the communication between literals and clauses by means of a time multiplexed pipelined bus architecture rater than hardwiring it using on-FPGA routing resources. This allows the circuits for different instances of the SAT problem to be identical except for small local differences. Thus, the incremental synthesis and place-and-route effort required for each instance of the problem becomes negligible compared to the time to actually solve the SAT problem. Interestingly, the time multiplexing feature also allows us to incorporate the dynamic addition of clauses into the SAT solver algorithm, since the compilation/configuration time is negligible. Finally, since the proposed architecture is highly pipelined, with very few long wires, and no wires crossing FPGA boundaries, high clock speeds are possible. The authors present the overall architecture and detailed circuits for it in the paper. They also present experimental results showing the performance of the architecture relative to earlier efforts on hardware acceleration of SAT and relative to software implementation.