论文摘要
CDCL（Conflict Derive Clause Learning）算法是解决布尔可满足性问题（Satisfiability Problem,SAT）的一种完备算法,CDCL算法求解过程的基本阶段依次为:预处理;分支决策;布尔约束传播（Boolean Constraint Propagate,BCP）;非时序性回溯;随机重启。分支决策是CDCL算法中重要的阶段之一,CDCL算法中的分支策略是VSIDS（Variable State Independent Decaying Sum）策略,基于VSIDS策略,本文提出了基于加权决策层的分支策略,新分支策略可优先满足短子句和优先满足新进学习子句。新分支策略是由初始变量决策策略和冲突变量决策策略构成,初始变量决策策略是初始选择变量时优先选择短子句中的变量进行赋值,从而优先满足短子句,冲突变量决策策略是冲突后选择变量时优先选择新子句中的变量进行赋值,从而优先满足新子句且避免同一搜索空间。将新分支策略嵌入到CDCL算法里,通过实验结果说明可实现算法的优化。本文不仅提出了基于加权决策层的分支策略,而且还提出了基于加权冲突次数的删除策略,子句删除可优化存储空间,删除一些价值较小的子句并保留对冲突影响较大的学习子句,冲突次数是评估学习子句质量的一项重要指标,子句中的变量参与冲突次数越多子句质量越高,删除低质量的学习子句可实现存储空间的优化,将新删除策略嵌入到CDCL算法里,通过实验结果证明可实现算法的优化。主要的研究工作为:1、对于一组子句,长子句中的文字较多,因此对变量赋值时相比短子句,长子句更易于满足,所以基于优先满足短子句的思想,结合子句的长度,设计变量权重的分值函数,给出一种新的初始变量决策策略。2、CDCL算法中,布尔约束传播遇到冲突时是非时序回溯,对于冲突后给予冲突相关变量的鼓励值可以依据变量的冲突层和决策层之间的差值进行馈赠,另外可以优先考虑满足短学习子句,因此结合子句的长度和决策层与冲突层之间的差,构造子句权重的计算函数,提出一种新的冲突变量决策策略。3、结合前面的两部分的内容,构成新的分支策略,并嵌入CDCL算法,形成新的算法。4、每次产生冲突时经冲突分析所学习到的子句会增添到子句库,随着子句数目的增大,存储空间变小,因此为优化存储空间需删减价值较小的学习子句。子句参与冲突次数越多对冲突影响越大,所以基于子句平均冲突次数提出一种新的删除策略,并嵌入CDCL算法,形成新的算法。5、新分支策略与新删除策略分别嵌入CDCL算法并将形成的新算法结合Glucose4.1和求解器MapleLCMDistChronoBT改进为新求解器Glucose4.1+awdl与求解器ChronoBT+awdl、求解器Glucose4.1+dwct与求解器ChronoBT+dwct,以及两新策略共同嵌入CDCL算法并将形成的新算法结合Glucose4.1和求解器MapleLCMDistChronoBT改进为求解器Glucose4.1+awdl+dwct与求解器ChronoBT+awdl+dwct,采用SAT国际竞赛例子进行测试,通过实验结果验证新求解器的有效性。
论文目录
文章来源
类型: 硕士论文
作者: 胡忠雪
导师: 徐扬
关键词: 问题,分支策略,删除策略,决策层,子句长度,学习子句
来源: 西南交通大学
年度: 2019
分类: 基础科学
专业: 数学
单位: 西南交通大学
基金: 西南交通大学唐山研究院项目“程序可信性自动验证技术研究”(批准号:TY2017024),国家自然科学基金项目“基于矛盾体分离的动态自动演绎推理研究”(批准号:61673320)
分类号: O221.1
DOI: 10.27414/d.cnki.gxnju.2019.000807
总页数: 72
文件大小: 3375K
下载量: 12