基于扩展规则的启发式#SAT求解算法

来源：软件学报杂志2018年第11期北京时间：

作者：王强,刘磊,吕帅

单位：王强，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001211,刘磊，吉林大学 计算机科学与技术学院, 吉林 长春 13001202,吕帅，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001203

摘要：#SAT在人工智能领域取得了广泛应用，很多现实问题可以规约成#SAT进行求解，得到命题理论的模型个数.通过对基于扩展规则的#SAT求解器的深入研究，发现选择规约子句的顺序对极大项空间的大小有着较大的影响，因此提出两种加速#SAT求解的启发式策略：MW和LC&MW.MW每次选择具有最大权值的子句作为规约子句；LC&MW每次选择最长子句作为规约子句，若最长子句存在多个，则在多个最长子句中选择具有最大权值的子句作为规约子句.利用MW策略设计了算法CER_MW，利用LC&MW策略设计了算法CER_LC&MW.实验结果表明，CER_MW和CER_LC&MW相对于先前的#SAT求解算法在求解效率和求解能力上都有显著的提高.在求解效率方面，CER_MW和CER_LC&MW的求解速度是其他算法的1.4倍~100倍.在求解能力方面，CER_MW和CER_LC&MW在限定时间内可解的测试用例更多.

关键词：扩展规则;模型计数;启发式算法;极大项空间;规约子句

基金资助：国家自然科学基金（61300049，61402195，61502197，61503044）；教育部高等学校博士学科点专项科研基金（201200 61120059）；吉林省自然科学基金（20180101053JC）；吉林省青年科研基金（20140520069JH，20150520058JH）