CDCL SAT求解器中的分支变量启发式算法研究

摘要

命题逻辑公式的可满足性问题（即SAT问题）是人工智能和计算机科学领域的核心问题之一。1971年Stephen.Cook从算法时间复杂度的角度证明了SAT问题是NP完全问题，而NP完全问题在七大数学难题中排在首位，可见SAT问题是一类非常困难的问题。由于SAT问题在约束可满足问题、数理逻辑、自动推理、软件及硬件验证等领域具有广泛的应用，因此研究SAT问题的求解具有重要的理论价值和应用前景。
　　目前求解SAT问题的算法大致可归为两类:一类是完备的求解算法;一类是不完备的求解算法。基于DPLL算法的CDCL(Conflict Derive Clause Learning)算法是目前比较流行的完备算法，由该算法设计的求解器(CDCLSAT求解器)的求解过程主要分为三大阶段，分别是分支变量选择阶段、布尔约束传播阶段和冲突分析及回溯阶段。其中，变量选择阶段的分支变量启发式算法可归结为两类:第一类是没有与冲突分析过程相结合的启发式算法，比如JW算法(Jeroslow-Wang)、DLIS(Dynamic LargerIndependent Sum)算法等;第二类是与冲突分析过程相结合的启发式算法，比如VSIDS(Variable State Independent Decaying Sum)算法、CHB(Conflict History-based BranchingHeuristic)算法、LRB（Learning Rate Branching）算法等。由于第一类分支变量启发式算法计算代价大，第二类分支变量启发式算法未能很好地利用子句固有的信息以及未体现出学习子句中变量的不同。故为了尽可能减少这些算法的不足以及选出更好的分支变量，本文以经典的VSIDS算法为基本框架设计了基于奖励的分支变量启发式算法，并用该算法代替MiniSat求解器中的分支变量启发式算法，得到新的求解器一Modified-MiniSat求解器。
　　本文就新算法的提出主要做了以下四方面的工作:
　　1.对于一般的SAT问题，短予句较长子句更难被满足，依据子句的长度赋予每个子句权重，进而给出变量在子旬以及子句集中的权重的定义。并用变量在子句集中的权重刻画变量的活性，从而尽可能准确地反映变量在子句集中的活跃度。
　　2.设计了与决策层有关的奖励函数。在问题求解过程中，当学习子句添加到子句集时，根据学习子句中变量所在决策层的不同，奖励变量，以便增大学习子句中的变量活性。
　　3.基于上述两方面的工作，给出了基于奖励的分支变量启发式算法，并用该算法代替MiniSat求解器中的分支变量启发式算法，设计了相应的求解器—Modified-MiniSat求解器。
　　4.选择2013 SAT竞赛以及2016年SAT竞赛例作为测试例，对Modified-MiniSat求解器和MiniSat求解器做对比测试，通过分析实验结果得知Modified-MiniSat求解器有一定的优势，从而说明了改进后的分支变量启发式算法的有效性。

目录

声明

摘要

第1章 绪论

1．1 SAT问题的研究背景及意义

1．2 SAT问题的研究现状

1．3 本文研究的内容和结构安排

第2章 预备知识

2．1 相关定义

2．2 完备算法

2．2．1 DPLL算法

2．2．2 CDCL算法

2．3 本章小结

第3章 两类分支变量启发式算法

3．1 第一类分支变量启发式算法

3．1．1 JW(Jeroslow-Wang)算法

3．1．2 DLIS(Dynamic Larger Independent Sum)算法

3．2 第二类分支变量启发式算法

3．2．1 VSIDS算法

3．2．2 CHB(Conflict History-based Branching Heuristic)算法

3．2．3 LRB(Leaming Rate Branching)算法

3．3 本章小结

第4章 基于奖励的分支变量启发式算法

4．1 刻画变量的初始活性

4．2 引入奖励函数

4．3 基于奖励的分支变量启发式算法

4．4 本章小结

第5章 算法评估

5．1 理论分析

5．2 实验分析

5．3 本章小结

总结与展望

致谢

参考文献

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

附录