基于重启策略的学习子句优化方法

doi:10.12068/j.issn.1005-3026.2020.01.008

东北大学学报:自然科学版 ›› 2020, Vol. 41 ›› Issue (1): 44-48.DOI: 10.12068/j.issn.1005-3026.2020.01.008

基于重启策略的学习子句优化方法

李壮，刘磊，张桐搏，吕帅

(吉林大学计算机科学与技术学院，吉林长春130012)

收稿日期:2019-03-19 修回日期:2019-03-19 出版日期:2020-01-15 发布日期:2020-02-01
通讯作者: 李壮
作者简介:李壮(1988-)，男，吉林白城人，吉林大学博士研究生; 刘磊(1960-)，男，吉林长春人，吉林大学教授，博士生导师.
基金资助:
国家重点研发计划项目(2017YFB1003103); 国家自然科学基金资助项目(61300049，61763003); 吉林省科技发展计划项目(20180101053JC，20190201193JC).

Learnt Clauses Optimize Method Based on Restart Strategy

LI Zhuang， LIU Lei， ZHANG Tong-bo， LYU Shuai

College of Computer Science and Technology， Jilin University， Changchun 130012， China.

Received:2019-03-19 Revised:2019-03-19 Online:2020-01-15 Published:2020-02-01
Contact: LYU Shuai
About author:-
Supported by:
-

摘要/Abstract

摘要： 以学习子句数据库优化为背景，在原MiniSAT求解器的基础上提出了一种新的学习子句的优化方法.该方法基于博弈论的思想，在若干次重启后，根据当前求解器的实时反馈信息改进MiniSAT原有的增长参数，尽可能靠近学习数据库中子句存储量的均衡点，从而使学习库的存储量尽可能达到Pareto最优.实验表明:所提的优化方法是有效的，并在随机SAT问题上胜过现有优化方法.该方法既不会因为学习数据库的子句过多而影响单元传播速度，也不会因为学习数据库中的子句过少而破坏学习的整体性.

关键词: DPLL, 子句学习, 学习子句数据库, MiniSAT求解器, Pareto最优

Abstract: With the background of optimization of the learnt clauses database， a new optimization method for learnt clauses based on the original MiniSAT solver was proposed. Based on game theory， this method adjusts the growth parameters after several restarts on the basis of the real-time feedback of the current solver， in order to be as close as possible to the balance point of clauses in the learnt clauses database. This makes the storage capacity of the learnt clause database reach the Pareto optimality as much as possible. Experiments showed that the proposed method is effective and outperforms existing optimization methods in random SAT problems. This method neither affects the speed of unit propagation because of too many clauses in the learnt clause database， nor destroys the integrity of learning because of too few clauses in the learnt clause database.

Key words: DPLL(Davis-Putnam-Logemann-Loveland), clause learning, learnt clauses database, MiniSAT solver, Pareto optimality

中图分类号:

TP181

李壮，刘磊，张桐搏，吕帅. 基于重启策略的学习子句优化方法[J]. 东北大学学报:自然科学版, 2020, 41(1): 44-48.

LI Zhuang， LIU Lei， ZHANG Tong-bo， LYU Shuai. Learnt Clauses Optimize Method Based on Restart Strategy[J]. Journal of Northeastern University Natural Science, 2020, 41(1): 44-48.

参考文献

[1]Beame P，Kautz H，Sabharwal A.Towards understanding and harnessing the potential of clause learning［J］.Journal of Artificial Intelligence Research，2004，22:319-351.
[2]Silva J，Sakallah K.Grasp—a new search algorithm for satisfiability［C］//IEEE/ACM International Conference on Computer-aided Design(CAD 1996).Ann Arbor，1996:220-227.
[3]Audemard G，Simon L.Predicting learnt clauses quality in modern SAT solvers［C］//International Joint Conference on Artificial Intelligence(IJCAI 2009).Pasadena，2009:399-404.
[4]Luo M，Li C，Xiao F，et al.An effective learnt clause minimization approach for CDCL SAT solvers［C］//Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence(IJCAI 2017).Melbourne，2017:703-711.
[5]Moskewicz M，Madigan C，Zhao Y，et al.Chaff:engineering an efficient SAT solver［C］//Proceedings of Design Automation Conference(DAC 2001).Las Vegas，2001:530-535.
[6]Audemard G，Lagniez J M，Mazure B，et al.On freezing and reactivating learnt clauses［C］//Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing(SAT 2011).Ann Arbor，2011:188-200.
[7]Hamadi Y，Jabbour S，Sas L.What we can learn from conflicts in propositional satisfiability［J］.Annals of Operations Research，2016，240(1):13-37.
[8]Luo M，Xiao F，Li C，et al.Maple_CM，Maple_CM_Dist，Maple_CM_ordUIP and Maple_CM_ordUIP+ in the SAT competition 2018［C］//Proceedings of SAT Competition 2018—Solver and Benchmark Descriptions.Oxford，2018:44-46.
[9]Atserias A，Fichte J K，Thurley M.Clause-learning algorithms with many restarts and bounded-width resolution［J］.Journal of Artificial Intelligence Research，2011，40:353-373.
[10]Dixon H E，Ginsberg M L，Parkes A J.Generalizing boolean satisfiability I:background and existing work［J］.Journal of Artificial Intelligence Research，2004，21:193-243.
[15]关守平，房少纯.一种新型的区间-粒子群优化算法［J］.东北大学学报(自然科学版)，2012，33(10):1381-1384.(Guan Shou-ping，Fang Shao-chun.A new particle swarm optimization algorithm［J］.Journal of Northeastern University(Natural Science)，2012，33(10):1381-1384.)

基于重启策略的学习子句优化方法

Learnt Clauses Optimize Method Based on Restart Strategy

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 3

编辑推荐

Metrics

本文评价

[1]	王兴伟;赵焕彦;黄敏;. 一种多粒子群切换决策机制[J]. 东北大学学报(自然科学版), 2010, 31(5): 625-629.
[2]	刘晓霞;谢里阳;陶泽;郝长中;. 柔性作业车间多目标调度优化研究[J]. 东北大学学报(自然科学版), 2008, 29(3): 362-365+382.
[3]	王兴伟;江南;王家林;黄敏;. 一种基于微观经济学的网格资源分配模型[J]. 东北大学学报(自然科学版), 2006, 27(7): 731-734.