布尔可满足性问题

布尔可满足性问题通常简称 SAT，是判定能否通过为变量赋予真值，使一个命题逻辑公式为真的问题。至少存在一个这样的赋值时，公式称为可满足的；不存在时，则称为不可满足的。SAT 是计算机科学中的基础问题：它是第一个被证明具有NP完全性的问题，也为表达和求解许多有限约束问题提供了通用框架。(cs.princeton.edu)

定义与逻辑含义

布尔公式由取值为真或假的变量，以及否定（ $\neg$ ）、合取（ $\land$ ）、析取（ $\lor$ ）等联结词组成。真值赋值为每个变量指定一个值。SAT 要回答的是：是否存在一个赋值，使整个公式的求值结果为真。(arxiv.org)

对于含有变量 $x_1,\ldots,x_n$ 的公式 $F$ ，这一问题可写为

\exists a\in\{0,1\}^{n}\quad F(a)=1,

其中， $0$ 表示假， $1$ 表示真。满足公式的赋值也称为该公式的模型。(theory.cs.princeton.edu)

例如，

F=(x\lor y)\land(\neg x\lor z)\land\neg z

是可满足的：令 $x=0$ 、 $y=1$ 、 $z=0$ ，即可使每个合取项都为真。相比之下，

G=x\land\neg x

是不可满足的，因为它的两个合取项要求 $x$ 取互不相容的值。

可满足性不同于逻辑有效性。可满足的公式在至少一个赋值下为真；有效的公式，即重言式，则在每一个赋值下都为真。这两个概念通过否定联系起来： $F$ 有效，当且仅当 $\neg F$ 不可满足。因此，检查一组前提是否蕴涵某个结论，可以归约为检查这些前提与该结论的否定合在一起是否不可满足。(arxiv.org)

合取范式与编码

SAT 求解器通常处理以合取范式（CNF）表示的公式。文字是一个变量或其否定；子句是若干文字的析取；CNF 公式则是若干子句的合取：

F=\bigwedge_{i=1}^{m}C_i, \qquad C_i=\bigvee_{j=1}^{k_i}\ell_{ij}.

满足赋值必须使每个子句中至少有一个文字为真。这种表示方式可以将公式存储为子句列表，每个子句又包含一个文字列表，便于高效存储和操作。(theory.cs.princeton.edu)

若反复运用析取对合取的分配律，将任意公式转换为逻辑等价的 CNF，所得表达式的规模可能呈指数增长。Tseitin 变换通过引入表示子公式的辅助变量，并添加强制满足其定义的子句，避免了这种增长。在通常的运算符元数有界的表示方式下，所得 CNF 的规模与原表达式的规模成线性关系，并且与原公式等可满足。(cs.cmu.edu)

等可满足性保留的是解是否存在，而不是要求两个公式在相同变量集上具有完全相同的满足赋值。定义式编码允许将原变量的满足赋值扩展到辅助变量上，也允许将编码的模型投影回原变量。(cs.cmu.edu)

在实践中，编码方式的选择十分重要。同一约束的两种编码可能在规模、传播能力和求解器性能上有所不同。规模更小的编码不一定更容易求解。(cs.cmu.edu)

计算复杂性与历史意义

SAT 在计算复杂性理论中占据核心地位。斯蒂芬·库克于 1971 年证明了其奠基性的完全性结果；列昂尼德·列文独立得出了相关结果，并于 1973 年发表。这一结果被称为库克—列文定理。(theory.stanford.edu)

其现代表述包含两个部分：

**SAT 属于 NP：**对于一个给定的候选满足赋值，可以在相对于公式规模的多项式时间内检查它是否满足公式。
**SAT 是 NP 难的：**NP 中的每个判定问题都可以通过保持答案不变的多项式时间归约转换为 SAT。(theory.cs.princeton.edu)

这一定理将计算与逻辑联系起来。一个时间受多项式界限约束的计算过程，可以用布尔约束来表示，这些约束描述其初始配置、合法的状态转移和接受结果。这些约束可满足，当且仅当存在一个接受的计算过程。(cs.princeton.edu)

因此，若一般 SAT 存在多项式时间算法，则 $P=NP$ ；反之，若 $P=NP$ ，则这样的算法必然存在。NP 完全性是对最坏情况的分类，并不意味着每个 SAT 实例都很难求解。(cs.princeton.edu)

严格来说，SAT 是一个判定问题，答案为“是”或“否”。求解器通常还会在满足赋值存在时返回一个这样的赋值。判定与搜索密切相关：给定一个 SAT 判定过程，可以逐个固定变量的值，并测试公式是否仍然可满足，从而构造出一个模型。(theory.cs.princeton.edu)

重要的受限形式

对公式结构施加限制，可以显著改变问题的复杂性。

3-SAT 要求 CNF 中每个子句至多含有三个文字。它仍然是 NP 完全的，并广泛用于复杂性归约。借助辅助变量，可以将长子句替换为由短子句组成的链，同时保持可满足性。(theory.cs.princeton.edu)

2-SAT 允许每个子句至多含有两个文字，可在多项式时间内求解。子句 $a\lor b$ 可以解释为蕴涵 $\neg a\Rightarrow b$ 和 $\neg b\Rightarrow a$ 。由此可得到一种蕴涵图方法：公式不可满足，当且仅当某个变量及其否定属于同一个强连通分量。(cs.princeton.edu)

Horn-SAT 要求每个子句至多含有一个正文字。这样的子句可以表达蕴涵规则，从而系统地传播被强制确定的真值。霍恩可满足性可以在线性时间内判定，时间界限以文字出现的总次数计。(seas.upenn.edu)

