DPLL算法中的变量决策启发式策略
Heuristic Strategies for Deciding Variables in DPLL Algorithm

作者: 刘文秀 , 江建国 , 李千卉 :辽宁师范大学数学学院,辽宁 大连;

关键词: DPLL算法启发式策略可满足性问题DPLL Algorithm Heuristic Strategy Propositional Satisfiability Problem

摘要:
针对命题公式φ(CNF形式)的可满足性问题的求解效率问题,基于对DPLL完全算法的学习和在不同形式下对子句文字排序处理的研究,提出了一种新的求解SAT问题的算法。新算法根据子句长度对命题公式φ进行分组,并根据变量出现次数进行初始排序,然后考虑变量中正负文字出现的次数,并对次数高的进行赋值。算法实例表明:新算法能减少求解过程中规则使用次数,减少求解步骤,尽早剪除不满足解空间,从而有效提高求解效率。

Abstract: Aiming at the problem of the resolution efficiency of propositional satisfiability problem for propositional formula φ (CNF Form), based on the study of the DPLL complete algorithm and the research of the word order processing under different forms, a new algorithm for solving SAT problem is proposed. The algorithm groups propositional formula φ according to the length of clause, and sorts the words according to the number of polarity occurrence frequency in the initial sort. Then it considers the number of occurrences of the plus or minus words in variables and gets the value of high numbers. Algorithm instance shows that the new algorithm can reduce the number of rules in the process of using, reduce the solving steps, cut off the unsatisfy space of solution as soon as possible, so as to improve the solution efficiency.

文章引用: 刘文秀 , 江建国 , 李千卉 (2016) DPLL算法中的变量决策启发式策略。 软件工程与应用, 5, 47-55. doi: 10.12677/SEA.2016.51006

参考文献

[1] Davis, M. and Putnam, H. (1960) A Computing Procedure for Quantification Theory. Journal of the ACM, 7, 201-215.
http://dx.doi.org/10.1145/321033.321034

[2] Davis, M., Logemann, G. and Loveland, D. (1962) A Machine Program for Theorem Proving. Communications of the ACM, 5, 394-397.
http://dx.doi.org/10.1145/368273.368557

[3] 郭庆贺. 基于DPLL和GPS的同步信号合成及授时系统研究[D]: [硕士学位论文]. 南京: 南京理工大学, 2013.

[4] 李壮. 基于细胞膜演算的伴随子句学习的DPLL算法描述[D]: [硕士学位论文]. 长春: 吉林大学, 2015.

[5] Bonacina, M.P. and Johansson, M. (2011) On Interpolation in Decision Procedures. Automated Reasoning with Analytic Tableaux and Related Methods: Lecture Notes in Computer Science, 6793, 1-16.
http://dx.doi.org/10.1007/978-3-642-22119-4_1

[6] 金继伟, 马菲菲, 张建. SMT求解技术简述[J]. 计算机科学与探索, 2015(7): 769-780.

[7] 姜波. DPLL在异形板材预热电源中的应用研究[D]: [硕士学位论文]. 阜新: 辽宁工程技术大学, 2013.

[8] 陈稳. 基于DPLL的SAT算法的研究及应用[D]: [硕士学位论文]. 成都: 电子科技大学, 2011.

[9] 王洪琳. 基于DPLL的#SAT子类算法的研究[D]: [硕士学位论文]. 长春: 东北师范大学, 2013.

[10] 胡显伟, 任世军. 基于函数变换的求解SAT问题的新算法[J]. 智能计算机与应用, 2012, 2(3): 33-36.

[11] 余晓星. 一种SAT邻域的快速搜索算法[J]. 现代计算机, 2012(4): 9-11.

[12] 徐云, 陈国良, 张国义. 一种求解难SAT问题的改进DP算法[J]. 中国科学技术大学学报, 2002, 32(3): 358-362.

[13] 邓晓瑶, 冯志勇, 饶国政, 王鑫. 基于子句文字长度动态约束的变量消除算法[J]. 计算机科学与探索, 2014, 8(11): 1314-1323.

[14] 毕忠勤, 陈光喜, 单美静. 可满足性问题全部解的求解算法[J]. 计算机工程与应用, 2009, 45(3): 35-37.

[15] Nieuwenhuis, R., Oliveras, A. and Tinelli, C. (2006) Solving SAT and SAT Modulo Theories: From an Abstract Davis- Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM, 53, 937-977.
http://dx.doi.org/10.1145/1217856.1217859

[16] Moskewicz, M.W., Madigan, C.F., Zhao, Y., et al. (2001) CHAFF: Engineering an Efficient SAT Solver. Proceedings of the 38th Design Automation Conference, 17, 530-535.

分享
Top