paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Monomial size vs. Bit-complexity in Sums-of-Squares and Polynomial Calculus

平方和与多项式演算中单项式大小与比特复杂度
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 2/10 · 论文研究SOS/PCR证明系统中单项式规模与比特复杂度的下界，属于证明复杂度/形式化验证理论，但未涉及LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析，与画像核心方向基本无关。引用 0 inbox
Tuomas Hakoniemi
定理证明与证明工程逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：构造布尔约束Q_n：存在度2且单项式数多项式的SOS/PCR/ℚ反驳，但任何反驳均需指数级比特复杂度。

本文研究在有理数上的多项式演算消解（PCR/ℚ）与平方和（SOS）证明系统中，反驳的单项式规模与比特复杂度之间的关系。作者构造了一族定义在布尔变量上的多项式约束 Q_n，并证明该约束集同时具有度数为 2 的 SOS 反驳和 PCR/ℚ 反驳，因此其单项式数量仅为多项式级。然而，当有理系数以二进制表示的既约分数形式编码时，任何 SOS 或 PCR/ℚ 反驳都必然具有指数级比特复杂度。该结果说明，单项式数量少并不保证系数表示也小，从而在证明复杂度中严格区分了单项式规模与比特复杂度这两个度量。

问题
探究在 SOS 与 PCR/ℚ 证明系统中，单项式数量较小的反驳是否意味着有理系数的比特复杂度也较小，即两类复杂度度量之间的关系。
方法
构造一族布尔变量上的多项式约束 Q_n，给出度 2 的 SOS 与 PCR/ℚ 反驳，并证明任意 SOS/PCR/ℚ 反驳在二进制既约分数表示下具有指数比特复杂度下界。
评估
通过构造性证明与复杂度下界证明进行理论评估，展示 Q_n 的多项式单项式规模与指数比特复杂度可同时成立。
原文摘要（Abstract）

In this paper we consider the relationship between monomial-size and bit-complexity in Sums-of-Squares (SOS) in Polynomial Calculus Resolution over rationals (PCR/ℚ). We show that there is a set of polynomial constraints Qnover Boolean variables that has both SOS and PCR/ℚ refutations of degree 2 and thus with only polynomially many monomials, but for which any SOS or PCR/ℚ refutation must have exponential bit-complexity, when the rational coefficients are represented with their reduced fractions written in binary.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot6166,
  title = {Monomial size vs. Bit-complexity in Sums-of-Squares and Polynomial Calculus},
  author = {Tuomas Hakoniemi},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470545}
}