析取范式可满足性也易于求解：一个由若干合取项构成的析取式是可满足的，当且仅当至少有一个合取项不包含互相矛盾的一对文字。然而，将任意公式转换为这种表示可能需要指数空间，因此，这并不能提供高效的通用 SAT 判定过程。(cs.cmu.edu)

求解方法

穷举搜索与 DPLL

一种直接的方法是构造真值表，或以其他方式测试 $n$ 个变量的全部 $2^n$ 个赋值。这种方法是完备的，但其计算量随变量数呈指数增长。更有效的方法会避免探索已被约束排除的赋值。(cs.cmu.edu)

1962 年提出的戴维斯—普特南—洛格曼—洛夫兰算法（DPLL）将分支搜索与化简相结合。它反复执行单元传播：如果一个子句中只有一个文字尚未被判定为假，那么该文字必须为真。当传播无法确定公式的可满足性时，算法会选择一个尚未赋值的变量，尝试一个取值；如果某个子句变为假，就进行回溯。(cs.cmu.edu)

冲突驱动子句学习

冲突驱动子句学习（CDCL）通过分析冲突并推导新子句，扩展了上述搜索过程，以防止导致冲突的原因再次出现。求解器不只是撤销最后一次决策，还可以回跳到更早的相关决策层级。(cs.cmu.edu)

CDCL 的实现将子句学习与高效传播、分支启发式方法、重启，以及选择性删除已学习子句相结合。重启会放弃当前的部分赋值，同时保留有用的已学习信息。这些技术引导搜索，但不改变所要回答的逻辑问题。(cs.cmu.edu)

局部搜索

局部搜索方法从一个完整赋值出发，反复改变变量的值，以减少未满足的子句数量。这类方法可能有效地找到满足赋值，但未能在时限内找到赋值，并不能证明公式不可满足。这一点使其有别于完备的判定过程：后者在资源充足的情况下，能够确定公式可满足或不可满足。(cs.cmu.edu)

应用与结果验证

通过将问题转换为布尔约束，SAT 可以充当通用求解引擎。其应用包括硬件和软件的形式验证、自动规划以及调度。在验证中，约束可以描述违反某项要求的系统执行过程；此时，满足赋值就代表一个反例。(cs.cmu.edu)

对于可满足的结果，可以将返回的赋值代入输入公式求值，以检查其正确性。不可满足的结果则需要另一种证据：证明不存在满足赋值。SAT 求解器能够生成 DRAT、LRAT 等格式的证明日志，将复杂的证明生成过程与独立检查分离。LRAT 添加了提示信息，使检查器可以相对简单且高效，其中一些实现还经过定理证明系统的验证。(cs.cmu.edu)

证明检查验证的是编码所得公式的不可满足性。从原始应用到公式的转换是否正确，仍需另行保证；如果系统编码有误，求解器可能对错误的问题给出正确的 SAT 结果。(cs.cmu.edu)

扩展与相关问题

一些相关问题保留了布尔推理，但改变了所问的问题，或增强了表达能力。

**最大可满足性问题（MaxSAT）**要求找到使尽可能多的子句得到满足的赋值。加权变体要求最大化已满足子句的总权重；部分变体则区分必须满足的硬子句和可选择满足的软子句。这些属于数学优化问题，而不只是可行性检验。(cs.cmu.edu)
**模型计数（ $\#\mathrm{SAT}$ ）**要回答有多少个赋值满足某个公式。它是一个计数问题，具有 $\#P$ 完全性。一般而言，找到一个模型不足以确定模型的总数。(cs.cornell.edu)
**量化布尔公式（QBF）**允许同时使用存在量词和全称量词。普通 SAT 相当于对每个变量施加存在量化；判定不受限制的闭合 QBF 的真值是 PSPACE 完全的。量词的顺序决定了哪些存在量化变量的取值可以依赖于先前全称量化变量的取值。(cs.cmu.edu)
**可满足性模理论（SMT）**将布尔结构与具有特定解释的约束相结合，例如算术、数组或位向量约束。许多 SMT 求解器通过协调布尔求解器与专门的理论判定过程来工作；其复杂性和可判定性取决于所涉及的理论及公式片段。(arxiv.org)

实践中的局限

高效的 SAT 求解并未消除最坏情况下的计算困难。性能取决于实例的结构、编码方式和求解器的搜索策略。即便某些约束具有高效的专用算法，如果编码未能充分呈现其结构，通用布尔求解器也可能难以处理它们。(cs.cmu.edu)

资源限制也会影响所报告结果的含义。超时或“未知”结果意味着计算尚未解决该问题，并不是不可满足的证据。同样，验证结果的适用范围取决于所编码的模型及其边界条件，而不只是求解器能否回答 SAT 或 UNSAT。(cs.cmu.edu)

参考来源

Cook-Levin Theorem: SAT is NP-completecs.princeton.edu
Intractability IIcs.princeton.edu
Lecture: SAT & SMT, Part 2cs.cmu.edu
The Complexity of Theorem-Proving Procedurestheory.stanford.edu
Computational Complexity: A Modern Approachtheory.cs.princeton.edu
A Survey of Satisfiability Modulo Theoryarxiv.org
Verified CNF Encodingscs.cmu.edu
Logic and Mechanized Reasoning: SAT Basicscs.cmu.edu
Lecture 23: Intractabilitycs.princeton.edu
Chapter 18 — Horn and 2-SAT Satisfiability (Classical)users.ece.utexas.edu
Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulaeseas.upenn.edu
Generalizing Boolean Satisfiability I: Introductioncs.cmu.edu