从是或否恢复一份可检查的答案 ​

给你一台只回答“有解吗”的机器，怎样让它帮你找到答案？本单元要逐份写出它收到的查询，恢复一份能直接检查的见证，再解释这些查询花了多少时间、为什么会停止，以及同样的做法何时不能迁移。

下载Python 标准库检查器。它不联网，不调用 SAT 库或其他求解器；内部判定器故意枚举所有小赋值，外层恢复程序只拿到布尔值。将文件放入一个空目录，用 Python 3.10 或更新版本运行：

python foundations-decision-to-witness-checker.py
python -O foundations-decision-to-witness-checker.py

两次结果应一致。检查使用会实际抛错的条件判断，不能被 -O 删除。JSON 给出公式查询、SAT oracle 内部尝试数、枚举输出时刻、完整背包表和位长账本。枚举函数本身逐项产生答案；为显示这个很小的例子，测试层把输出收集成列表，这份演示列表不作为多项式空间算法的证据。

1. 选择入口，先检查三个基础问题 ​

核心链只有三站：NP 的验证器接口理路复杂度类 NPNP · Nondeterministic polynomial time由正实例拥有多项式长度、可在多项式时间内验证的证书所刻画的语言类。 → 搜索关系与 FNP理路搜索关系与 FNPFNP · Polynomially balanced search relation · 多项式平衡搜索关系用多项式平衡关系规定可接受见证，处理变长证书与无解返回，并证明前缀语言怎样借助NP完全判定器恢复见证。 → SAT 逐变量恢复理路SAT 的逐变量见证恢复SAT self-reduction · SAT search-to-decision · SAT 自归约只调用返回是或否的SAT判定器，用逐变量限制恢复总赋值，并分开计算查询次数、查询位长、外层成本与无解终止。。已有“算法与复杂性”路线负责 P/NP 和困难性，不需要重读整个多项式层级才能做本实验。

如果下面的自测有困难，按相应链接补课：

1. 在 CNF 中，“没有子句”与“有一条空子句”分别是真还是假？补读 CNF 可满足性理路CNF 可满足性问题CNF satisfiability · CNF-SAT给定有限个命题子句的合取，判定是否存在同时满足全部子句的布尔赋值。
2. 二进制整数 $2^{20}$ 用多少位，输出 $2^{2^{20}}$ 的完整二进制串又需要多少位？补读 位复杂度理路位复杂度Bit complexity · Bit operation complexity固定有限编码与逐位计算模型后，以基本位操作数衡量算法成本，并将中间数的实际位长计入每次算术运算。
3. Karp 归约能否看到目标答案后，再决定第二次问什么？补读 多项式时间归约理路多项式时间归约Polynomial-time reduction · Karp reduction用一个多项式时间可计算的变换把问题 A 的实例转换为问题 B 的实例。

检查答案：没有子句的合取为真，空子句为假；$2^{20}$ 用21位，而后一个输出需 $2^{20}+1$ 位；Karp 归约是一次性实例变换，不允许自适应调用。第三项不会阻止多项式 Turing 归约采用多次询问，它们是不同接口。

完成 SAT 核心后，有两条分支。数值分支读 FP 的输出函数理路函数复杂度类 FPFP · Function polynomial time · 多项式时间函数明确单值函数的全输入输出契约、写出成本与复合封闭性，并区分FP函数、P语言和FNP关系的选择算法。、优化阈值与见证理路从优化阈值到最优见证Optimization to threshold decision · Binary search for optimum · 优化搜索判定归约在有限整数目标和显式上界下二分求最优值，再用受阈值约束的前缀恢复见证，分开核算数值范围与编码成本。、容量 DP 完整账单理路复杂度类 PP · Polynomial time能由确定性算法在输入长度的多项式时间内判定的语言集合。和已有 FPTAS 缩放证明理路通过缩放构造 FPTASFPTAS via scaling · value scaling FPTAS通过缩放并向下取整数值，把背包的伪多项式动态规划转为对输入规模与精度均多项式的方案。。输出流分支读 解枚举的延迟、输出与空间理路解枚举的延迟、输出与空间Polynomial delay enumeration · Output-polynomial enumeration · 枚举复杂性为无重复的有限解枚举分别规定首项、中间、收尾延迟、总输出成本与工作空间，并证明SAT前缀剪枝的oracle延迟界。。分支的结果都回到本页核验。

2. 固定对象、接口与资源 ​

SAT 输入明确列出变量 $(x_1,x_2,x_3)$，公式为

把文字 $x_i$ 写成整数 $i$，$\mathrm{\neg }{x}_i$ 写成 $-i$，则三条子句是 (1,2),(-1,3),(-2,-3)。oracle 的输出只有真或假。UNSAT 与空赋值是不同结果；脚本以 None 表示无解，以空元组表示没有变量的有效赋值。公式限制通过删除已满足子句、删除假文字完成，声明的原变量表始终保留。

背包输入为物品 $(4,10),(3,8),(2,6)$ 与容量5，二元组的第一项是重量、第二项是价值。每件至多选一次，输出为按原物品顺序排列的三个选择位。目标值是非负整数，阈值问题询问“是否有总重量至多容量、总价值至少阈值的子集”。空集可行。

