基于不完全算法的并行FPGA SAT求解器  

A parallel FPGA SAT solver based on incomplete algorithm

作　　者：黎铁军[1] 马柯帆[1] 张建民[1] LI Tie-jun;MA Ke-fan;ZHANG Jian-min(College of Computer Science and Technology,National University of Defense Technology,Changsha 410073,China)

机构地区：[1]国防科技大学计算机学院,湖南长沙410073

出　　处：《计算机工程与科学》2021年第12期2126-2130,共5页Computer Engineering & Science

基　　金：国家自然科学基金(62072464,U19A2062);并行与分布处理国家级重点实验室开放基金(WDZC20205500116)。

摘　　要：可满足性问题是计算机理论与应用的核心问题。在FPGA上提出了一个基于不完全算法的并行求解器pprobSAT+。使用多线程的策略来减少相关组件的等待时间,提高了求解器效率。此外,不同线程采用共用地址和子句信息的数据存储结构,以减少片上存储器的资源开销。当所有数据均存储在FPGA的片上存储器时,pprobSAT+求解器可以达到最佳性能。实验结果表明,相比于单线程的求解器,所提出的pprobSAT+求解器可获得超过2倍的加速比。The Boolean satisfiability(SAT)problem is the key problem in computer theory and application.his paper proposes a parallel SAT solver based on incomplete algorithm on FPGA.The algorithm uses a multi-threaded strategy to reduce the waiting time of related components and improve the efficiency of the solver.In addition,different threads use data storage structures that share addresses and clause information to reduce the resource overhead of on-chip memory.When all data is stored in the FPGA’s on-chip memory,the solver can achieve the best performance.The experimental results show that,compared with the single-threaded solver,the solver proposed in this paper can achieve a speedup of more than 2 times.

关 键 词：布尔可满足 FPGA 不完全算法 多线程 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]