证明复杂性和Kneser-Lovász定理
Proof Complexity and the Kneser-Lovász Theorem
摘要：
我们研究了一类命题公式的证明复杂性，这些公式表达了一个被称为Kneser-Lovász定理的组合原理。这是一个命题重言式族，由一个非负整数参数$k$索引，它推广了鸽子洞原理（为$k=1$获得）。我们表明，对于所有固定的$k$，$2^{Ω(n)}$下界分辨率的复杂性和指数下界有界深度弗雷格证明。这些结果甚至适用于更严格的一类公式编码Schrijver的加强Kneser-Lovász定理。另一方面，对于$k=2,3$（Kneser-Lovász定理的组合证明是已知的）的情况下，我们给出多项式大小的弗雷格（$k=2$），分别扩展弗雷格（$k=3$）的证明。本文最后简要宣布了Kneser-Lovász定理一般情况下证明复杂性的结果（在随后的工作中提出）。
英文摘要：
We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovász Theorem. This is a family of propositional tautologies, indexed by an nonnegative integer parameter $k$ that generalizes the Pigeonhole Principle (obtained for $k=1$). We show, for all fixed $k$, $2^{Ω(n)}$ lower bounds on resolution complexity and exponential lower bounds for bounded depth Frege proofs. These results hold even for the more restricted class of formulas encoding Schrijver's strenghtening of the Kneser-Lovász Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the Kneser-Lovász Theorem are known) we give polynomial size Frege ($k=2$), respectively extended Frege ($k=3$) proofs. The paper concludes with a brief announcement of the results (presented in subsequent work) on the proof complexity of the general case of the Kneser-Lovász theorem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
