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

#SAT Solving Algorithms Based on Extension Rule Using Heuristic Strategies

作　　者：王强[1,2] 刘磊[1] 吕帅[1,2] WANG Qiang;LIU Lei;LU Shuai(College of Computer Science and Technology,Jilin University,Changehun 130012,China;Key Laboratory of Symbolic Computation and Knowledge Engineering（Jilin University）,Ministry of Education,Changehun 130012,China)

机构地区：[1]吉林大学计算机科学与技术学院,吉林长春130012 [2]符号计算与知识工程教育部重点实验室(吉林大学),吉林长春130012

出　　处：《软件学报》2018年第11期3517-3527,共11页Journal of Software

基　　金：国家自然科学基金(61300049;61402195;61502197;61503044);教育部高等学校博士学科点专项科研基金(201200 61120059);吉林省自然科学基金(20180101053JC);吉林省青年科研基金(20140520069JH;20150520058JH)~~

摘　　要：#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在限定时间内可解的测试用例更多.#SAT is used widely in the field of artificial intelligence, and many real-world problems can be reduced to #SAT to get the number of models of a propositional theory. By an in-depth study of #SAT solvers using extension rule, this paper finds that the order of reduction clause has great impact on the size of maxterm space. Thus, in this paper two heuristic strategies, MW and LCMW are proposed to enhance the efficiency of solving #SAT. MW chooses the clause with maximum weight as reduction clause in every calling procedure; LCMW chooses the longest clause as reduction clause in every calling procedure and takes the clause with maximum weight as tie breaker. The algorithm CER_MW is designed by using MW, and the algorithm CER_LCMW is designed by using LCMW. According to the experimental results, CER_MW and CER_LCMW show a significant improvement over previous #SAT algorithms. Comparing the new #SAT solvers with other state-of-the-art #SAT solvers using extension rule also shows that CER_MW and CER_ LCMW are significantly improved over the previous #SAT algorithms in solving efficiency and solving capacity. In terms of efficiency, the speed of CER_MW and CER_LCMW is 1.4~100 times that of other algorithms. In terms of capacity, CER_MW and CER_LCMW can solve more instances in a time limit.

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

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]