[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.
|