SAT 问题概览:从求值到搜索

但要让非人类的机器达到小学二年级里计算数学表达式的能力并不简单，我们冻结关于计算机的原理，在已经有现代计算机的基础上，机器要能对表达式求值，首先要完成的是对字符串的解析（parsing）。

它其实是对字符串建立内部表征，被称为抽象语法树（AST）。

如果建立表征失败，意味着这个字符串并不符合布尔逻辑的语法，比如 &(pq ，解析器看到有 & 之后，它应该预期其前面有一个命题，之后也有一个命题，但它前方没有命题符号，于是停止理解抛出异常。

~(p&q) 是合法表达式，那么就会得到它的 AST 树，比如是

Not(
    And(
        p,
        q
    )
)

这里：

• 根节点是 Not
• 它有一个子节点 And
• And 再连接两个叶子节点 p 和 q

相比于字符串，AST 树在求值这个目标下被认为是更稳定的结构，比如 ~(p&q) 可以写成前缀表达式 ~(&pq) 但只要稍微修改解析规则就可以得到一样的 AST ，以内 AST 可以忽略对求值不太重要的表面细节，比如空格，括号是用 () 还是 [], 运算符写在前面还是中间。这些主要是满足人的审美和情绪价值的。

或者说，布尔逻辑表达式的核心不是字符排列，而是其运算结构。

AST 表征对计算机是友好的，因为它是一个递归性质的数据结构，有各种处理这种树的算法，比如遍历，替换子树等等。

对 AST 求值的过程和对一般代数表达式求值完全是一样的。

对于布尔逻辑由于我们关注的最小单位是原子句子，比如 p,q,r 这样的的对象，因此对于只包含 p 和 q 两个原子（叶子）命题的句子，比如 ~(p&q) 它的一个变量赋值就是 {p: 真，q: 假}, 这就是一组赋值，有了它，根据真值表查出 p&q 是假，而假的否定是真，因此最终 ~(p&q) 在 {p: 真，q: 假} 赋值下为真。

这里纯粹是一个给定 value("p")=1, value("q")=0; 计算 value("~(p&q)") 的问题。

它和给定 value("x")=1, value("y")=2; 计算 value("x(x+y)") 在思路上没有什么区别。

对应到 AST 上就是对树进行后序遍历操作，根据子树根节点的运算符求出子树的值，然后不断向上规约。

注意，到目前为止，整个系统只是：

• 表达布尔表达式
• 建立 AST
• 根据赋值进行真假求值

日常语境下，通过一些零散的句子 p,q,r 的真相，得到一个更大的句子 p&(q|r) 的真假是一种按照规则进行的信息变换，它可以看作推理。

但严格来说，这里并没有“演绎推理”（deductive inference），因为整个过程中：

• 没有前提集合（premises）
• 没有“从公式推出新公式”的规则

应用这些要素去得到新的句子才是通常所说的逻辑推理。

这里关心的只是布尔逻辑的求值系统，而且即便只有这一部分，就足够去建模显示中的复杂应用，比如组合逻辑电路中实现 ALU，同时也会出现非常复杂的问题，如 SAT 。

回顾前文，求值问题的例子是，给定 a&b 以及一组赋值 a=1, b=0, 然后根据运算表去查结果为 1, 这过程非常快，和表达式的 大小（AST 节点数量）呈线性关系。

逻辑电路设计中，给定了一个函数 f(x,y)=z 的全部定义，去寻找函数 f, 这类似机器学习问题，但 f 的空间并非连续，而仅仅是一个有限的小的已有模块集合。所以它虽然是求值的逆过程，但处理起来也非常高效。

但现在考虑这个问题： "给定一个已经设计好的 8 位全加器，是否存在输入，使最高位输出为 1？"

乍看之下，这似乎毫不困难。我们根据"整数加法"的语义：最高位为 1 ，那么 10000000 就是一个输出，那么输入是 10000000 和 0 就可以了。

我们利用了加法的性质 x+y=z, 当给定 z 之后，要寻找 (x,y) 的解空间，一个线性方程两个未知变量，因此不单纯在某组满足方程的 x,y, 这种解还有无穷个。

虽然加法例子因为线性而简单，但它确实是一个 SAT 问题，即约束可满足问题，或者说就是解方程问题。

现在问题是，给定一个乘法 x*y=z, 如果 z 是一个超大的数，那是否有解？

当然 x=1, y=z 是一组解，但如果 x,y 都小于 z, 那么这就变成一个质数判定问题，它瞬间变得非常困难。

这里重要的不是质数本身，而是 “正向计算或设计”和“逆向求解” 在复杂性上可能完全不同。

SAT 问题也是类似的现象。

给定一个复杂的由 not, and, or 组合的布尔逻辑表达式：

\[ \varphi(x_1,\dots,x_n) \]

问是否存在某组赋值，使整个表达式为真？

即：

\[ \exists x_1,\dots,x_n \quad \varphi(x_1,\dots,x_n)=1 \]

由于不同变量之间会互相耦合， 一个局部选择可能影响整个表达式。虽然每个局部运算规则都非常简单，但整体满足条件的赋值结构可能极其复杂。

理论上，n 个变量，共有 \( 2^n \) 种不同赋值，SAT 问题的目标就是要从在这些可能性中寻找满足全部约束的某个解

因此 SAT 的暴力算法是指数规模搜索。当然，根据上一节加法问题启发，优化的算法一般是要能从表达式中找出某种特殊的结构来简化搜索。

首先，任意布尔表达式都可以写成 DNF（析取范式）

其结构是：

\[ (T_1)\lor(T_2)\lor\cdots \]

其中每个 \( T_i \) 称为 term , 它是若干 literal 的 and。

例如以下是一个 DNF 表达式：

\[ (a\land b)\lor(\neg c\land d) \]

线性扫描每一个 term ，只要存在一个不是互相矛盾的表达式（如 \( \neg a\land a \)），整个表达式就可满足了，所以 DNF 形式的 SAT 非常简单，是多项式复杂度。

但实际上，这种 DNF 展开形式就是把所有的可满足的解全部写出来了，它不单单是可满足判定，而是直接给出所有解。

因此，将一般表达式转成 DNF 形式比判断它是否有解更为复杂。

暴力的 DNF 算法是遍历 \( 2^n \) 语义空间，列出巨大的真值表，然后把真值表中结果为 True 的行选出来构成 term 。

比如以 f(a, b) = a XOR b 为例

真值表共 \(2^2 = 4\) 行：

找出输出为 1 的行：

• 第 2 行：a=0, b=1 ； 构成最小项：¬a ∧ b
• 第 3 行：a=1, b=0 ； 构成最小项：a ∧ ¬b

得到 DNF \( f(a,b) = (\neg a \land b) \lor (a \land \neg b) \)

CNF 的结构是：

\[ (C_1)\land(C_2)\land\cdots \]

其中每个 \( C_i \) 称为 clause ，它是若干 literal 的 or。

例如：

\[ (a\lor b)\land(\neg c\lor d) \]

和 DNF 类似，可以暴力展开 n 个变量的 \( 2^n \) 行的真值表方式构建。

但不同于 CNF 的是，它的展开并不是暴露所有解，它还是一种解之间互相约束的“压缩”解空间状态，要满足 CNF 表达式，意味着所有 clause 都要同时满足，所以判定它并不简单。

这种“仍旧压缩”的状态使得有更高效地转成 CNF 的算法，比如 Tseitin Transformation ，它通过引入辅助变量， 在线性规模内将任意电路或布尔表达式转成等可满足（equisatisfiable）的 CNF。

注意这里并不是转成等价的 CNF 表达式，因为其中增加了变量，所以求解变复杂了一些，但只要能找到转换后的 CNF 的解，那么也找到了原表达式的解。

而 CNF 下表达式被拆分成了多个小的局部子约束，而这些子约束互相之间又相互约束，总体更加结构化了，适合算法去处理。

所以 SAT 的标准形式通常采用 CNF。

在 CNF 中还包括 2SAT 和 Horn SAT 两种简单形式，2SAT 每个 clause 最多两个 literal：

\( (a\lor b) \)

由于它可以转化为 \( \neg a \to b \) 形式，因此如果 (a=False) ，为了让 clause 成立，就必须有 (b=True)。

同理还可以得到 \( \neg b \to a \) ，所以一个 literal 相当于只有一个变量取值，整个 2SAT 公式可以转化为一个“蕴含图”问题，并利用强连通分量等图算法在线性时间内求解。

Horn SAT 的每个 clause 最多只有一个正 literal：

\[ (\neg a\lor \neg b\lor c) \]

它对应：

\[ a\land b \to c \]

和 2SAT 类似，可以在多项式时间内解决。

但问题在于没有多项式算法能将一般 CNF 形式等价转成 2SAT 或者 Horn SAT 。

3SAT 的结构是，每个 clause 最多包含 3 个 literal

例如：

\[ (a\lor b\lor \neg c) \]

虽然一般 CNF-SAT 无法转到 2SAT, 但却可以在多项式时间规约到 3SAT

每个 clause 只包括 3 个 literal 使得它能够很好地作为分析复杂度的理论工具，3SAT 是 NPC 问题证明参考 16. Cook-Levin Theorem_哔哩哔哩_bilibili

但实践中求解它的算法和求解一般 CNF 是一样的，并没有更多结构优势，反而还会引入额外辅助变量，因此实际中算法还是在 CNF 形式上的。

参考 satisfiablility 或其他文章