3. 复算 SAT 的四次查询 ​

先独立写出所有四个查询及回答，再比对下面的完整答案。

第一次询问原式 $F$，答案为真。随后先试 $x_1=0$：第一子句变为 $x_2$，第二子句已经由 $\mathrm{\neg }{x}_1$ 满足而删除，第三子句仍为 $\mathrm{\neg }{x}_2\vee \mathrm{\neg }{x}_3$。第二次查询为

答案为真，于是固定 $x_1=0$。

再试 $x_2=0$，单位子句 $x_2$ 变为空子句，另一子句已被 $\mathrm{\neg }{x}_2$ 满足。第三次查询含空子句，答案为假。当前分支已知有解，所以必须选 $x_2=1$；这时只剩 $\mathrm{\neg }{x}_3$。

最后试 $x_3=0$，唯一子句被满足，第四次查询是空子句集，答案为真。输出 010。将它代回三条原子句，依次由 $x_2$、$\mathrm{\neg }{x}_1$、$\mathrm{\neg }{x}_3$ 满足。

必须同时交出的证明是不变量：“已记录的前缀可以补成原式的满足赋值”。初问建立它；试零回答是就保留0，回答否时原有补全只能取1；每轮增加一位，三轮后前缀就是完整答案。一般 $n$ 变量时得到 $n+1$ 次调用，而不是只看到本例恰好四次就猜出规律。

查询大小也有证据：限制操作只删子句和文字，不增加变量表。若原编码长 $N$，每份查询仍为 $O(N)$，外层扫描和输出的保守位时间为 $O(N^2+nN\log (n+2)+n)$，再加 $(n+1)T(cN)$ 才是使用实际判定器的总界。这份账单将解析检查、前缀处理和 oracle 内部工作分开。

4. 迁移：哪些改动仍能恢复，哪些会破坏接口 ​

先尝试四个变体，再看答案。

• 给 $F$ 加单位子句 $x_1$：答案变成什么，试零顺序是什么？
• 给 $F$ 同时加 $x_1$ 与 $x_2$：算法在哪里停止？
• 不加约束，只在变量表里额外声明 $x_4$：该输出多少位？
• 没有变量时，无子句和一条空子句分别返回什么？

完整答案：加入 $x_1$ 后唯一模型是 101，三个试零回答依次为否、是、否，加上初问共四次。加入 $x_1,x_2$ 后，由第一条选择迫使 $x_3=1$，再由 $x_2=1$ 迫使 $x_3=0$，原式无解，初问即返回 UNSAT。额外声明自由 $x_4$ 时，本算法仍输出四位 0100，并执行五次查询；所有模型为 0100,0101,1010,1011。零变量且无子句输出空赋值，零变量且含空子句输出无解，二者都只有初次一次询问。

再考虑一般 FNP 关系，其合法见证为 $\{\epsilon ,10,111\}$，长度上界3。问前缀是否可补全后，必须先验证当前空串；它已经是答案，应立即停止。若合法集合改为 $\{10,111\}$，就先排除0前缀，进入1，再进入10并停止。把10补为100会失去合法性。固定长度正规化必须同时存原长度、检查长度不超过上界，并要求剩余填充位全为0。

最后指出不可直接迁移的情况：只知道 $R(x,y)$ 可快速验证，不能推断原域语言 $D_R(x)$ 的判定器能回答任意前缀约束。正确的通用方法是构造 $E_R(x,s)$，证明它在 NP 中，再归约到一个 NP 完全判定器；若 $D_R$ 自身 NP 完全，也可选它作为目标。对永远有解的求逆关系，域判定器可能始终回答是，它没有因此透露原像的下一位。

5. 复算最优值，再恢复同一份背包见证 ​

所有价值相加给出上界24。初次询问阈值0为真，之后的二分阈值依次为

范围依次为 $[0,24]\to [12,24]\to [12,17]\to [12,14]\to [13,14]\to [14,14]$，所以最优值为14。初问加二分共六次，但还没有输出选择位。

恢复见证时，试排除第1件仍可由第2、3件达到14，选0。试排除第2件，只剩第3件且价值仅6，答案否，所以选1，将剩余容量与阈值变为2与6。试排除第3件，空集价值0达不到6，选1。三次恢复调用后输出 011，总计九次调用。

为什么这三次仍可交给同一种背包阈值判定器？每一步剩下的是一个更短的物品表、一个剩余容量与剩余目标。没有把一个原本不支持“前缀”的接口强行多传一个参数，而是给出并证明了残余实例变换。若某件超重，已知有解保证排除它不会失败；阈值降到非正时，空集自动够用。

迁移题：容量改成4，答案是什么？完整答案是价值10、选择 100；第2、3件合重5，已不再可行。最优值不能从旧容量5的答案直接复用。若所有价值改乘 $2^{20}$，最优选择不变，最优值为 $14\cdot 2^{20}$，上界位数只增加20；二分的查询数相应只增加线性于20的量，而逐个试数值会付出约 $2^{20}$ 倍的轮数。

