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

摘要：

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

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

所属期刊栏目：32

分类号：TP181(自动化基础理论)

资助基金：国家重点研发计划;国家自然科学基金;吉林省自然科学基金;吉林大学研究生创新基金

在线出版日期：2021-09-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：2744-2754