FPGA-based Hardware/Software Co-design of a Bio-inspired SAT Solver
FPGA-based Hardware/Software Co-design of a Bio-inspired SAT Solver
复制标题
基于 FPGA 的仿生 SAT 求解器的硬件/软件协同设计
DOI：
10.1109/access.2020.2980008
复制
发表时间：
2020
期刊：
影响因子：
3.9
通讯作者：
and Yuko Hara-Azumi
中科院分区：
文献类型：
--
作者：
Anh Hoang Ngoc Nguyen;Masashi Aono;and Yuko Hara-Azumi
针对控制规则可以用可满足性(SAT)问题表示的各种物联网(IoT)系统，采用硬件/软件协同设计的方法，利用仿生算法AmoebaSAT，实现了一种面向IoT的基于FPGA的SAT求解器。在软件组件方面，我们对基线算法进行了扩展，以更快地摆脱局部极小值，并实现了迭代次数的显著减少。在硬件方面，充分提取了算法的细粒度并行性，进一步加速了解的搜索。通过使用几个不同变量数量和复杂性的基准测试进行评估，我们证明了我们的求解器的效率，特别是对于较大的实际SAT实例。与三个先进的解算器(即一个软件实现原始的AmoebaSAT算法和两个基于FPGA的硬件解算器)相比，迭代次数平均减少了15.9倍，最高可减少48倍。此外，通过对实验结果的深入分析，我们提供了问题复杂性与SAT算法之间关系的基本发现，可用于硬件和软件设计的扩展。
For various kinds of Internet of Things (IoT) systems whose control rules can be expressed in a Satisfiability (SAT) problem, this work aims at realizing an IoT-oriented FPGA-based SAT solver leveraging a bio-inspired algorithm, AmoebaSAT, using a hardware/software co-design approach. With regard to the software component, we extended the baseline algorithm to escape from local minima more quickly and achieve significant reduction in iteration count. With regard to hardware, we fully extracted the fine-grained parallelism of the algorithm to further accelerate the solution search. Through our evaluations using several benchmarks of varying variable count and complexity, we demonstrated the efficiency of our solver, especially for larger practical SAT instances. Compared with three state-of-the-art solvers (i.e., one software implementation of the original AmoebaSAT algorithm and two FPGA-based hardware solvers), we achieved an average of 15.9× and up to 48× reduction in iteration count. Furthermore, through in-depth analyses of the experimental results, we provided the essential findings on the relationship between the problem's complexity and the SAT algorithm that can be leveraged for extensions of both the hardware and software designs.