3-SAT

3-SAT 把一般逻辑约束限制为局部的三元析取，却仍保留 SAT 的全部 NP 困难性，因为许多共享变量的小约束组合起来仍能表达全局选择困难，而困难并不来自某个巨大子句。宽度约束也使归约构件局部而规则，适合作为图、集合和调度问题的起点。把一般长子句拆分时必须引入辅助变量，以保持“存在某个扩展赋值”的等可满足性，而非逐赋值等价。

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

四文字子句 $(a\vee b\vee c\vee d)$ 可用新变量 $u$ 替换为

原子句可满足当且仅当存在 $u$ 使新公式可满足；对长度更长的子句可串联辅助变量。长度为 $1$ 或 $2$ 的子句可重复文字补到三个位置。

2-SAT 有线性时间算法，因此“每个子句常数宽”本身不导致 NP 完全；阈值恰在宽度从 $2$ 到 $3$。拆分保持的是整体可满足性，不能要求原变量每个固定赋值下新公式不经选择辅助变量便同值。

3-SAT 建立在命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。上，并由Cook–Levin 定理公理库Cook–Levin 定理Cook–Levin theorem · SAT is NP-complete布尔可满足性问题 SAT 是 NP 完全问题。后的宽度约化得到 NP 完全性；许多图问题归约从三文字子句构造常数规模 gadget。精确时间主线固定 $n$ 为变量数：ETH公理库指数时间假设 ETHExponential Time Hypothesis · ETH假设以变量数 n 衡量的 3-SAT 不存在 2^{o(n)} 乘多项式因子的算法。排除 $2^{o(n)}$，稀疏化引理公理库稀疏化引理Sparsification lemma · Sparsification lemma for k-SAT将固定宽度 CNF 分解为指数率任意小的线性规模稀疏公式析取，并保持可满足性。把稠密固定宽度公式拆成线性子句分支，SETH公理库强指数时间假设 SETHStrong Exponential Time Hypothesis · SETH假设随着子句宽度增长，k-SAT 的最优指数底数不能被某个统一小于 2 的常数界定。则量化所有 $k$-SAT 的指数底数。三者是条件假设或定理，不属于 3-SAT 问题定义。