Page 120 - 《软件学报》2021年第9期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(9):2744−2754 [doi: 10.13328/j.cnki.jos.005974] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

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

1,2
1,2
1
1,2
李 壮 , 刘 磊 , 张桐搏 , 周文博 , 吕 帅 1,2
1
(吉林大学 计算机科学与技术学院,吉林 长春 130012)
2 (符号计算与知识工程教育部重点实验室(吉林大学),吉林 长春 130012)
通讯作者: 吕帅, E-mail: lus@jlu.edu.cn

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

中文引用格式: 李壮,刘磊,张桐搏,周文博,吕帅.基于局部搜索的并行扩展规则推理方法.软件学报,2021,32(9):2744−2754.
http://www.jos.org.cn/1000-9825/5974.htm
英文引用格式: Li Z, Liu L, Zhang TB, Zhou WB, Lü S. Local search-based parallel extension rule reasoning method. Ruan Jian
Xue Bao/Journal of Software, 2021,32(9):2744−2754 (in Chinese). http://www.jos.org.cn/1000-9825/5974.htm

Local Search-based Parallel Extension Rule Reasoning Method
1,2
1
1,2
1,2
LI Zhuang , LIU Lei , ZHANG Tong-Bo , ZHOU Wen-Bo , LÜ Shuai 1,2
1 (College of Computer Science and Technology, Jilin University, Changchun 130012, China)
2 (Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University), Changchun 130012, China)
Abstract: 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

∗ 基金项目: 国家重点研发计划(2017YFB1003103); 国家自然科学基金(61300049, 61763003); 吉林省自然科学基金(2018
0101053JC, 20190201193JC, 20190103005JH); 吉林大学研究生创新基金(101832018C025)
Foundation item: National Key Research and Development Program of China (2017YFB1003103); National Natural Science
Foundation of China (61300049, 61763003); Natural Science Research Foundation of Jilin Province of China (20180101053JC,
20190201193JC, 20190103005JH); Graduate Innovation Fund of Jilin University of China (101832018C025)
收稿时间: 2019-02-28; 修改时间: 2019-08-25; 采用时间: 2019-10-30; jos 在线出版时间: 2019-12-05
CNKI 网络优先出版: 2019-12-05 14:55:15, http://kns.cnki.net/kcms/detail/11.2560.TP.20191205.1454.007.html