可行插值

普通 Craig 插值告诉我们，只要左右两部分合起来矛盾，就存在一条只谈共同词汇的边界。可行插值进一步要求这条边界能从给定证明高效读出，并且电路规模受证明长度多项式控制。证明不再只是“矛盾成立”的证书，还隐含一台区分两个不交集合的分类器。

这个转换建立了下界桥梁。若已知任何分离 $U,V$ 的电路都很大，而系统 $P$ 又有可行插值，那么 $A\wedge B$ 不可能有很短的 $P$-反驳；否则提取算法会制造一张过小电路。桥梁的每一端都要精确：共享变量决定电路输入，证明系统决定提取规则，电路下界决定最后的数值。

取

以及

若 $x=0$，$A$ 退化为 $y\wedge \mathrm{\neg }y$，所以任何满足 $A$ 的赋值都必须有 $x=1$；若 $x=1$，$B$ 退化为 $z\wedge \mathrm{\neg }z$，所以任何满足 $B$ 的赋值都必须有 $x=0$。于是 $A\wedge B$ 不可满足，且单门插值电路

满足两条蕴涵。这里 $y,z$ 的具体取值不会进入 $I$；若提取结果依赖 $y$，它就没有完成变量消去。

存在插值式不等于可行插值。把所有共享赋值列成真值表总能定义一个 separator，但可能需要指数规模，也没有展示如何从 $\pi$ 构造。可行性也不是单个公式的偶然短路：算法必须统一处理该系统的全部合适证明，运行时间和输出大小由同一个多项式控制。

归结反驳公理库归结反驳Resolution refutation · Propositional resolution从 CNF 初始子句反复归结并导出空子句的命题反驳系统。具有经典的可行插值构造，可沿证明 DAG 自底向上为每个子句配一个小电路；共享节点防止重复展开。在本文令 $I=1$ 于 $U$ 的方向下，单调版本通常要求共享变量 $x$ 在 $A$ 中只正出现、在 $B$ 中只负出现，使 $U$ 向上闭而 $V$ 向下闭；resolution 的提取电路这时可保持单调。标准 cutting planes 的相应定理通常提取单调实电路，并依赖具体规则与系数编码。缺少极性条件时仍可能有普通插值，却不能直接调用单调电路下界。

可行插值把 clique–coloring、匹配和其他互不相交 NP 对的分离下界转成 resolution、cutting planes 及若干受限 Frege 系统的证明下界：resolution 对接单调布尔电路，而标准 CP 结论须匹配单调实电路下界。切割平面证明系统公理库切割平面证明系统Cutting planes proof system · CP proof system用布尔变量上的整数线性不等式、非负组合和整数取整导出矛盾的证明系统。是否适用取决于规则和系数条件；多项式演算公理库多项式演算证明系统Polynomial calculus proof system · Polynomial calculus · PC proof system将 CNF 不可满足性编码成域上多项式方程并通过理想推理导出常数一的代数证明系统。的插值版本则要核对字段与代数表示。这里的链接表示应用场景，而不是宣称所有变体共享同一定理。

对很强的系统，可行插值本身可能是开放问题或会导致未解决的电路后果。因而证明某系统不具备已知提取算法，不能反推它一定没有 feasible interpolation；同样，短证明只会给出一般电路，而要使用 monotone lower bound 还须证明提取电路单调。明确区分“存在插值”“可高效提取”“带结构地提取”三层，是正确使用该方法的前提。