两种新的基于扩展规则#SAT问题求解算法  

Two Novel Algorithms Based on Extension Rule for Solving #SAT Problem

作　　者：吕帅[1] 张桐搏 王强[1] 刘磊[1] LYU Shuai;ZHANG Tong-bo;WANG Qiang;LIU Lei(College of Computer Science and Technology,Jilin University,Changchun 130012,China)

机构地区：[1]吉林大学计算机科学与技术学院,吉林长春130012

出　　处：《东北大学学报（自然科学版）》2019年第5期630-634,646,共6页Journal of Northeastern University(Natural Science)

基　　金：国家重点研究发展计划项目(2017YFB1003103);国家自然科学基金资助项目(61502197;61503044;61763003);吉林省科技发展计划项目(20180101053JC)

摘　　要：提出一种新的基于扩展规则的#SAT求解算法NCER,该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现,结合NCER和CDP的优点提出混合#SAT求解算法NCDPER.实验结果表明:NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高.通过与目前最好的基于扩展规则的#SAT求解器的比较,该求解器具有更好的性能.A novel #SAT solver NCER based on extension rule is proposed,which adds heuristic strategy on #ER algorithm.The heuristic strategy chooses the longest clause in current set of clauses every calling procedure to reduce the maxterm space,and it helps decrease the frequency of recursive invocation to enhance the efficiency of solving.Besides,a mixed model counting algorithm called NCDPER is proposed by combining NCER algorithm and CDP algorithm,to overcome the poor performance on instances where complementary factor of the #SAT solvers is small using the extension rule.NCDPER integrates advantages of NCER algorithm and CDP algorithm.According to the experimental results,NCER has a significant improvement over previous #SAT solvers on all 85 random SAT instances.The #SAT solvers proposed are compared with state-of-the-art #SAT solvers using extension rule,and the results show that the proposed #SAT solvers have better performances.

关 键 词：自动推理 扩展规则 模型计数 极大项空间 启发式策略 

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