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 代表原子子公式参与更高层组合。这样生成规模近似线性。

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

从穷举到 DPLL/CDCL

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

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

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

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

SAT 是 NP-complete 问题，最坏情况仍可能困难；这不妨碍成熟求解器解决许多结构化的大型工业实例。复杂度类别说明一般问题的上界困难，不等于每个实例都慢。

UNSAT 也需要解释

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

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

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

cache_requires_database
cache_is_mandatory
database_is_forbidden

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

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