Inscriere cercetatori

Site nou !

Daca nu va puteti recupera parola (sau aveti alte probleme), scrieti-ne la pagina de contact. Situl vechi se gaseste la adresa


Proof complexity and the Lovasz-Kneser Theorem

Domenii publicaţii > Ştiinţe informatice + Tipuri publicaţii > Articol în volumul unei conferinţe

Autori: Gabriel Istrate, Adrian Craciun

Editorial: Lecture Notes in Computer Science, Springer Verlag, Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), vol. 8561 , p.138-153, 2014.


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 (PHP, 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 strengthening 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 discussion of the results (that will be presented in a subsequent paper) on the complexity of the general case of the Kneser-Lovasz theorem.

A free preliminary version is available at

Cuvinte cheie: combinatorial topology, resolution complexity, Frege proofs