Short Proofs of the Kneser-Lov\'asz Coloring Principle

TL;DR

This paper presents polynomial and quasi-polynomial size propositional proofs for the Kneser-Lovász theorem using a new combinatorial counting proof that bypasses topological methods, with an open question about a related lemma.

Contribution

It introduces a new counting-based combinatorial proof for the Kneser-Lovász theorem and establishes proof size bounds in propositional proof systems.

Findings

Polynomial size extended Frege proofs for propositional translations.

Quasi-polynomial size Frege proofs for propositional translations.

Open problem regarding the propositional proof size of the truncated Tucker lemma.

Abstract

We prove that the propositional translations of the Kneser-Lov\'asz 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\'asz 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.