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

Local Search-based Parallel Extension Rule Reasoning Method

作　　者：李壮[1,2] 刘磊 张桐搏[1,2] 周文博 吕帅[1,2] LI Zhuang;LIU Lei;ZHANG Tong-Bo;ZHOU Wen-Bo;LÜ Shuai(College of Computer Science and Technology,Jilin University,Changchun 130012,China;Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University),Changchun 130012,China)

机构地区：[1]吉林大学计算机科学与技术学院,吉林长春130012 [2]符号计算与知识工程教育部重点实验室(吉林大学),吉林长春130012

出　　处：《软件学报》2021年第9期2744-2754,共11页Journal of Software

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

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

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

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]