paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems

论 Sherali-Adams 与 Nullstellensatz 作为命题证明系统的强度
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 1/10 · 论文属于证明复杂度与代数证明系统理论，研究 Sherali-Adams 和 Nullstellensatz 相对于 Frege/Resolution 的强度，与用户关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接交集；仅与形式化验证的理论基础有非常间接的关联。引用 6 inbox
Ilario Bonacina, Maria Luisa Bonet
定理证明与证明工程逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：刻画 Sherali-Adams 与 Nullstellensatz 相对于 Frege 类系统及树状/一般 Resolution 的证明强度。

本文研究代数证明系统 Sherali-Adams (SA) 与 Nullstellensatz (NS) 相对于 Frege 类系统的强度。已知 SA 能多项式规模证明鸽巢原理，而 bounded-depth Frege 不能，因此自然的问题是 bounded-depth Frege 加入 SA 是否足以模拟 SA。作者用 Frege 风格系统刻画二者强度，证明带一元整数系数的 SA 严格位于树状 Resolution 与 Resolution 之间；并引入加权版本，证明带整数系数的加权 SA 也严格位于二者之间。对 NS，则借助双射鸽巢原理及其加权版本得到类似刻画。

问题
如何用 Frege 风格系统刻画 Sherali-Adams 与 Nullstellensatz 的证明强度，并确定它们与树状/一般 Resolution 及 bounded-depth Frege 的相对能力。
方法
通过将代数证明系统与 Frege 风格系统比较，引入带一元/整数系数以及加权版本的 SA/NS，并使用鸽巢原理及其双射变体进行分离。
评估
以多项式规模证明的模拟/分离结果衡量，证明这些系统严格位于树状 Resolution 与 Resolution 之间，并给出 NS 的类似结论。
原文摘要（Abstract）

We characterize the strength of the algebraic proof systems Sherali-Adams () and Nullstellensatz () in terms of Frege-style proof systems. Unlike bounded-depth Frege, has polynomial-size proofs of the pigeonhole principle (). A natural question is whether adding to bounded-depth Frege is enough to simulate . We show that , with unary integer coefficients, lies strictly between tree-like and tree-like Resolution. We introduce a weighted version of () and we show that with integer coefficients lies strictly between tree-like and Resolution. Analogous results are shown for using the bijective (i.e. onto and functional) pigeonhole principle and a weighted version of it.

链接与引用

DOI 原文 · DBLP

BibTeX 
@inproceedings{BonacinaB21,
  title = {On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems},
  author = {Ilario Bonacina and Maria Luisa Bonet},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533344}
}