Reducing Compilation Time of Zhong's FPGA-based SAT Solver
Pak K. Chan, M. J. Boyd, S. Goren, K. Klenk, V. Kodavati,
R. Kundu, M. Margolese, J. Sun, K. Suzuki, E. Thorne, X. Wang, J. Xu,
M. Zhu
Department of Computer Engineering
University of California, Santa Cruz
Santa Cruz, California 95064 USA
Abstract
We present schemes to reduce the compilation time
of configurable hardware that solves Boolean Satisfiability. The SAT
solver presented by Zhong in last year's FCCM conference has a large
compilation time overhead mainly due to placement and routing of many
FPGAs. We attack the problem on 3 fronts. First, we partition the
SAT solver into instance-specific and non-specific components.
Secondly, we transform SAT instances to a canonical form. Finally,
we present a board-level architecture to solve large SAT instances.
All these efforts amount to a reduction in placement and routing time
to configure the reconfigurable hardware. We are able to reduce the
compilation time to mere routing time of the implication circuits for
each instance of the SAT problem, given the best scenario.