﻿ DPLL算法中的变量决策启发式策略

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

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.

[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