基于局部搜索的并行扩展规则推理方法
作者:
作者单位:

作者简介:

李壮(1988-),男,博士,主要研究领域为人工智能,自动推理,机器学习.
周文博(1991-),男,博士,CCF学生会员,主要研究领域为形式化方法,云计算.
刘磊(1960-),男,教授,博士生导师,CCF专业会员,主要研究领域为软件理论与技术.
吕帅(1981-),男,博士,副教授,博士生导师,CCF高级会员,主要研究领域为人工智能,机器学习,自动推理.
张桐搏(1995-),男,硕士,主要研究领域为人工智能,自动推理,云计算.

通讯作者:

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

中图分类号:

TP181

基金项目:

国家重点研发计划(2017YFB1003103);国家自然科学基金(61300049,61763003);吉林省自然科学基金(20180101053JC,20190201193JC,20190103005JH);吉林大学研究生创新基金(101832018C025)


Local Search-based Parallel Extension Rule Reasoning Method
Author:
Affiliation:

Fund Project:

National Key Research and Development Program of China (2017YFB1003103); National Natural Science Foundation of China (61300049, 61763003); Natural Science Research Foundation of Jilin Province of China (20180101053JC, 20190201193JC, 20190103005JH); Graduate Innovation Fund of Jilin University of China (101832018C025)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    扩展规则推理方法在经典的可满足性问题求解中已得到广泛应用,若干个基于扩展规则的推理方法已被提出,皆得到国内外的认可,例如完备的NER,IMOMH_IER,PPSER算法以及基于局部搜索的不完备算法ERACC等,都具有良好的求解效果.其中,ERACC算法是当前扩展规则求解器中求解效率最高、能力最强的算法.但是,串行的ERACC算法在启发式和预处理上仍然具有可提升的空间.基于此,设计了相应的并行框架,提出了PERACC算法.该算法基于格局检测的局部搜索方法,从变量赋初始值、化简解空间和启发式这3个阶段出发,将原极大项空间分解成为若干极大项子空间,并对原子句集进行化简后,并行处理各个子空间.通过实验显示:该算法与原算法相比,不仅在求解效率方面有较大提高,而且可以求解规模更大的测试用例,使扩展规则方法再次突破公式规模的限制.

    Abstract:

    Extension rule reasoning method has been widely used in solving the classical satisfiability problem. Several reasoning methods based on extension rule have been proposed, which have been recognized around the world. These methods include the complete algorithms like NER, IMOMH_IER, PPSER, and local search-based incomplete algorithm like ERACC. All of them have sound performance. ERACC algorithm is the most efficient and powerful algorithm in the current extension rule solver. However, the serial algorithm ERACC still needs improvement on heuristics and preprocessing. Therefore, a parallel framework is designed and it is called PERACC algorithm. Based on the configuration checking of local search method, the algorithm decomposes the original maximum term space into several maximum term subspaces, from three stages of assigning initial values to variables, simplifying solution space, and heuristic, simplifying the original clause set, then processing each subspace in parallel. Experiments show that, compared with the original algorithm, the proposed algorithm not only can improve the efficiency of solution, but also can solve larger benchmark, which makes the extension rule method break through the limitation of formula size again.

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

李壮,刘磊,张桐搏,周文博,吕帅.基于局部搜索的并行扩展规则推理方法.软件学报,2021,32(9):2744-2754

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

京公网安备 11040202500063号