第3章 完备算法(Complete Algorithms)

章节简介

完备算法：当程序运行终止时，能够对SAT问题的满足性做出正确判断的算法。

• 存在量化(Existential Quantification)

  在不改变满足性情况下，对变量进行消除。将复杂问题转化为简单测试。

• 可靠和完备的推理规则(Sound and Complete Inference Rule)

  使用推理规则，直到产生矛盾（空字句）。

• 真值赋值空间中的系统搜索(Systematic Search in the Space of Truth Assignments)

  相较于前两种方法占用空间较少。

知识准备

SAT问题的合取范式形式（CNF）：

简化形式：

重要事实：若，则SAT问题不可满足。

解析(Resolution)/变量消除

若且，通过变量消除推理规则可以导出新子句。

变量消除推理规则：

• 蕴含(Implication)
• 可靠但不完备
• 推理出的子句都是符合SAT系统的，但不是所有符合SAT系统的子句都可以被推出。
• 如果SAT系统是不可满足的，一定可以通过变量消除推理规则得到空字句。这也是证明SAT问题不可满足的主要方式。

约束(Conditioning)/变量赋值

对SAT系统中的变量（文字）进行赋值：

• ，该子句已经满足，从系统中删除该子句。
• ​，该文字对子句已经没有贡献，从子句中删除该文字。

存在量化

存在量化：​，反复执行使得变量减少。

问题（非书中内容）：和均为CNF形式，但不是，在复杂的情况下会产生大量子句。

• DP(Davis-Putnam)算法
• 符号SAT求解

推理规则

• 解析/变量消除推理规则

• Stalmarck算法

  合取三元组：，其中是变量，和是文字，可以是逻辑连词或等价词。

  此时代表了原始公式，通过设定一系列传播规则，期望从推导出矛盾。

• HeerHugo算法：总体来说与Stalmarck算法类似。

搜索算法

变量赋值+搜索回溯

单位解析(Unit Resolution)/单位传播

单位传播：

• 如果存在单位子句()，进行变量赋值：
• 如果存在单位子句()，进行变量赋值：
• 重复进行以上操作

单位传播是以搜索为基础的SAT求解器中一个非常重要的组成部分。

DPLL算法：

• 变量赋值+搜索回溯
• 单位传播

冲突集

推断过程中涉及到的变量设置为冲突集：

经过两次冲突，发现当时，X取真或假均不满足，故直接回溯到A（非时间顺序回溯）。

• 在选择变量赋值时，难以避免选择到与最终冲突无关的变量，用冲突集检查
• 都可以由初始子句进行变量消除得到，如果一开始就有这个子句，搜索过程将被简化，如何得到这个子句？是否还有其他有价值的子句？

其他思考

• First UIP可能会出现重复搜索的情况：但算法依然完备

  

• 冲突驱动子句过多：需要删除

  • 蕴含关系
  • 启发式方法（删除较长的、较旧的、较不活跃的）

• 重启：实验表明重启是有利的，但可能导致算法不完备

  • 冲突次数/赋值变量数量：目前搜索空间过大

总结

• 三类完备算法：

  • 存在量化
  • 逻辑推理
  • 系统搜索

• 现有主流算法：搜索+推理

• 认证(Certifying)：对于不满足的SAT问题，显式推理到一个空子句（以及其他变体）。