形式陈述

3-SAT 的输入是合取范式

$$\phi =C_1\wedge \cdots \wedge C_m,$$

其中每个子句 $C_i$ 是三个文字的析取，文字是变量 $x$ 或其否定 $\mathrm{\neg }x$。问题询问是否存在布尔赋值使 $\phi$ 为真。

本条采用“每个子句恰有三个文字”的约定；允许重复文字时，含一或两个文字的子句可填充为三个，因此与“至多三个文字”的常见约定多项式等价。

直觉

3-SAT 把一般逻辑约束限制为局部的三元析取，却仍能通过许多局部约束组合表达全局选择困难。

例子与边界

公式 $(x\vee y\vee z)\wedge (\mathrm{\neg }x\vee y\vee y)$ 是合法实例。3-SAT 不应与 2-SAT 混淆：2-SAT 可在线性时间内求解，而 3-SAT 是 NP-complete。若要求三个互异变量且不允许重复，需要额外的等价变换。

推论与应用

3-SAT 属于 NP，并可由 SAT 多项式归约得到，因此是 NP-complete。它是图着色、独立集、顶点覆盖及大量组合优化问题困难性归约的标准起点。

参考资料

• Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009，§2.2。
• Michael Sipser, Introduction to the Theory of Computation, 3rd ed., Cengage, 2013，§7.4。