SAT 的逐变量见证恢复

判定器像只会回答“这条路后面还有出口吗”的向导。恢复算法每次先试 0 分支；如果没有出口，就走 1 分支。但这一动作之所以可靠，是因为走到当前节点之前已知这里至少有一个出口。没有初次 SAT 检查，两个分支都失败时仍盲选 1，就会把任意比特串错当答案。

三个变量，四次询问 ​

取变量表 $(x_1,x_2,x_3)$，以及

初次询问回答是。例如 $(0,1,0)$ 满足三条子句。算法自身还不知道这个赋值，随后才逐项恢复：

输出是 010。逐项检查原式：第一条由 $x_2$ 满足，第二条由 $\mathrm{\neg }{x}_1$ 满足，第三条由 $\mathrm{\neg }{x}_3$ 满足。先试 0 的规则还保证它是给定变量次序下的字典序最小满足赋值：每次舍弃的 0 分支确实没有答案，任何更小总赋值都会在某个首次分歧处落进这种被排除分支。

一般正确性与终止 ​

第 $i$ 轮开始时的 不变量理路循环不变式Loop invariant在循环初始化后成立，并在每次循环迭代后继续成立的断言。是：已经记录 $a_1,\dots ,a_{i-1}$，当前 $G=F\upharpoonright a$，并且 $G$ 可满足。初次查询为真时建立它。若试零可满足，限制等价式直接保持不变量；若试零不可满足，当前 $G$ 的任何满足赋值只能给 $x_i$ 取 1，所以限制为 1 后仍可满足。

每轮固定一个之前未固定的变量，因此恰好 $n$ 轮后结束。此时没有自由变量，而当前公式仍可满足，只能是真公式；限制等价式于是证明完整的 $a$ 满足原式。证明使用准确判定器。若把超时、未知或概率性猜测当成“否”，维持可满足性的推导立即失效。

空输入、空子句和无关变量 ​

对 $(x_1)\wedge (\mathrm{\neg }{x}_1)$，初次询问为否，算法返回 UNSAT，不进入恢复。这个字符串是对所信任 oracle 回答的转述，并非一个可独立检查的归结反驳。

$n=0$ 且无子句时，初次询问为是，零次循环后返回空赋值；空赋值是有效答案，不能拿它表示无解。$n=0$ 且含空子句时，初次询问为否。空子句集即使带三个声明变量，也让算法依次选择 000，仍有四次询问。不出现在公式里的变量可任选，而本算法的确定规则总选 0。

线性查询数不等于线性总时间 ​

限制操作不增添文字或子句，变量表保持原样，因此每条查询的编码长度为 $O(N)$。按顺序扫描编码、比较编号并复制剩余文字，可给出保守的 $O(N\log (n+2))$ 位处理界；一次有效性检查另付多项式成本，例如直接检查编号与表的朴素实现为 $O(N^2)$。每轮至多构造两个限制公式，加上写出 $n$ 位答案，外层成本可界为

这里使用顺序扫描的有限编码实现，没有假设任意长整数比较免费。若一个实际 SAT 判定器在长度不超过 $cN$ 的输入上用时至多 $T(cN)$，整套程序的保守时间上界为

$n+1$ 仅是调用次数；oracle 内部可能耗费指数时间。位复杂度理路位复杂度Bit complexity · Bit operation complexity固定有限编码与逐位计算模型后，以基本位操作数衡量算法成本，并将中间数的实际位长计入每次算术运算。还要求把查询写入、解析与赋值输出一起记账。只保留当前公式与一个临时公式、原变量表及输出，外层工作存储可控制为 $O(N+n)$ 位；判定器内部空间单列。

这一构造说明 SAT 搜索可多项式 Turing 归约到 SAT 判定，不声称 SAT 已有多项式求解算法。与 Karp 归约一次写出一个目标实例不同，这里后续查询依赖之前的回答；它也不同于 DPLL 在没有 oracle 时自行探索和回溯。

一般 FNP 关系理路搜索关系与 FNPFNP · Polynomially balanced search relation · 多项式平衡搜索关系用多项式平衡关系规定可接受见证，处理变长证书与无解返回，并证明前缀语言怎样借助NP完全判定器恢复见证。可经 NP 前缀语言，再归约到一个 NP 完全判定器来恢复。SAT 更便利之处是前缀限制自然仍为 CNF，直接保留了原问题的接口。优化见证可在先确定最优阈值后使用同样的前缀思路，但所询问的必须是“满足阈值且兼容前缀”的语言。

共同终点与可运行检查器把判定黑箱明确实现为独立的暴力真值表，只为小输入复核这份恢复程序。有限穷举是实现证据；本页的不变量证明才覆盖任意有限输入。