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

Research Advance of SAT Solving Algorithm

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.