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

来源：计算机工程与科学杂志2016年第4期北京时间：

作者：马柯帆，肖立权,张建民，黎铁军

单位：（国防科学技术大学计算机学院，湖南 长沙 410073）

摘要：布尔可满足性SAT问题作为第一个被证明的NP完全问题，是计算机理论与应用的核心问题，有着重要的应用价值，因此近年来涌现了各种各样SAT求解器。但是，SAT求解器的运算效率始终是影响其应用的关键因素，所以利用硬件的高性能与并行性来加速SAT求解过程已成为验证领域的一个研究热点。归纳总结了在SAT求解过程中，利用硬件现场可编程门逻辑FPGA的并行性和灵活性加速求解过程的各种算法研究，着重总结分析了应用型SAT求解器的加速策略。通过对各种方法的深入分析，指出它们的优缺点，为未来的研究提供了思路。

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

基金资助：国家自然科学基金（61103083，61133007）