SAT——布尔可满足性问题（那个著名的可判定却很难的问题）

上级：logic

SAT

给定一个由布尔变量构成的命题公式（由 ∧, ∨, ¬ 组成；通常写成合取范式（CNF），即若干子句的合取），是否存在一个使它为真的赋值？

与 FOL validity 不同，SAT 是可判定的——赋值的数量有限——但它是那个典型的困难问题。

Cook–Levin：第一个 NP 完全问题

Cook–Levin（1971）

SAT 是 NP 完全的——它属于 NP，并且 NP 中每一个问题都能在多项式时间内归约到它。（3-SAT 本身就已经是 NP 完全的。）

所以 P vs NP 这个问题就活在 SAT 里：一个多项式时间的 SAT 算法会把 NP 坍缩成 P。SAT 是一个枢纽，成千上万个问题都是靠（从 SAT）归约才被证明为 NP 难的。

∀∃ 阶梯——SAT → QBF → FOL

• SAT（命题逻辑，无量词）：NP 完全（可判定）。
• QBF（量化布尔公式——布尔变量上的 ∀/∃）：PSPACE 完全（仍可判定，但更难）。
• FOL 有效性（量词作用在无穷论域上）：不可判定。 量词作用在无穷论域上，正是逻辑从"难但可判定"跳到"不可判定"的那道分界线。

求解器是我们复用的引擎

实际中的 SAT 求解靠DPLL → CDCL（冲突驱动子句学习）来运行；SMT = SAT modulo theories（DPLL(T)）在此基础上加入了算术/数组。recursive-harness 把这整套机制原样搬到了 agent 上：

• csp-formalization——把 harness 视作一个动态 CSP（collapse = 传播）；
• conflict-learning-and-backjumping——CDCL 式 no-good 学习加非时序回跳；
• llm-as-fallible-theory-solver——DPLL(T)，LLM 充当（会犯错的）理论求解器。

这就是"我们已经用过 SAT"的地方。