基于CDCL求解SAT问题的启发式策略研究

论文摘要

在逻辑问题中,布尔可满足性问题(即SAT问题)一直广受人们的关注。SAT问题是确定以合取范式(CNF)的形式给出的命题逻辑公式是否具有对其变量的一组布尔真值赋值,使得该公式是可满足的,或者证明它不可满足。SAT问题在算法时间复杂度上是首个被证明的NP完全问题。目前,SAT问题是许多领域的研究热点,如定理证明、自动推理、模型检查、电子设计自动化、计算机辅助设计等。因此,有关SAT问题的研究,不仅在理论方面意义重大,而且在实际应用中也有着巨大的价值。不完备算法和完备算法是解决SAT问题的两类主要算法。不完备算法主要基于随机局部搜索的思想,完备算法主要基于回溯搜索的思想。完备算法的优点在于一定能够判定SAT问题的可满足性。目前,最流行的完备算法是CDCL算法,本文则是基于CDCL算法结构展开研究,主要取得了如下研究成果:1.在EVSIDS和ACIDS算法的启发下,提出了一种基于动态奖励的分支启发式算法,也称为DRB算法。每当冲突发生时,DRB算法通过综合考虑变量决策层、冲突层、冲突次数和变量冲突频率进行活性分数更新,从而引导求解器的分支变量决策。2.根据学习子句的LBD值引入了层次差,用于评估LBD值相同的学习子句之间的质量差异。基于此,提出了基于层次差的学习子句删除启发式策略,也称为LDCR策略,从而指导求解器的子句数据库管理。3.将DRB算法和LDCR策略嵌入到Glucose 3.0与MapleLCMDistChronoBT求解器中,得到了6个新的SAT求解器。主要做了两类实验,实验一是基于Glucose 3.0的改进求解器与Glucose 3.0之间的对比实验,选择2015年、2016年和2017年三年的SAT竞赛实例进行测试;实验二是基于2018年冠军求解器MapleLCMDistChronoBT的改进求解器与MapleLCMDistChronoBT之间的对比实验,选择2018年的SAT竞赛实例进行测试。将改进求解器的测试结果与原来的求解器进行对比分析,实验结果表明改进求解器的性能均高于原来的求解器。因此,本文提出的两种新的启发式策略可以有效改进已有的CDCL算法框架,进而提升求解器的性能。

论文目录

摘要

Abstract

第1章绪论

1.1 研究背景及研究意义

1.2 SAT问题研究现状

1.3 本文研究内容及结构安排

第2章预备知识

2.1 SAT问题基础知识

2.1.1 算法复杂度

2.1.2 P、NP、NPC问题

2.1.3 SAT问题基本定义

2.2 DPLL算法

2.2.1 DPLL算法基本思想

2.2.2 DPLL算法求解过程

2.2.3 DPLL算法优劣势

2.3 CDCL算法

2.3.1 CDCL算法求解过程

2.3.2 CDCL算法关键技术

2.4 本章小结

第3章基于动态奖励的分支启发式策略

3.1 已有分支启发式算法

3.1.1 VSIDS算法

3.1.2 EVSIDS算法

3.1.3 ACIDS算法

3.2 基于动态奖励的分支启发式算法

3.2.1 DRB算法

3.2.2 示例

3.3 本章小结

第4章基于层次差的学习子句删除启发式策略

4.1 已有学习子句删除策略

4.1.1 基于子句长度与子句活性的删除策略

4.1.2 基于LBD的删除策略

4.2 基于层次差的学习子句删除策略

4.3 本章小结

第5章实验结果及评估

5.1 实验设置

5.1.1 实验一基于Glucose3.0 的改进求解器

5.1.2 实验二基于MapleLCMDistChronoBT的改进求解器

5.2 测试结果比较

5.2.1 实验一结果比较

5.2.2 实验二结果比较

5.3 本章小结

第6章总结与展望

6.1 总结

6.2 展望

致谢

参考文献

攻读硕士学位期间发表的论文及参与的科研工作

1.硕士期间发表的论文

2.硕士期间参与的科研项目

文章来源

类型: 硕士论文

作者: 陈秀兰

导师: 徐扬

关键词: 问题,算法,分支启发式策略,学习子句删除启发式策略,策略,求解器

来源: 西南交通大学

年度: 2019

分类: 基础科学

专业: 数学

单位: 西南交通大学

基金: 国家自然科学基金项目(61673320)

分类号: O141

DOI: 10.27414/d.cnki.gxnju.2019.000820

总页数: 68

文件大小: 911K

下载量: 28

基于CDCL求解SAT问题的启发式策略研究

论文摘要

论文目录

文章来源

相关论文文献

猜你喜欢