基于扩展规则的启发式#SAT求解算法
作者:
作者单位:

作者简介:

王强(1994-),男,山西临汾人,硕士,主要研究领域为人工智能,智能规划与自动推理;吕帅(1981-),男,博士,副教授,CCF高级会员,主要研究领域为人工智能,智能规划与自动推理;刘磊(1960-),男,教授,博士生导师,CCF专业会员,主要研究领域为软件理论与技术.

通讯作者:

吕帅,E-mail:lus@jlu.edu.cn

中图分类号:

基金项目:

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


#SAT Solving Algorithms Based on Extension Rule Using Heuristic Strategies
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61300049, 61402195, 61502197, 61503044); Specialized Research Fund for the Doctoral Program of Higher Education of China (20120061120059); Natural Science Research Foundation of Jilin Province (20180101053JC); Natural Science Research Foundation of Jilin Province for Young Scholars (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在限定时间内可解的测试用例更多.

    Abstract:

    #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 LC&MW are proposed to enhance the efficiency of solving #SAT. MW chooses the clause with maximum weight as reduction clause in every calling procedure; LC&MW 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_LC&MW is designed by using LC&MW. According to the experimental results, CER_MW and CER_LC&MW 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_LC&MW 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_LC&MW is 1.4~100 times that of other algorithms. In terms of capacity, CER_MW and CER_LC&MW can solve more instances in a time limit.

    参考文献
    相似文献
    引证文献
引用本文

王强,刘磊,吕帅.基于扩展规则的启发式#SAT求解算法.软件学报,2018,29(11):3517-3527

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2016-11-29
  • 最后修改日期:2017-01-11
  • 录用日期:
  • 在线发布日期: 2018-04-16
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号