Run-time performance optimization of an FPGA-based deduction engine for SAT solvers
Run-time performance optimization of an FPGA-based deduction engine for SAT solvers
复制标题
用于 SAT 求解器的基于 FPGA 推导引擎的运行时性能优化
DOI：
10.1145/605440.605444
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Bharani Thiruvengadam
中科院分区：
文献类型：
--
作者：
Andreas Dandalis;V. Prasanna;Bharani Thiruvengadam
FPGA是一种很有前途的加速SAT求解器的技术。除了它们的高密度、细粒度和大规模并行性之外，FPGA还提供了基于给定SAT实例的硬件运行时定制的机会。本文提出了一种用于回溯搜索算法的并行推理引擎。演绎引擎的性能对算法的整体性能至关重要，因为对于任何中等SAT实例，都会导出数百万个含义。我们提出了一种新的方法，其中p，引擎的并行化量，在解决问题的过程中进行微调，以优化性能。不仅硬件最初是基于输入实例定制的，而且它还基于在求解SAT实例期间获得的知识在p方面动态修改。与对应于p = 1的传统演绎引擎相比，我们展示了几个SAT实例在2.87到5.44的范围内的加速比。
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.