命题逻辑¶
在高中, 我们学过有关真命题、假命题与逆否命题的内容. 例如, 对于任意一个命题 \(A\), 我们知道"\(A\) 或非 \(A\)"一定是一个真命题, 而"\(A\) 与非 \(A\)"一定是一个假命题.
这篇教程会先将上面的直觉形式化, 然后介绍判定命题逻辑中公式真假的算法.
命题逻辑中的公式¶
命题逻辑中有以下几种公式：
- 与：\(A\land B\). 当且仅当 \(A\) 和 \(B\) 都为真的时候, \(A\land B\) 才是真的.
- 或：\(A\lor B\). 当且仅当 \(A\) 和 \(B\) 至少一个为真时, \(A\lor B\) 才是真的.
- 非：\(\neg A\). 当且仅当 \(A\) 为假时, \(B\) 为真.
可以将它们与 C 系语言中的 &&, || 与 ! 相比较.
这里的 \(A\) 和 \(B\) 是两个变量, 它们只能取"真"和"假"两个值. 有时我们将这种变量叫做命题变量. 我们把 \(A\) 和 \(\neg A\) 统称为文字 (literal).
你可能会觉得 \(\land\) 和 \(\lor\) 长得很像, 记不住哪个是哪个. 可以这样理解：\(\land\) 和交集的符号 \(\cap\) 开口方向一样, 因为 \(A\land B\) 为真的情况是 \(A\) 为真和 \(B\) 为真情况的交集. 同理, \(\lor\) 和并集的符号 \(\cup\) 开口方向一样, 因为 \(A\lor B\) 为真的情况是 \(A\) 为真和 \(B\) 为真情况的并集.
对上面的三种公式, 我们各用了两句话描述. 第一句话是语法, 表明它长的样子; 第二句话是语义, 表明它的意思. 语法和语义的区别在编译器与编程语言相关的其他领域也很重要.
除了与、或、非之外, 经常出现的还有下面两种公式：
- 实质蕴涵 (implies): \(A\rightarrow B\). 等价于 \(\neg A\lor B\).
- 双向蕴涵 (bi-implies): \(A\leftrightarrow B\). 等价于 \((A\rightarrow B)\land (B\rightarrow A)\).
一般而言, 运算优先级是非 > 与 > 或 > 蕴涵 > 双向蕴涵. 例如, \(A\land B\lor C\) 实际上意为 \((A\land B)\lor C\). "与"结合得比"或"更紧密, 这和 C 的运算符优先级是一致的.
语言和元语言¶
你可能会觉得奇怪："双向蕴涵"和"等价"有什么区别呢? "实质蕴涵"为什么要加上"实质"两个字呢?
双向蕴涵会产生一个命题逻辑中的公式, 而等价则是在描述公式之间的关系. 例如, \((A\leftrightarrow B) \land C\) 是合法的公式, 但"(\(A\) 等价于 \(B\)) 且 \(C\)" 显然不是合理的描述.
不过, 它们之前确实有联系：如果公式 \(P\) 等价于公式 \(Q\), 那么公式 \(P\leftrightarrow Q\) 恒为真.
这个结论从直觉上应当很好理解. 不过要真正证明这一点的话, 我们还需要严格化等价的定义, 同时介绍与"实质蕴涵"有所不同的蕴涵.
解释¶
我们先介绍解释 (interpretation) 的概念. Wikipedia 中这样介绍：
解释是一种将形式语言中的符号赋予意义的行为.
具体来说, 命题逻辑就是一种形式语言, 其中的符号则指的是各个命题变量. 赋予意义, 在这里指的是为它们指定真假.
例如, 公式 \(A\land B\) 有 4 种解释（以 1 代表真, 0 代表假）：
- \(\{ A = 1, B = 1 \}\);
- \(\{ A = 1, B = 0 \}\);
- \(\{ A = 0, B = 1 \}\);
- \(\{ A = 0, B = 0 \}\).
只有在解释 \(\{ A = 1, B = 1 \}\) 下, 公式 \(A\land B\) 才是真的.
对于一个命题逻辑中的公式 \(P\):
- 如果所有的解释都使得它为真, 那么我们称 \(P\) 为永真式 (tautology, 或者 valid);
- 如果没有任何一个解释能使得它为真, 那么 \(P\) 是不可满足的 (unsatisfiable);
- 如果至少有一个解释使得它为真, 那么 \(P\) 是可满足的 (satisfiable).
例如, 上述的 \(A\land B\) 是可满足的, 因为我们已经找到了一个解释使它为真. 在文章开头举的例子中, 不论 \(A\) 的真值是什么, \(A\land \neg A\) 恒为假, 这说明 \(A\land \neg A\) 是不可满足的. 同样地, \(A\lor \neg A\) 恒为真, 说明它是永真的.
判断一个命题公式是否可满足, 具有很广泛的应用场景. 我们将这个问题称作 SAT (satisfiability). 例如, 如果 \(P\) 是不可满足的, 那么 \(\neg P\) 是永真的, 这可以视作对 \(\neg P\) 的证明. 在编译器中, 它可以用来指导窥孔优化、寄存器分配等问题. SAT (以及基于它的 SMT) 求解器的一种应用方式可以参看本站的另一篇教程: CEGIS.
SAT 问题是 NP-完全的, 意思是: 就我们目前所知而言, 公式的可满足性最坏情况下需要指数级的时间才能判断. 然而, 在实际运用中, 我们确实有高效的判断方法, 可以解决含有数万个变量的问题. 较为基础的 DPLL 算法将在本文的后半部分讲到, 而 本站的教程 SAT 求解器 介绍了对它的更多优化.
如果公式 \(A\) 蕴涵 (entail) \(B\), 那么使得 \(B\) 为真的每个解释, 也都会使得 \(A\) 为真. 如果公式 \(A\) 等价于 \(B\), 那么 \(A\) 蕴涵 \(B\), 而且 \(B\) 蕴涵 \(A\).
容易发现实质蕴涵和蕴涵的关系, 正相当于双向蕴含和等价的关系: \(A\rightarrow B\) 恒为真, 当且仅当 \(A\) 实质蕴涵 \(B\). 为了区别二者, 我们才加上了"实质"二字.
合取范式 (CNF)¶
接下来我们介绍合取范式 (conjuction normal form, CNF). 这个名字听起来很吓人, 不过其实它只是在使用生僻词汇而已. "合取"其实就是"与"的意思, 相对应地"析取" (disjunction) 则是"或"的意思. 范式则意为"标准型".
所以 CNF 是指用"与"连接的一些括号, 其中每个括号都是"或"连接的文字, 形似这样: $$ (A_1\lor \neg A_2\lor \dots A_n) \land (\neg B_1\lor B_2\lor \dots \neg B_m) \land \dots $$
其中的每个括号都被称作一个子句 (clause), 而这些子句必须全部为真, 原本的公式才会为真. 不过在子句内部, 只要有一个变量是真的, 整个子句就是真的.
有的时候我们会这样写 CNF 的子句: $$ \lbrace A_1, \neg A_2, \dots, A_n\rbrace $$ 只要记住它们是由"或"连接的就好.
每个命题逻辑的公式都可以转化为 CNF, 并且这样的转化是可以在线性时间内进行的. 具体的算法请见本站的另外一篇教程QF_BV理论, 或搜索"Tseitin 算法". 许多解决 SAT 问题的算法都要求命题公式是 CNF 形态, 例如 DPLL 算法 (Davis-Putnam-Logeman-Loveland). 我们将在下一节中介绍它.
DPLL 算法¶
判断 CNF 公式 \(x\) 的可满足性, 意思是判断是否存在一个解释, 使得 \(x\) 为真. 换句话说, 我们要寻找一个对变量的赋值, 使得 \(x\) 的所有子句都为真.
首先, 我们可以删除那些已经恒定为真的子句, 因为这不会对 \(x\) 的真值产生影响. 我们可以检查是否有某个 \(A\) 满足 \(A\) 和 \(\neg A\) 在这个子句中同时出现. 这是因为子句中的文字都是以"或"连接的, 而 \(A\lor \neg A\) 一定是真的. 同时, 如果有一些文字只出现了一次, 我们完全可以删除它所在的那个子句. 因为我们总是可以把它赋值成真, 使得那个子句恒定为真.
接下来, 检查那些只有一个文字的子句, 称作单元子句. 既然我们想让 \(x\) 为真, 这个子句也必须为真, 所以这个文字必须是真的. 由此, 我们可以确定这个子句对应变量的真值. 例如, 当我们碰到单元子句 \(\lbrace A\rbrace\) 时, 我们知道 \(A\) 为真; 当我们碰到 \(\lbrace \neg A\rbrace\) 时, 我们知道 \(A\) 为假.
假设上一步中, 我们得到了变量 \(A\) 的真值. 如果 \(A\) 是真的, 现在所有含有 \(A\) 的子句都为真了, 它们可以被删去. 我们还知道 \(\neg A\) 不可能为真, 所以可以将 \(\neg A\) 从子句中删除. 同理, 我们可以处理 \(A\) 为假时的情况.
这两步称作单元传播 (unit propagation), 是 SAT 求解时执行次数最多的部分.
这一步可能会产生更多的单元子句, 此时我们重复单元传播, 直到出现以下两种情况之一:
- 产生了一个空的子句. 空的子句永远为假 (想一想, 为什么?), 所以这时 \(x\) 不可满足.
- 所有子句都有至少两个文字. 这时, 我们任意地选择一个变量, 然后将它分为真、假两种情况, 递归地执行 DPLL 算法. 只要有一种情况可以满足, \(x\) 就可以满足.
这就是 DPLL 算法的全貌. 作为总结:
- 删除永真式;
- 执行单元传播;
- 分类讨论, 递归执行 DPLL.