基于扩展规则的若干SAT问题研究

论文摘要

从二十世纪五十年代开始,自动推理就成为了计算机科学的一个核心研究领域,而可满足性SAT （Satisfiability）问题是自动推理最重要的问题之一。基于扩展规则的方法是由林海等人于2003年提出的一种可用于求解SAT问题的方法,发表于人工智能领域的国际知名期刊Journal of Automated Reasoning。此方法一经提出,即得到包括欧美等地的众多学者的关注。基于扩展规则的方法不同于传统的基于归结的方法,对于互补因子高的子句集,具有明显的优势。求解SAT问题的方法被广泛应用于计算机科学的很多领域,包括定理机器证明、机器视觉、数据库等。很多NP问题,如：图染色问题、约束满足问题等,都可以转化成SAT问题求解。关于SAT问题的国际学术会议International Conference on Theory and Applications of Satisfiability Testing,每年举行一次,并且每两届会议举行一次SAT求解器竞赛。关于SAT问题的研究主要集中在提高SAT求解方法的效率上。本文的工作主要是研究如何将传统的归结方法与基于扩展规则的方法相结合以提高SAT求解方法的效率,以及将基于扩展规则的方法应用到模型计数（#SAT）问题的求解中,设计出高效的算法：（1）利用DPLL规则对基于扩展规则方法进行优化。减小待求解SAT问题的规模,将待求解SAT问题分解为一系列规模较小的问题进行求解。并提出MOAMD策略,对原子的排列顺序进行优化。设计出应用DPLL规则和MOAMD策略的算法CIER,实验结果显示,CIER算法保留了基于扩展规则方法在互补因子较高的SAT问题求解方面高效的特点,同时相比于IER算法,在不增加空间复杂性的前提下,时间效率上有1-2个数量级的提高。（2）提出基于碰集的SAT算法,此类算法不依赖于互补因子的高低。以扩展规则为理论基础,将求解子句集的可满足性问题,转化为判断子句集是否存在不包含互补文字的碰集的问题。并根据这个结论,提出基于碰集的SAT求解算法CBHST和RNHST。本文选择了具有代表性的基于归结的算法DR与算法CBHST和RNHST进行了实验比较,两者相对于基于归结的算法DR都有1个数量级以上的效率提升。当子句长度较大的时候,RNHST的搜索树高度较低,时间效率优于CBHST。当子句长度较小的时候,CBHST的搜索树中易出现剪枝,时间效率优于RNHST。对于布尔代数式形式的SAT问题,本文提出了算法SSBF。这个算法不需要将布尔代数形式的SAT问题转换成子句集的形式求解,可以直接用布尔代数进行计算,所以适用于布尔代数式形式的SAT问题。实验显示,该算法在相同参数下与RNHST算法的时间效率处于同一数量级。（3）将上述的基于碰集的方法与基于扩展规则的方法相结合,用于#SAT问题的求解。通过对扩展规则的研究发现,子句集所扩展不出的每一个极大项都对应这个子句集的一个模型,而且这个模型恰好是子句集的碰集所能扩展出的极大项。因此,当子句的长度较短,子句数较多的时候,可以先把子句集转化为一个规模较小的极小碰集的集合,然后使用基于扩展规则的方法对这个极小碰集的集合进行模型计数。依据这个思想,提出了可以精确进行模型计数的间接使用扩展规则方法的模型计数算法MCEHST。本文选择了同样可以精确进行模型计数的基于归结方法的算法CDP和基于扩展规则的算法CER与算法MCEHST进行实验比较。实验结果显示,当子句的长度较短,子句数较多的时候,这个模型计数算法的时间效率要高于模型计数算法CDP和CER,并且当子句数达到一定数量的时候,该算法所消耗时间的增长速度要小于CDP和CER。MCEHST算法适用于子句集形式的#SAT问题,对于布尔代数式形式的#SAT问题,本文提出了MCBE算法。MCBE算法与MCEHST具有类似的特点,当布尔代数式中项的长度较短且数量较大时,时间效率很高。因为MCBE算法直接应用布尔代数进行计算,所以更适合布尔代数式形式的#SAT问题求解。

论文目录

• 提要
• 摘要
• Abstract
• 第1章 绪论
• 1.1 自动推理
• 1.1.1 自动推理的发展
• 1.1.2 自动推理的证明方法
• 1.1.2.1 基于归结的方法
• 1.1.2.2 表推演方法
• 1.1.2.3 Davis-Putnam过程
• 1.1.2.4 扩展规则方法
• 1.1.3 推理系统
• 1.2 可满足性问题
• 1.2.1 可满足性问题的重要性
• 1.2.2 可满足性问题的求解方法
• 1.3 本文的工作
• 第2章 基于分裂规则和扩展规则的SAT问题求解算法
• 2.1 扩展规则
• 2.2 基于扩展规则的SAT问题求解算法
• 2.3 基于分裂规则和扩展规则的SAT问题求解算法
• 2.3.1 使用DPLL规则优化ER算法
• 2.3.2 MOAMD（Maximum Occurrences and Maximum Difference）策略
• 2.4 ER、IER、CIER的实验比较
• 2.5 本章小结
• 第3章 基于碰集的可满足性算法
• 3.1 引言
• 3.2 用扩展规则将SAT问题转化为HS问题
• 3.3 基于碰集的SAT算法
• 3.3.1 CBHST （Complementary Binary Hitting Set Tree）
• 3.3.2 RNHST（Revised NewHS-Tree）
• 3.3.3 SSBF（Solving SAT problem with Boolean Formulas）
• 3.4 实验结果
• 3.5 本章小结
• 第4章 间接使用扩展规则求解#SAT问题
• 4.1 引言
• 4.2 子句集的碰集与模型之间的关系
• 4.3 间接应用扩展规则的#SAT算法
• 4.3.1 MCEHST（Model Counting with Extension Rule and Hitting Set Tree）
• 4.3.2 MCBE（Model Counting with Boolean Algebra and Extension Rule）
• 4.4 实验结果与比较
• 4.5 本章小结
• 第5章 总结与展望
• 参考文献
• 作者读博士期间完成的论文与参加的科研项目 论文:
• 致谢