主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
李壮,刘磊,张桐搏,周文博,吕帅.基于局部搜索的并行扩展规则推理方法.软件学报,0,(0):0
基于局部搜索的并行扩展规则推理方法
Local Search-Based Parallel Extension Rule Reasoning Method
投稿时间:2019-02-28  修订日期:2019-08-25
DOI:10.13328/j.cnki.jos.005974
中文关键词:  自动推理  局部搜索  扩展规则  格局检测  并行框架
英文关键词:automated reasoning  local search  extension rule  configuration checking  parallel framework
基金项目:国家重点研发计划项目(2017YFB1003103);国家自然科学基金项目(61300049,61763003);吉林省自然科学基金项目(20180101053JC,20190201193JC);吉林大学研究生创新基金资助项目(101832018C025)
作者单位E-mail
李壮 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
 
刘磊 吉林大学 计算机科学与技术学院, 吉林 长春 130012  
张桐搏 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
 
周文博 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
 
吕帅 吉林大学 计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
lus@jlu.edu.cn 
摘要点击次数: 255
全文下载次数: 122
中文摘要:
      扩展规则推理方法在经典的可满足性问题求解中已得到广泛应用,若干个基于扩展规则的推理方法已被提出,皆得到国内外的认可.例如完备的NER、IMOMH_IER、PPSER算法,以及基于局部搜索的不完备算法ERACC等,都具有良好的求解效果.其中,ERACC算法是当前扩展规则求解器中求解效率最高,能力最强的算法.但是串行ERACC算法在启发式和预处理上仍然具有可提升的空间,本文基于此设计了相应的并行框架,提出了PERACC算法.该算法基于格局检测的局部搜索方法,从变量赋初始值,化简解空间和启发式三个阶段出发,将原极大项空间分解成为若干极大项子空间并对原子句集进行化简后,并行处理各个子空间.通过实验显示,该算法与原算法相比,不仅在求解效率方面有较大地提高,而且可以求解规模更大的测试用例,使扩展规则方法再次突破公式规模的限制.
英文摘要:
      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. For example, the complete algorithms like NER, IMOMH_IER, PPSER, and partial search-based incomplete algorithm like ERACC. All of them have good 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. So we designed a parallel framework and called it PERACC algorithm. We were 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 assign initial values to variables, simplifying solution space and heuristic. Simplifying the original clause set, then processes each subspace in parallel. Experiments show that, compared with the original algorithm, the new algorithm not only can be improved the efficiency of solution, but also can be solved larger benchmark, which makes the extension rule method break through the limitation of formula size again.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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