基于分支策略与距离比删除策略的SAT问题求解算法研究

摘要

自然科学与社会科学中的许多问题均可转化成布尔可满足问题(Satisfiability Problem，SAT)，并且SAT问题也是计算机以及人工智能等科学领域的核心问题之一。因此，随着计算机科学、智能信息的快速发展，为解决各种实际问题，研究SAT问题以及其求解具有深刻意义。　　SAT问题中的算法主要分为完备算法和不完备算法，本文主要研究的是完备算法中的CDCL(Conflict Drive Clause Learning)算法。在CDCL算法基本求解过程中，分支过程以及子句学习过程是非常重要的两个阶段，对求解效率和求解速度都有很大的影响。而现在多数的改进算法在分支过程均未考虑整个算法过程中的其他阶段，所以求解结果未能达到最优。基于此，本文考虑冲突分析阶段对分支过程影响的同时，结合回溯以及重启两个阶段产生的影响，提出加权决策变量决策层的改进分支策略。新策略设计了新的变量得分函数，使其具有在分支过程能够更快的挑选出决策变量的优势，因此能减少后续冲突和重启次数，最终减少求解时间。对由新策略形成新的求解器进行试验测试，实验结果表明新分支策略具有优化的效果。另外，现在多数算法在子句学习过程评估学习子句质量均是将学习子句的长度、活跃度或者文字块距离(literal block distance,LBD)值作为评价标准，但少有考虑制定新的删除标准，基于此，本文考虑平衡LBD的值，提出文字块紧密度(literal block close,LBC)的概念，并将其与学习子句活跃度结合，形成基于距离比的学习子句删除策略。新策略能更有效地删除利用率低的学习子句，由此加强求解器的求解能力，增加求解例子个数，减少求解时间。对此策略形成新的求解器进行实验测试，结果表明新策略的求解能力更强。本文的主要研究工作如下：　　1、通过分析冲突、回溯和重启过程，根据变量作为决策变量的次数以及对其决策层加权，提出了新的变量得分计算函数方法，并提出了加权决策变量决策层(DVT)的策略，将DVT策略嵌入CDCL算法中并形成Glucose4.1+DVT求解器。采用SATLIB中的基准例以及2019年、2018年和2017年国际SAT竞赛MainTrack组中的测试例进行实验测试，结果表明新求解器成功求解的平均总时长比原求解器缩短10%，成功求解出的测试例总个数相比原版求解器增加6个。　　2、由于冲突子句学习过程中会产生大量的学习子句，基于平衡子句LBD值的思想，提出文字块紧密度的概念以及距离比的学习子句删除(LBDR)策略，将此策略加入CDCL算法中，形成Glucose4.1+LBDR求解器。采用SATLIB中的基准例以及2019年、2018年和2017年国际SAT竞赛MainTrack组中的测试例进行实验测试，结果表明新求解器成功求解时间比原求解器缩短12.5%，成功求解出测试例的总个数相比原版求解器增加14个。

目录

声明

第一章 绪论

1.1 研究的背景和意义

1.2 SAT问题的国内外研究现状

1.3 本文的研究内容结构

第二章 基础知识

2.1 基本概念

2.2 DPLL算法

2.3 CDCL算法

2.3 本章小结

第三章 分支与删除策略

3.1 分支策略

3.1.1 JW策略

3.1.2 DLIS策略

3.1.3 VSIDS策略

3.1.4 CHB策略

3.1.5 LRB策略

3.2 删除策略

3.2.1静态删除策略

3.2.2动态删除策略

3.3 本章小结

第四章 基于加权决策变量决策层的分支策略

4.1 决策变量的选择

4.2 变量的得分与赋值

4.3 基于加权决策变量决策层的分支策略

4.4 本章小结

第五章 基于距离比的学习子句删除策略

5.1 学习子句的删除

5.2 衡量学习子句价值的删除标准

5.3 基于距离比的学习子句删除策略

5.4本章小结

第六章 实验结果与分析

6.1 实验的设置

1. 实验的求解器

2. 实验的测试例

3. 实验的环境配置

4. 测试时间和方法

6.2 实验的测试结果

测试组一

测试组二

测试组三

总结与展望

总结

展望

致谢

参考文献

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

一、硕士期间发表以及完成的论文

二、硕士期间参与的科研项目