发表机构
University of Bristol（布里斯托大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明常宽CNF在多项式演算中的线性度蕴含同一素数域上常度数多项式消解的指数规模下界，并给出多种应用，包括不同模数分离及改进的消解下界。
AI 中文摘要
对于每个常宽CNF，我们证明在多项式演算（PC）中线性度意味着在常度数多项式上的消解中指数规模，且在同一素数域上。应用包括在$\operatorname{Res}(\operatorname{PC}_r/\mathbb{F}_p)$中CNF的指数下界，从而在$\operatorname{Res}(\oplus_p)$中，不同模数之间的分离，改进$\operatorname{Res}(k)$在$k=\varepsilon\log n$时的下界，证明搜索后果，以及从非常强的PC度下界推导超多项式$AC^0[p]$-Frege界。证明使用了从Braun [arXiv:2609.23015]中提取的公共乘子思想来构造一个保持推理的Razborov--Smolensky近似，而不引入扩展变量。近似误差通过误差见证多项式诱导的乘法映射的秩来衡量，模有界度的PC推论。
英文摘要
For every constant-width CNF, we show that linear degree in polynomial calculus (PC) implies exponential size in resolution over constant-degree polynomials, over the same prime field. Applications include exponential lower bounds for CNFs in $\operatorname{Res}(\operatorname{PC}_r/\mathbb{F}_p)$ and hence in $\operatorname{Res}(\oplus_p)$, separations between different moduli, improved lower bounds for $\operatorname{Res}(k)$ up to $k=\varepsilon\log n$, proof-search consequences, and an implication of super-polynomial $AC^0[p]$-Frege bounds from very strong PC degree lower bounds. The proof uses the common-multiplier idea isolated from Braun [arXiv:2609.23015] to construct a Razborov--Smolensky approximation that preserves inferences, without introducing extension variables. The approximation errors are measured by ranks of the multiplication maps induced by the error-witness polynomials, modulo bounded-degree PC consequences.
