1.2 逻辑等价、范式与 SAT：让机器搜索解

假设一个产品有数据库、缓存、审计和离线模式四个特性，其中存在十几条兼容约束。逐个勾选测试很快失控；把约束化为布尔公式，就能问一个精确问题：是否存在同时满足全部规则的配置？

这就是 SAT（Boolean Satisfiability Problem）的基本形状。

等价变换的工具箱

常用逻辑等价包括：

双重否定      ¬¬p ≡ p
德·摩根律     ¬(p ∧ q) ≡ ¬p ∨ ¬q
              ¬(p ∨ q) ≡ ¬p ∧ ¬q
蕴含消去      p → q ≡ ¬p ∨ q
双条件        p ↔ q ≡ (p → q) ∧ (q → p)
分配律        p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)
              p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
吸收律        p ∨ (p ∧ q) ≡ p
              p ∧ (p ∨ q) ≡ p

每次变换都应替换一个已知等价子公式。只看符号“差不多”很容易把德·摩根律写错：否定穿过括号时，要否定原子命题并交换 ∧ 与 ∨。

NNF、CNF 和 DNF

**否定范式（NNF）**要求只使用 ∧、∨ 和直接作用于原子命题的 ¬。

¬(p → (q ∧ r))
≡ ¬(¬p ∨ (q ∧ r))
≡ p ∧ (¬q ∨ ¬r)

**合取范式（CNF）**是多个子句的合取，每个子句是文字的析取：

(p ∨ ¬q ∨ r) ∧ (¬p ∨ s) ∧ (q ∨ s)

其中 p 或 ¬p 称为文字，括号内称为子句。

**析取范式（DNF）**是多个项的析取，每个项是文字的合取：

(p ∧ q) ∨ (¬p ∧ r)

CNF 适合许多 SAT 求解器输入；DNF 能直观列出使公式为真的若干情形。但范式是结构，不代表表达一定短。

直接分配可能指数膨胀

把：

(a1 ∧ b1) ∨ (a2 ∧ b2) ∨ ...

机械分配成 CNF，子句数可能指数增长。实际 SAT 编码常使用 Tseitin 变换：为子公式引入辅助变量，再添加约束表达它们之间的关系。

例如为：

x ↔ (p ∧ q)

加入 CNF 约束：

(¬x ∨ p) ∧ (¬x ∨ q) ∧ (x ∨ ¬p ∨ ¬q)

再用 x 代表这个子公式参与上层组合。对固定元数的联结词，每个语法节点只添加常数条子句，所以编码规模随原公式规模线性增长。还必须断言代表整个公式的根变量为真，否则只定义子公式关系，并没有要求原公式成立。

若原公式就是 p ∧ q，上面三条子句还需加单元子句 (x)。不加时，p=F, q=F, x=F 也满足三条定义子句，却不满足原公式。固定原变量后，正确编码应当“存在辅助变量使新公式成立，当且仅当原公式成立”。

Tseitin 结果通常强调与原公式等可满足：原公式有解，当且仅当扩展了辅助变量的新公式有解。加入辅助变量后，不应不加说明地把两个公式称为在完全相同变量集合上的逐赋值等价。

把产品配置编码成子句

定义：

d: 启用数据库
c: 启用缓存
a: 启用审计
o: 启用离线模式

规则：

1. 缓存需要数据库；
2. 启用数据库时必须审计；
3. 离线模式不能使用数据库；
4. 至少启用缓存或离线模式。

翻译：

c → d          ≡ ¬c ∨ d
d → a          ≡ ¬d ∨ a
o → ¬d         ≡ ¬o ∨ ¬d
c ∨ o

合并后已经是 CNF：

(¬c ∨ d) ∧ (¬d ∨ a) ∧ (¬o ∨ ¬d) ∧ (c ∨ o)

一个满足赋值是：

o=T, d=F, c=F, a=F

另一个是：

c=T, d=T, a=T, o=F

SAT 求解器找到一个模型只证明“至少有一种合法配置”，不证明规则符合产品真实意图。编码错误仍会得到非常高效的错误答案。

这个四变量例子可用 Python 3 标准库穷举，元组顺序固定为 (d, c, a, o)：

from itertools import product

def valid(d, c, a, o):
    return ((not c or d) and (not d or a)
            and (not o or not d) and (c or o))

models = [bits for bits in product([False, True], repeat=4) if valid(*bits)]
print(len(models))
print(models)
# 3
# [(False, False, False, True), (False, False, True, True),
#  (True, True, True, False)]

共三个模型。前两个只在离线时是否开启审计上不同，因为规则没有禁止离线审计；若产品本意不同，应该补规则，不能责怪求解器太听话。这里只演示有限枚举，没有实现 DPLL/CDCL。

从穷举到 DPLL/CDCL

含 n 个变量的真值表有 2^n 行。直接穷举适合教学和小公式，不能支撑大规模约束。

现代 SAT 求解的核心思路可以分层理解：

1. 选择一个尚未赋值的变量进行决策；
2. 用单元传播推导被迫的赋值；
3. 若产生冲突，回溯并尝试其他选择；
4. CDCL 求解器还会从冲突中学习新子句，并跳回相关决策层；
5. 重启和启发式继续引导搜索。

例如子句 (p) 只有一个未定文字时，p 必须为真；随后 (¬p ∨ q) 又迫使 q 为真。这种传播能在不枚举全部赋值的情况下迅速收缩搜索空间。

SAT 是 NP-complete：候选赋值可在多项式时间内验证，且每个 NP 问题都能多项式归约到 SAT。这不等于证明所有算法都必须用指数时间；若 SAT 有多项式时间算法，就会有 P=NP。最坏情形困难与许多结构化工业实例能有效求解并不矛盾。

UNSAT 也需要解释

若公式不可满足，工程人员最关心“哪几条规则冲突”。求解器或上层工具可返回 unsat core：一组已经足以造成不可满足的约束。

规则 A：c → d
规则 B：c
规则 C：¬d

三者不能同时成立。给约束稳定命名，能把 core 映射回需求文档：

cache_requires_database
cache_is_mandatory
database_is_forbidden

这比报告“公式不可满足”更有行动价值。注意 unsat core 不一定是最小冲突集合，具体保证取决于工具。

还要区分“删掉任意一条就不再冲突”的包含极小核心，与“条数最少”的最小基数核心；前者不保证后者。超时或 unknown 都不是 UNSAT。SAT 模型可代回原约束检查；需要独立核验 UNSAT 时，应确认工具支持相应证明输出与检查。Z3 的模型、核心和证明接口见作者的 Programming Z3。

SAT、SMT 和约束求解的边界

SAT 变量取布尔值。若规则涉及整数、数组、位向量、字符串或线性实数，可以使用 SMT 求解器，在布尔结构之外接入相应理论。

replicas >= 3
replicas <= available_nodes
region != backup_region

不要为了使用 SAT 手工把所有数值都拆成大量布尔位，除非你了解编码规模和所需语义。选择工具时先看领域约束。

完成检查

为一个三节点部署写出至少六条规则：主节点唯一、至少一个副本、同故障域限制、维护模式限制。然后：

1. 转成 CNF；
2. 找到两个满足赋值；
3. 加一条使其不可满足的规则；
4. 标出一个冲突核心；
5. 说明哪些约束若涉及数量，更适合 SMT 而不是纯 SAT。

参考资料

• SAT Competition
• SMT-LIB Standard