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

Learnt Clauses Optimize Method Based on Restart Strategy

作　　者：李壮[1] 刘磊[1] 张桐搏 吕帅[1] LI Zhuang;LIU Lei;ZHANG Tong-bo;LYU Shuai(College of Computer Science and Technology,Jilin University,Changchun 130012,China)

机构地区：[1]吉林大学计算机科学与技术学院

出　　处：《东北大学学报（自然科学版）》2020年第1期44-48,共5页Journal of Northeastern University(Natural Science)

基　　金：国家重点研发计划项目(2017YFB1003103);国家自然科学基金资助项目(61300049,61763003);吉林省科技发展计划项目(20180101053JC,20190201193JC)

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

关 键 词：DPLL 子句学习 学习子句数据库 MiniSAT求解器 PARETO最优 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]