基于硬件可编程逻辑的SAT求解算法研究与进展  

State of the art and future research of a SAT problem solver on FPGA

作　　者：马柯帆[1] 肖立权[1] 张建民[1] 黎铁军[1] 

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

出　　处：《计算机工程与科学》2016年第4期634-639,共6页Computer Engineering & Science

基　　金：国家自然科学基金(61103083;61133007)

摘　　要：布尔可满足性SAT问题作为第一个被证明的NP完全问题,是计算机理论与应用的核心问题,有着重要的应用价值,因此近年来涌现了各种各样SAT求解器。但是,SAT求解器的运算效率始终是影响其应用的关键因素,所以利用硬件的高性能与并行性来加速SAT求解过程已成为验证领域的一个研究热点。归纳总结了在SAT求解过程中,利用硬件现场可编程门逻辑FPGA的并行性和灵活性加速求解过程的各种算法研究,着重总结分析了应用型SAT求解器的加速策略。通过对各种方法的深入分析,指出它们的优缺点,为未来的研究提供了思路。As the first proved NP-complete problem,Boolean satisfiability problem（SAT）is a key problem in computer theory and applications,and has crucial significance in both theoretical research and practical applications.A variety of SAT solvers have emerged in recent years.However,the operation efficiency of SAT solvers is always a key factor affecting its applications,so taking advantage of the hardware＇s high performance and parallelism to accelerate the SAT solving process becomes a hot research topic in the area of verification.We summarize the methods for accelerating SAT solving solution,which use the parallelism and flexibility of FPGA,and analyze the acceleration policies of application-specified solver emphatically.Through in-depth analysis of these methods,we point out their advantages and disadvantages,and provide ideas for future research.

关 键 词：现场可编程门逻辑 可满足性 求解器 

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