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

J4 ›› 2016, Vol. 38 ›› Issue (04): 634-639.

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

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

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

收稿日期:2015-08-26 修回日期:2015-10-24 出版日期:2016-04-25 发布日期:2016-04-25
基金资助:
国家自然科学基金（61103083，61133007）

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

MA Kefan，XIAO Liquan,ZHANG Jianmin，LI Tiejun

(College of Computer,National University of Defense Technology,Changsha 410073,China)

Received:2015-08-26 Revised:2015-10-24 Online:2016-04-25 Published:2016-04-25

摘要/Abstract

摘要：

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

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

Abstract:

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.

Key words: FPGA;SAT;solver

马柯帆，肖立权,张建民，黎铁军. 基于硬件可编程逻辑的SAT求解算法研究与进展[J]. J4, 2016, 38(04): 634-639.

MA Kefan，XIAO Liquan,ZHANG Jianmin，LI Tiejun. State of the art and future research of
a SAT problem solver on FPGA [J]. J4, 2016, 38(04): 634-639.

参考文献［2］

［1］	Cook S A. The complexity of theoremproving procedures［C］∥Proc of the 3rd ACM Symposium on Theory of Computing. 1971:151158.
［2］	Zhou Jin,Zhao Xishun. A survey of SAT algorithm based FPGA［J］. Electronics World,2012(3):6069.(in Chinese)
［3］	Davis M，Logemann M,Loveland D．A machine program for theorem proving［J］. Communication of the ACM, 1962,5(7):394397.
［4］	Davis M,Putnam H． A computer procedure for quantification theory［J］.Journal of the ACM，1960，7(3):202215.
［5］	Zhang Lintao,Malik S．The quest for efficient boolean satisfiability solvers［C］∥Proc of the 14th International Conference on Computer Aided Verification,2002:1736.
［6］	Kanazawa K,Maruyama T. An FPGA solver for WSAT algorthm［C］∥IEEE Proceedings,2005:978981.
［7］	Kanazawa K,Maruyama T. An approach for solving large SAT problems on FPGA［J］.ACM Transactions on Reconfigurable Technology and Systems,2010,4(1):488496.
［8］	Kanazawa K, Maruyama T. An FPGA solver for SATencoded formal verification problems［C］∥Proc of FPL’11,2011:3843.
［9］	Kanazawa K, Maruyama T. Solving SATencoded formal verification problems on SoC based on a WSAT algorithm with a new heuristic for hardware acceleration［C］∥Proc of International Symposium on Embedded Multicore/Manycore SystemonChip,2013:101106.
［10］	Kanazawa K, Maruyama T. FPGA acceleration of SATMaxSAT solving using variableway cache［C］∥Proc of FPL’14,2014:1.
［11］	Yokoo M,Suyama T,Sawada H. Solving satisfiability problems using field programmable gate arrays:First results［C］∥Proc of Principles and Practice of Constraint Programming(CP’96),1996:497509.
［12］	Suyama T,Yokoo M,Sawada H,et al,Solving satisfiability problems using reconfigurable computing ［J］.IEEE Transactions on Very Large Scale Integration (VLSI) Systems,2001,9(1):109116.
［13］	Zhong P,Ashar P,Malik S,et al. Using reconfigurable computing techniques to accelerate problems in the CAD domain:A case study with boolean satisfiability ［C］∥Proc of the 35th Annual Design Automation Conference,1998:194199.
［14］	Zhong P,Martonosi M,Ashar P,et al. Accelerating Boolean satisfiability with configurable hardware［C］∥Proc of IEEE Symposium on FPGAs for Custom Computing Machines,Proceedings,1998:186195.
［15］	Zhong P, Martonosi M, Ashar P. FPGAbased SAT solver architecture with nearzero synthesis and layout overhead［C］∥Proc of Computers and Digital Techniques,IEEE Proceedings, 2000:135141.
［16］	Safar M, ElKharashi M W,Shalan M, et al. A reconfigurable,pipelined,conflict directed jumping search SAT solver ［C］∥Proc of Design,Automation and Test in Europe,2011:978981.
［17］	Ivan T,Aboulhamid E l M. An efficient hardware implementation of a SAT problem solver on FPGA［C］∥Euromicro Conference on Digital System Design,2013.
［18］	Haller L,Singh S. Relieving capacity limits on FPGAbased SATsolvers［C］∥Proc of FMCAD’13,2013:217220.
［19］	Davis J D,Tan Zhangxi. A practical reconfigurable hardware accelerator for boolean satisfiability solvers［C］∥Proc of DAC’08,2008:780785.
［20］	Thong J,Nicolic N. FPGA acceleration of enhanced boolean constraint propagation for SAT solvers［C］∥Proc of ICCAD’13,2013:234241.
	附中文参考文献：
［2］	周进，赵希顺. 基于硬件可编程逻辑（FPGA）的SAT算法的综述［J］.电子世界，2012(3):6069.

[1]	黎兴玉, 何星星, 马雪, 李莹芳. 命题逻辑中一种矛盾体生成新方法[J]. 计算机工程与科学, 2023, 45(06): 1134-1140.
[2]	王欣怡, 殷志祥, 唐震, 杨静, 崔建中, . 基于DNA折纸术求解可满足性问题的计算模型[J]. 计算机工程与科学, 2021, 43(09): 1529-1537.
[3]	张建民，黎铁军，马柯帆，肖立权. 基于一阶逻辑的可满足求解方法研究进展[J]. 计算机工程与科学, 2019, 41(12): 2119-2126.
[4]	吴贯锋1,2，徐扬2,3,陈青山1,2,何星星2,3，常文静1,2. 基于频次的SAT问题学习子句混合评估算法[J]. 计算机工程与科学, 2019, 41(08): 1374-1380.
[5]	胡潇洒，张越岭，李建文，蒲戈光，张敏. 基于不可满足原因的最小纠正集求解[J]. 计算机工程与科学, 2018, 40(06): 1067-1074.
[6]	罗炜麟，魏欧，黄鸣宇. 基于SAT求解器的故障树最小割集求解算法[J]. 计算机工程与科学, 2017, 39(04): 725-733.
[7]	何安平，吴尽昭，梁艺，熊玲芳，吴昊. 基于几何规划的布尔可满足问题求解方法[J]. J4, 2013, 35(9): 122-126.
[8]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[9]	李〓婧，刘万伟. SMT求解器理论组合技术研究[J]. J4, 2011, 33(10): 111-119.
[10]	张建民, 沈胜宇, 李思昆. 可满足性求解技术研究[J]. J4, 2010, 32(1): 50-54.