主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
王强,刘磊,吕帅.基于扩展规则的启发式#SAT求解算法.软件学报,2018,29(11):3517-3527
基于扩展规则的启发式#SAT求解算法
#SAT Solving Algorithms Based on Extension Rule Using Heuristic Strategies
投稿时间:2016-11-29  修订日期:2017-01-11
DOI:10.13328/j.cnki.jos.005298
中文关键词:  扩展规则  模型计数  启发式算法  极大项空间  规约子句
英文关键词:extension rule  model counting  heuristic strategy  maxterm space  reduction clause
基金项目:国家自然科学基金(61300049,61402195,61502197,61503044);教育部高等学校博士学科点专项科研基金(201200 61120059);吉林省自然科学基金(20180101053JC);吉林省青年科研基金(20140520069JH,20150520058JH)
作者单位E-mail
王强 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
 
刘磊 吉林大学 计算机科学与技术学院, 吉林 长春 130012  
吕帅 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
lus@jlu.edu.cn 
摘要点击次数: 1071
全文下载次数: 714
中文摘要:
      #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 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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利