Solving Satisfiability Problems on FPGAs
Solving Satisfiability Problems on FPGAs
复制标题
解决 FPGA 的可满足性问题
DOI：
10.1007/3-540-61730-2_14
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Hiroshi Sawada
中科院分区：
文献类型：
--
作者：
Takayuki Suyama;M. Yokoo;Hiroshi Sawada
本文提出了一种解决可满足性问题（SAT）的新方法，即，创建专用逻辑电路来解决现场可编程门阵列（FP-GA）上的每个问题实例。最近，由于FPGA技术的进步，用户现在可以创建自己的可重构逻辑电路。此外，通过使用当前的自动逻辑综合技术，用户能够使用高级硬件描述语言（HDL）自动设计逻辑电路。这两种技术的结合使用户能够快速创建专门用于解决单个问题实例的逻辑电路。选择可满足性问题（SAT）是因为它们构成了NP难问题的一个重要子类。我们已经开发了一种新的算法，称为并行检查，这是适合这种方法。在该算法中，所有的变量值被同时分配，并且所有的约束被同时检查。仿真结果表明，该算法中搜索树大小的顺序与Davis-Putnam过程中的顺序大致相同。然后，我们展示了如何并行检查算法可以在FPGA上实现。
This paper presents a report on a new approach for solving satisfiability problems (SAT), i.e., creating a specialized logic circuit to solve each problem instance on Field Programmable Gate Arrays (FP-GAs). Recently, due to advances in FPGA technologies, users can now create their own reconfigurable logic circuits. Furthermore, by using current automatic logic synthesis technologies, users are able to design logic circuits automatically using a high level hardware description language (HDL). The combination of these two technologies have enabled users to rapidly create logic circuits specialized for solving individual problem instances. Satisfiability problems (SAT) were chosen because they make up an important subclass of NP-hard problems. We have developed a new algorithm called parallel-checking, which is suitable for this approach. In the algorithm, all variable values are assigned simultaneously, and all constraints are checked concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs.