基于IAPS的扩展规则局部搜索算法

doi:10.3969/j.issn.0372-2112.2020.05.009

电子学报 ›› 2020, Vol. 48 ›› Issue (5): 899-905.DOI: 10.3969/j.issn.0372-2112.2020.05.009

基于IAPS的扩展规则局部搜索算法

王金艳^1,2, 胡春², 牛当当^1,3, 李先贤^1,2

1. 广西多源信息挖掘与安全重点实验室(广西师范大学), 广西桂林 541004;
2. 广西师范大学计算机科学与信息工程学院, 广西桂林 541004;
3. 西北农林科技大学信息工程学院, 陕西杨凌 712100

收稿日期:2019-11-15 修回日期:2020-02-10 出版日期:2020-05-25
- 通讯作者:
- 李先贤
- 作者简介:
- 王金艳 女,1982年1月2日生,广西资源人.现为广西师范大学计算机科学与信息工程学院副教授,主要研究方向为自动推理和数据安全.E-mail:wangjy612@gxnu.edu.cn;胡春男,1995年3月1日生,江西南昌人.现为广西师范大学计算机科学与信息工程学院研究生,主要研究方向为自动推理和人工智能.E-mail:huchungxnu@163.com;牛当当 男,1990年2月出生,陕西周至人.现为西北农林科技大学信息工程学院讲师,主要研究方向为自动推理和抽象论辩.E-mail:niudd@nwafu.edu.cn
- 基金资助:
- 国家自然科学基金 (No.61763003，No.61672176，No.61941201）; 广西多源信息挖掘与安全重点实验室系统性研究课题基金 (No.19-A-02-01）; 广西多源信息挖掘与安全重点实验室开放基金 (No.MIMS19-05）; 广西高等学校千名中青年骨干教师培育计划; "八桂学者"工程专项经费资助项目; 广西大数据智能与应用人才小高地; 广西区域多源信息集成与智能处理协同创新中心

An Extension Rule Algorithm Based on Local Search with IAPS Strategies

WANG Jin-yan^1,2, HU Chun², NIU Dang-dang^1,3, LI Xian-xian^1,2

1. Guangxi Key Lab of Multisource Information Mining&Security (Guangxi Normal University), Guilin, Guangxi 541004, China;
2. School of Computer Science and Information Engineering, Guangxi Normal University, Guilin, Guangxi 541004, China;
3. College of Information Engineering, Northwest A&F University, Yangling, Shaanxi 712100, China

Received:2019-11-15 Revised:2020-02-10 Online:2020-05-25 Published:2020-05-25
- Corresponding author:
- LI Xian-xian
- Supported by:
- National Natural Science Foundation of China (No.61763003, No.61672176, No.61941201); Guangxi Key Laboratory Foundation for Multi-source Information Mining and Security (No.19-A-02-01); Guangxi Key Laboratory Foundation for Multi-source Information Mining and Security (No.MIMS19-05); Training Project for Young Backbone Teachers of Universities in Guangxi Province; Supported by the Special Fund of Bagui Scholars Project; Guangxi Talent Highland Project of Big Data Intelligence and Application; Guangxi Regional Multi-Source Information Integration and Intelligent Processing Cooperation Innovation Center

摘要/Abstract

摘要： ERACC（Extension Rule Based on Accurate Configuration Checking）算法由杨洋等人基于扩展规则和格局检测提出，具有较高的推理效率.为进一步提高ERACC算法在大规模SAT（Satisfiability）问题求解上的性能，本文在搜索由极大项组成的空间时，首先利用IMOM（Improved Maximum Occurrences on Clauses of Maximum Size）思想生成初始极大项，接着设计了适用于扩展规则推理的CCA_ER（Configuration Checking with Aspiration for Extension Rule-Based Reasoning）启发式策略，为极大项中格局信息未发生变化的变量对应文字提供一定的翻转机会.同时，为进一步提高扩展规则推理算法在k-SAT问题求解上的性能，设计了适用于扩展规则推理的PAWS_ER（Pure Additive Weighting Scheme for Extension Rule-Based Reasoning）策略，并且给出变量的Subscore_ER（Subscore for Extension Rule-Based Reasoning），CScore_ER（Comprehensive Score for Extension Rule-Based Reasoning）和HScore_ER（Hybrid Score for Extension Rule-Based Reasoning）属性.在此基础上，提出了ERACC_IAPS（ERACC with IMOM，CCA_ER，PAWS_ER and Subscore_ER）和CERACC_IAPS（ERACC with IMOM，CCA_ER，PAWS_ER，CScore_ER and HScore_ER）算法.实验结果表明：ERACC_IAPS和CERACC_IAPS算法的效率明显优于ERACC算法，最高可将其求解效率提高1000多倍.

关键词: 扩展规则, 自动推理, 局部搜索, 格局检测

Abstract: The algorithm ERACC proposed by Yang et al. has high reasoning efficiency. To further improve performance of ERACC algorithm in solving large-scale SAT problem, firstly, IMOM is used to generate the initial maximum term. Then a CCA_ER is designed to provide certain opportunities for the literals of variables whose configurations have not been changed since their last flips in maximal terms. At the same time, in order to further improve the performance of extension rule-based reasoning algorithm on the k-SAT problem, PAWS_ER is designed. Then the Subscore_ER, CScore_ER and HScore_ER attributes for variables are further designed. Finally, ERACC_IAPS and CERACC_ER algorithms are proposed. The experimental results show that the efficiency of ERACC_IAPS and CERACC_IAPS algorithms is obviously better than that of ERACC algorithm, and the maximum solution efficiency can be improved by more than 1000 times.

Key words: extension rule, automated reasoning, local search, configuration checking

中图分类号:

TP181
TP301

王金艳, 胡春, 牛当当, 等. 基于IAPS的扩展规则局部搜索算法[J]. 电子学报, 2020, 48(5): 899-905.

WANG Jin-yan, HU Chun, NIU Dang-dang, et al. An Extension Rule Algorithm Based on Local Search with IAPS Strategies[J]. Acta Electronica Sinica, 2020, 48(5): 899-905.

参考文献

[1] Tompkins D A D,Balint A,Hoos H H.Captain Jack:new variable selection heuristics in local search for SAT[A].Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing[C].Berlin,Germany:Springer,2011.302-316.
[2] Cai S W,Su K L.Local search with configuration checking for SAT[A].Proceedings of the 23rd International Conference on Tools with Artificial Intelligence[C].New York,USA:IEEE Computer Society,2011.59-66.
[3] Cai S W,Su K L.Configuration checking with aspiration in local search for SAT[A].Proceedings of the 26th AAAI Conference on Artificial Intelligence[C].Menlo Park,CA:AAAI Press,2012.434-440.
[4] Cai S W,Su K L.Local search for Boolean Satisfiability with configuration checking and subscore[J].Artificial Intelligence,2013,204:75-98.
[5] Cai S W,Su K L.Comprehensive score:towards efficient local search for SAT with long clauses[A].Proceedings of the 23rd International Joint Conference on Artificial Intelligence[C].Menlo Park,CA:AAAI Press,2013.489-495.
[6] Lin H,Sun J G,Zhang Y M.Theorem proving based on the extension rule[J].Journal of Automated Reasoning,2003,31(1):11-21.
[7] 孙吉贵,李莹,朱兴军,吕帅.一种新的基于扩展规则的定理证明算法[J].计算机研究与发展,2009,46(1):9-14. Sun Ji-Gui,Li Ying,Zhu Xing-Jun,Lü Shuai.A novel theorem proving algorithm based on extension rule[J].Journal of Computer Research and Development,2009,46(1):9-14.(in Chinese)
[8] 张立明,欧阳丹彤,白洪涛.基于半扩展规则的定理证明方法[J].计算机研究与发展,2010,47(9):1522-1529. Zhang Li-Ming,Ouyang Dang-Tong,Bai Hong-Tao.Theorem proving algorithm based on semi-extension rule[J].Journal of Computer Research and Development,2010,47(9):1522-1529.(in Chinese)
[9] 杨洋,刘磊,李广力,张桐搏,吕帅.一种新的基于局部搜索的扩展规则推理方法[J].计算机学报,2018,41(4):825-839. Yang,Liu Lei,Li Guang-Li,Zhang Tong-Bo,Lü Shuai.A novel local search-based extension rule reasoning method[J].Chinese Journal of Computers,2018,41(4):825-839.(in Chinese)
[10] 谷文祥,王金艳,殷明浩.基于MCN和MO启发式策略的扩展规则知识编译方法[J].计算机研究与发展,2011,48(11):2064-2073. Gu Wen-Xiang,Wang Jing-Yan,Yin Ming-Hao.Knowledge compilation using extension rule based on MCN and MO heuristic strategies[J].Journal of Computer Research and Development,2011,48(11):2064-2073.(in Chinese)
[11] 王强,刘磊,吕帅.基于扩展规则的启发式#SAT求解算法[J].软件学报,2018,29(11):3517-3527. Wang Qiang,Liu Lei,Lü Shuai.#SAT solving algorithms based on extension rule using heuristic strategies[J].Journal of Software,2018,29(11):3517-3527.(in Chinese)
[12] 李莹,孙吉贵,吴瑕,朱兴军.基于IMOM和IBOHM启发式策略的扩展规则算法[J].软件学报,2009,20(6):1521-1527. Li Ying,Sun Ji-Gui,Wu Xia,Zhu Xing-Jun.Extension rule algorithms based on IMOM and IBOHM heuristics strategies[J].Journal of Software,2009,20(6):1521-1527.(in Chinese)
[13] Thornton J,Pham D N,Bain S.Additive versus multiplicative clause weighting for SAT[A].Proceedings of the 19th National Conference on artificial Intelligence and 16th Innovative Applications of Artificial Intelligence Conference[C].Menlo Park,CA:AAAI Press,2004.191-196.
[14] Balint A,Schöning U.Choosing probability distributions for stochastic local search and the role of Make versus break[A].Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing[C].Berlin,Germany:Springer,2012.16-29.
[15] Biere A.CaDiCaL,Lingeling,Plingeling treengeling and YalSAT entering the SAT competition 2018[A].Proceedings of SAT Competition 2018:Solver and Benchmark Descriptions,volume B-2018-1 of Department of Computer Science Series of Publications B[C].University of Helsinki,2018.13-14.

基于IAPS的扩展规则局部搜索算法

An Extension Rule Algorithm Based on Local Search with IAPS Strategies

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 14

编辑推荐

Metrics

[1]	张建民, 黎铁军, 马柯帆, 肖立权. 一种加速FPGA布线的不可满足子式求解算法[J]. 电子学报, 2021, 49(6): 1210-1216.
[2]	牛当当, 吕帅, 王金艳, 刘斌. 基于MACR和CAL启发式的求差知识编译算法[J]. 电子学报, 2020, 48(2): 285-290.
[3]	牛当当, 吕帅, 王金艳. 基于MOVR启发式的求差知识编译算法[J]. 电子学报, 2019, 47(11): 2299-2303.
[4]	牛当当, 刘磊, 吕帅. EPCCL理论的并行知识编译算法[J]. 电子学报, 2018, 46(3): 537-543.
[5]	曹玉莲, 李文锋, 张煜. 基于拟熵自适应启动局部搜索策略的混合粒子群算法[J]. 电子学报, 2018, 46(1): 110-117.
[6]	王春, 田娜, 纪志成, 王艳. 求解模糊柔性作业车间调度的多目标进化算法[J]. 电子学报, 2017, 45(12): 2909-2916.
[7]	续欣莹, 张扩, 谢珺, 谢刚. 基于互信息下粒子群优化的属性约简算法[J]. 电子学报, 2017, 45(11): 2695-2704.
[8]	叶东毅, 陈昭炯. 最小属性约简问题的一个有效的组合人工蜂群算法[J]. 电子学报, 2015, 43(5): 1014-1020.
[9]	王令赛, 姜淑娟, 张艳梅, 于巧. 基于正交搜索的粒子群优化测试用例生成方法[J]. 电子学报, 2014, 42(12): 2345-2351.
[10]	尹浩, 张长胜, 张斌, 孙若男, 刘婷婷. 一种求解SLA等级感知服务组合问题的多目标离散粒子群优化算法[J]. 电子学报, 2014, 42(10): 1983-1990.
[11]	莫宏伟, 徐立芳. 基于Memetic算法的电路演化设计研究[J]. 电子学报, 2013, 41(5): 1036-1040.
[12]	张雪霞;陈维荣;戴朝华. 带局部搜索的动态多群体自适应差分进化算法及函数优化[J]. 电子学报, 2010, 38(8): 1825-1830.
[13]	刘红;白栋;丁炜;曾志民. 多目标的Internet路由优化控制算法[J]. 电子学报, 2004, 32(2): 306-309.
[14]	孙元凯;刘民;吴澄. 变邻域结构Tabu搜索算法及其在JobShop调度问题上的应用[J]. 电子学报, 2001, 29(5): 622-625.