6. 同一张 DP 表，分别按数值和位数计费 ​

从第0行开始填表；$A_i[c]$ 的含义是前 $i$ 件、重量至多 $c$ 的最大价值，不是重量恰好为 $c$。完整答案如下：

按是否选择当前物品分成两类，得到 $A_i[c]=max(A_{i-1}[c],A_{i-1}[c-w_i]+v_i)$，超重时去掉第二项。每项读取上一行，所以每件最多使用一次；由行号归纳就是一般正确性证明。回溯依次经过 $(3,5),(2,3),(1,0)$，恢复第3、2件。

采用编码 $1^{\ell (a)}0\mathrm{bin}(a)$，字段顺序 $n,W,w_1,v_1,w_2,v_2,w_3,v_3$，各字段长 $5,7,7,9,5,9,5,7$，总计54位。表有24格，其中初始化6格，更新18格，允许尝试选入的格数为2+3+4=9。整数加比较还依赖保存价值的位数，不能把“18格”解释为“18次基本位操作”。

若容量为 $2^m$，且两件物品重量均为 $2^{m-1}$、价值均为1，编码长度为 $O(m)$，这份容量 DP 仍建立 $2^m+1$ 列。即便先把容量截到总重量，此例也不会缩小。它说明算法是伪多项式，没有证明背包困难性，更没有证明这个简单特例本身需要指数时间。强、弱数值困难是另一个归约性质，见 相应定义与条件理路NP 困难性NP-hardnessNP 中每个语言都可多项式时间归约到目标问题。。

已有缩放证明怎样接回来 ​

沿用旧 FPTAS 页的精度 $\epsilon =1/4$，所有三件都单独可行，$V_{max}=10\le OPT=14$。缩放因子 $K=\epsilon V_{max}/n=5/6$，缩放价值为 $(12,9,7)$。按缩放价值建立表时，最大总下标28，连零共29列；不能误写成28格。

返回第2、3件的缩放价值16，真实价值14。FPTAS 的保证仅是至少 $(1-1/4)14=10.5$，本例碰巧精确最优。证明的关键不是“数变小了”，而是每件舍入损失小于 $K$，总损失小于 $nK=\epsilon V_{max}\le \epsilon OPT$；完整不等式、空输入、零价值和有理精度位账继续由 旧缩放页理路通过缩放构造 FPTASFPTAS via scaling · value scaling FPTAS通过缩放并向下取整数值，把背包的伪多项式动态规划转为对输入规模与精度均多项式的方案。承担。

迁移边界：如果所有物品都超重，应先筛除并返回空集，不能对 $n=0$ 计算缩放因子；如果最大可行价值为零，空集已最优，也不能除以零。若随意把重量缩小而保留容量，返回集合可能超重，那是改变可行性的新问题。仅有伪多项式 DP 也不自动给出 FPTAS，必须证明状态压缩和误差界同时成立。

7. 枚举两个模型，连结束等待也计费 ​

按先0后1、仅进入 oracle 已确认非空的子树做深度优先遍历。输出完整答案应为 010、101，无重复。检查器在第5次 oracle 调用后输出第一份，第10次后输出第二份，第11次后完成，因此首项、中间、收尾的调用间隔分别为5、5、1。

这里11不是一份见证恢复的4，5也不是现实中的五个时钟周期。每次调用都可能触发暴力判定；可证明的是外层树高至多 $n$，相邻输出间至多回退和下降各 $n$ 层，因此只有 $O(n)$ 次判定及多项式外层工作。朴素递归保存每层一份公式，空间上界为 $O((n+1)N)$ 位，不缓存已经输出的模型。

迁移题：先等 $2^n$ 步，再输出全部 $n$ 位串，这算什么效率？答案是输出多项式总时间，因为输出本身已有 $\mathrm{\Theta }((n+1)2^n)$ 位；它没有多项式首项延迟。只有两个输出间的等待很小，也不能省略空集和收尾时间。若把所有模型存在内存中再输出，延迟和空间还得重新分析。

8. 完成标准与检查范围 ​

完成本单元时，应能在不运行脚本的情况下给出四次 SAT 查询和不变量，九次背包调用及残余实例，54位输入与24格容量表，变长证书停止条件，以及枚举三段间隔。还能解释：FP 输出指定字符串，FNP 允许任意合法见证，NP 是判定语言；这些接口的相互转换必须附带算法与成本。

检查器穷举446份小 CNF（另含重复文字、永真子句等变体），对照独立真值表检查最小模型、调用次数、全部模型与延迟。它还检查所有32768个“长度至多3的见证子集”，覆盖空集合与空串见证；再对3280个小背包核对 DP、暴力最优值和阈值恢复。长度正规化的超界字段和非零填充也会被拒绝。

这些是有限实现验证。一般正确性来自限制等价式、可满足前缀不变量、整数区间不变量和 DP 行归纳；多项式结论来自位长与操作账本。脚本没有验证任意规模的复杂性类分离，也不以 oracle 内部的小样本运行时间预测大型 SAT 求解器。