Title: Proof Complexity and the Kneser-Lov\'asz Theorem
Abstract:We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovasz Theorem. This is a family of propositional tautologies, indexed...We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovasz 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^{\Omega(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-Lovasz Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the Kneser-Lovasz 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-Lovasz theorem.Read More
Publication Year: 2014
Publication Date: 2014-02-18
Language: en
Type: preprint
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot