多项式演算证明系统

形式陈述

固定一个可有效运算的域 $\mathbb F$ ，在多项式环 $\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 常计全部行展开后的单项式出现数或完整系数编码，引用结果时必须说明采用哪一种。

对有限域或有标准精确表示的有理数域，每步加法、标量乘法与乘变量均可核验；连同系数位长计量后，这给出Cook–Reckhow 系统的一个代数实例。选择有限域时，域的特征是模型参数，而不是可以从证明中忽略的排版细节。

直觉

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

degree 衡量一次推理需要同时耦合多少变量。低次多项式只能观察低阶交互；若矛盾依赖大范围一致性，任何反驳可能被迫升到高次。size 与 degree 相关但不相同：一条高次单项式可以写得很短，一条低次多项式也可能含指数多个单项式。经典 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 度量。

推论与应用

多项式演算 p-模拟 resolution：子句多项式的归结可由乘变量与线性组合导出，开销为多项式；反方向没有一般保证。degree 下界常通过构造低次多项式的伪期望、线性泛函或免疫子空间实现，再借 size–degree 关系获得规模下界。鸽巢、Tseitin 和随机约束满足问题是典型试验场，但字段特征与编码都会改变结论。

与切割平面证明系统相比，PC 使用等式与域运算，CP 使用有序整数不等式与 rounding；两者都把布尔逻辑算术化，却保存不同语义。可行插值和代数通信方法有时能把短证明转成电路或协议，不过具体提取定理必须匹配 PC/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.

形式陈述 ​

反向链接

形式陈述