检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:李壮[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[自动化与计算机技术—控制理论与控制工程]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.179