多项式演算证明系统

形式陈述

固定域 $\mathbb F=\mathbb Q$ 或某个固定有限域，并采用可执行多项式时间精确运算的系数编码，在多项式环 $\mathbb F[x_1,\ldots,x_n]$ 中工作。为保证变量取布尔值，加入公理

x_i^2-x_i=0.

CNF 子句 $C$ 编成“所有文字同时为假”的指示多项式等于零：

p_C(x)= \prod_{x_i\in C}(1-x_i) \prod_{\neg x_j\in C}x_j =0.

证明从这些公理出发，允许从 $p=0,q=0$ 推出 $ap+bq=0$ （ $a,b\in\mathbb F$ ），以及从 $p=0$ 推出 $x_i p=0$ 。导出 $1=0$ 即为反驳。多项式演算的 degree 是所有证明行的最大总次数；size 常计全部行展开后的单项式出现数或完整系数编码，引用结果时必须说明采用哪一种。

每步加法、标量乘法与乘变量都可按展开系数表核验，系数位长也计入证书。CNF 不可满足时，对每个布尔赋值 $a$ ，选一个被它违反的子句 $C_a$ ；赋值指标 $\delta_a=\prod_{a_i=1}x_i\prod_{a_i=0}(1-x_i)$ 是 $p_{C_a}$ 的多项式倍，而 $\sum_a\delta_a=1$ 。把这些倍数展开后，反复乘变量和线性组合即可导出 $1$ ，证明反驳完备性，但没有承诺该枚举证明很短。把这种反驳写成Cook–Reckhow 系统时，对任意目标 $\varphi$ 固定Tseitin 编码 $E(\neg\varphi)$ ，核验其 PC 反驳后输出 $\varphi$ ；非法证书输出固定永真式。选择有限域时，域的特征是模型参数，而不是可以从证明中忽略的排版细节。

直觉

每个初始多项式都在所有满足赋值上取零；合法推理只是在这些多项式生成的理想中继续运算。因此若最终把常数 $1$ 写成初始多项式和布尔公理的代数组合，就说明不存在共同零点。resolution 用子句消去一个文字，多项式演算则用消项、乘变量和线性组合揭示矛盾，特别适合表达奇偶、计数和代数结构。

degree 衡量一次推理需要同时耦合多少变量。低次多项式只能观察低阶交互；若矛盾依赖大范围一致性，任何反驳可能被迫升到高次。size 与 degree 相关但不相同：一条高次单项式可以写得很短，总次数至多 $d$ 的 $n$ 元多项式可以含 $\binom{n+d}{d}$ 个单项式；固定 $d$ 时这仍是关于 $n$ 的多项式，但次数增长后可能很大。经典 size–degree 论证需在固定域、变量数和行表示下使用。

例子与边界

仍取

F=(x\lor y)\land(x\lor\neg y)\land(\neg x).

三个子句对应

(1-x)(1-y)=0,\qquad (1-x)y=0,\qquad x=0.

把前两式相加并展开：

(1-x)(1-y)+(1-x)y=(1-x)\bigl((1-y)+y\bigr)=1-x=0.

再与 $x=0$ 相加得到 $1=0$ 。这份反驳最大 degree 为 $2$ ；第一步的两个二次项 $xy$ 精确抵消。计算在任意特征上都成立，包括特征二，因为 $-y+y=0$ ，而 $1$ 仍非零。

域选择会影响证明复杂度。某些模计数原理在特征 $p$ 的域上可被自然消去，在特征不同的域上却可能需要高 degree；因此不能只写“PC 下界”而省略 $\mathbb F$ 。若改在一般环上工作，非零常数未必可逆，完备性与推理规范也会改变。

还要区分 polynomial calculus 与 Nullstellensatz、Gröbner basis 算法和 polynomial calculus with resolution（PCR）。PCR 为每个 $\neg x_i$ 引入补变量并加 $x_i+\bar x_i-1=0$ ，可能让行更简洁；它与 PC 在常见尺度上有关联，却不是逐字同一系统。把多项式保留为算术电路而不展开，也会改变 size 度量。

推论与应用

按展开单项式计大小时，不能把 PC 与 PCR 的模拟结论混在一起。对宽度 $w$ 的全正子句，本页编码 $\prod_{i=1}^w(1-x_i)$ 已有 $2^w$ 个非零单项式。例如 $(x_1\lor\cdots\lor x_w)\land\bigwedge_i\neg x_i$ 有线性行数的归结反驳，而本页 PC 反驳必须使用这个大公理：若不使用，零赋值满足其余全部公理。因此直接展开的 PC 并不多项式模拟任意宽度的归结。PCR 为正负文字各保留一个变量，子句成为单个单项式，标准的逐步模拟才具有多项式大小。再把补变量代回 $1-x_i$ 可得到 PC 推导，但展开成本须保留对证明宽度的指数依赖；固定宽度时这一开销受控。degree 下界常通过构造低次多项式的伪期望、线性泛函或免疫子空间实现，再借 size–degree 关系获得规模下界。鸽巢、Tseitin 和随机约束满足问题是典型试验场，但域特征与编码都会改变结论。

与切割平面证明系统相比，PC 使用等式与域运算，CP 使用有序整数不等式与 rounding；两者都把布尔逻辑算术化，却保存不同语义。可行插值和代数通信方法有时能把短证明转成电路或协议，不过具体提取定理必须匹配 PC/PCR 变体，不能因都含“多项式”便机械套用。

参考资料

Yuval Filmus et al., “Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds,” ICALP 2013 full version, §1 footnote1 and §2：展开单项式计量下的 PC/PCR 区分与 PCR 对归结的模拟。
Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo, “Using the Gröbner Basis Algorithm to Find Proofs of Unsatisfiability,” Proceedings of STOC 1996, pp. 174–183, §2.
Alexander A. Razborov, “Lower Bounds for the Polynomial Calculus,” Computational Complexity 7(4), 1998, pp. 291–324.
Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall, “Lower Bounds for the Polynomial Calculus and the Gröbner Basis Algorithm,” Computational Complexity 8(2), 1999, pp. 127–144.

形式陈述 ​

反向链接

形式陈述