求解SAT问题的算法的研究进展  

Research Advance of SAT Solving Algorithm

作　　者：郭莹[1,2] 张长胜[1] 张斌[1] 

机构地区：[1]东北大学信息科学与工程学院,沈阳110819 [2]宁夏理工学院电气信息工程学院,石嘴山753000

出　　处：《计算机科学》2016年第3期8-17,共10页Computer Science

基　　金：宁夏回族自治区自然科学基金资助项目(NZ13265)资助

摘　　要：SAT问题是研究最广泛的NPC问题之一。由于SAT问题本身的特性,除非P=NP,否则不存在最坏情况下多项式阶时间复杂度的SAT求解算法。因此设计出高效快速的SAT求解算法至今仍是研究热点。首先简要介绍了SAT问题;其次从完备算法、不完备算法和组合算法3个角度总结了新近的研究进展,深入分析了已有算法解决SAT问题的基本流程,并从适用问题类别、算法特点、求解效率等方面对各类先进的求解器进行了对比分析;最后讨论了求解SAT问题的算法面临的挑战,并对下一步研究工作进行了展望。SAT is one of the most widely studied NPC problems.Because of SAT characteristic,unless P=NP,polynomial time worst-case complexity of SAT algorithm does not exist.To design fast and efficient SAT algorithms is still a research hotspot.Firstly,the basic concept of SAT problem was introduced.Secondly,the recent research progress was summarized from three categories of complete algorithms,incomplete algorithms and combination algorithms.The general process of previous algorithms was thoroughly analyzed,and comparative analysis of some advanced solvers from the perspective of suitable problem class,algorithm character and solution efficiency was carried on.Finally,the main challenges of SAT solving algorithm was discussed,and some research issues in future were pointed out.

关 键 词：SAT问题 完备算法 不完备算法 组合算法 

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