基于局部搜索的并行扩展规则推理方法

作     者：李壮 刘磊 张桐搏 周文博 吕帅 LI Zhuang;LIU Lei;ZHANG Tong-Bo;ZHOU Wen-Bo;LÜ Shuai

作者机构：吉林大学计算机科学与技术学院吉林长春130012 符号计算与知识工程教育部重点实验室(吉林大学)吉林长春130012 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2021年第32卷第9期

页      面：2744-2754页

核心收录：

学科分类：08[工学] 081104[工学-模式识别与智能系统] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：自动推理 局部搜索 扩展规则 格局检测 并行框架 

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