软件学报

作者：李壮，刘磊，张桐搏，周文博，吕帅

单位：李壮，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001211,刘磊，吉林大学计算机科学与技术学院, 吉林 长春 13001202,张桐搏，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001203,周文博，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001204,吕帅，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001205

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

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

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

来源：2021年第9期

《软件学报》期刊编辑部

查看软件学报杂志2021年第9期