Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
A Practical Reconfigurable Hardware Accelerator for Boolean Satisfiability Solvers

John D. Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang

Abstract

We present a practical FPGA-based accelerator for solving Boolean Satisfiability problems (SAT). Unlike previous efforts for hardware accelerated SAT solving, our design focuses on accelerating the most time consuming part of the SAT solver ─ Boolean Constraint Propagation (BCP), leaving the choices of heuristics such as branching order, restarting policy, and learning and backtracking to software. Our novel approach uses an application-specific architecture instead of an instance-specific one to avoid time-consuming FPGA synthesis for each SAT instance. By avoiding global signal wires and carefully pipelining the design, our BCP accelerator is able to achieve much higher clock frequency than that of previous work. In addition, it can load SAT instances in milliseconds, can handle SAT instances with tens of thousands of variables and clauses using a single FPGA, and can easily scale to handle more clauses by using multiple FPGAs. Our evaluation on a cycle-accurate simulator shows that the FPGA co-processor can achieve 3.7-38.6x speedup on BCP compared to state-of-the-art software SAT solvers.

Details

Publication typeInproceedings
Published in45th Design Automation Conference (DAC)
PublisherAssociation for Computing Machinery, Inc.
> Publications > A Practical Reconfigurable Hardware Accelerator for Boolean Satisfiability Solvers