Abstract
We prove that the propositional translations of the Kneser-Lovász theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs. We present a new counting-based combinatorial proof of the Kneser-Lovász theorem that avoids the topological arguments of prior proofs for all but finitely many cases for each k. We introduce a miniaturization of the octahedral Tucker lemma, called the truncated Tucker lemma: it is open whether its propositional translations have (quasi-)polynomial size Frege or extended Frege proofs.
J. Aisenberg—Supported in part by NSF grants DMS-1101228 and CCF-1213151.
M.L. Bonet—Supported in part by grant TIN2013-48031-C4-1.
S. Buss—Supported in part by NSF grants DMS-1101228 and CCF-1213151, and Simons Foundation award 306202.
A. Crãciun and G. Istrate—Supported in part by IDEI grant PN-II-ID-PCE-2011-3-0981“Structure and computational difficulty in combinatorial optimization: an interdisciplinary approach”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aisenberg, J., Bonet, M.L., Buss, S.R.: Quasi-polynomial size Frege proofs of Frankl’s theorem on the trace of finite sets (201?) (to appear in Journal of Symbolic Logic)
Bonet, M.L., Buss, S.R., Pitassi, T.: Are there hard examples for Frege systems? In: Clote, P., Remmel, J. (eds.) Feasible Mathematics II, pp. 30–56. Birkhäuser, Boston (1995)
Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic 52, 916–927 (1987)
Buss, S.R.: Propositional proof complexity: An introduction. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic, pp. 127–178. Springer, Berlin (1999)
Buss, S.R.: Towards NP-P via proof complexity and proof search. Annals of Pure and Applied Logic 163(9), 1163–1182 (2012)
Buss, S.R.: Quasipolynomial size proofs of the propositional pigeonhole principle (2014) (submitted for publication)
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44, 36–50 (1979)
Istrate, G., Crãciun, A.: Proof complexity and the Kneser-Lovász theorem. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 138–153. Springer, Heidelberg (2014)
Jeřábek, E.: Dual weak pigeonhole principle, boolean complexity, and derandomization. Annals of Pure and Applied Logic 124, 1–37 (2004)
Krajíček, J.: Bounded Arithmetic. Propositional Calculus and Complexity Theory. Cambridge University Press, Heidelberg (1995)
Lovász, L.: Kneser’s conjecture, chromatic number, and homotopy. Journal of Combinatorial Theory, Series A 25(3), 319–324 (1978)
Matoušek, J.: A combinatorial proof of Kneser’s conjecture. Combinatorica 24(1), 163–170 (2004)
Segerlind, N.: The complexity of propositional proofs. Bulletin of Symbolic Logic 13(4), 417–481 (2007)
Ziegler, G.M.: Generalized Kneser coloring theorems with combinatorial proofs. Inventiones Mathematicae 147(3), 671–691 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aisenberg, J., Bonet, M.L., Buss, S., Crãciun, A., Istrate, G. (2015). Short Proofs of the Kneser-Lovász Coloring Principle. In: Halldórsson, M., Iwama, K., Kobayashi, N., Speckmann, B. (eds) Automata, Languages, and Programming. ICALP 2015. Lecture Notes in Computer Science(), vol 9135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47666-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-47666-6_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47665-9
Online ISBN: 978-3-662-47666-6
eBook Packages: Computer ScienceComputer Science (R0)