Run-time performance optimization of an FPGA-based deduction engine for SAT solvers

FPGAs are a promising technology for accelerating SAT solvers. Besides their high density, fine granularity, and massive parallelism, FPGAs provide the opportunity for run-time customization of the hardware based on the given SAT instance. In this article, a parallel deduction engine is proposed for backtrack search algorithms. The performance of the deduction engine is critical to the overall performance of the algorithm because, for any moderate SAT instance, millions of implications are derived. We propose a novel approach in which p, the amount of parallelization of the engine, is fine-tuned during problem solving in order to optimize performance. Not only the hardware is initially customized based on the input instance, but it is also dynamically modified in terms of p based on the knowledge gained during solving the SAT instance. Compared with conventional deduction engines that correspond to p = 1, we demonstrate speedups in the range of 2.87 to 5.44 for several SAT instances.