next up previous
Next: About this document ...

Tree-Resolution complexity of the Weak Pigeon-Hole Principle1

Stefan Dantchev2
Dept. of Mathematics and Computer Science, University of Leicester
Søren Riis
Dept. of Computer Science, Queen Mary, University of London


We show some tight results about the tree-resolution complexity of the Weak Pigeon-Hole Principle, $PHP_{n}^{m}$ . We prove that any optimal tree-resolution proof of $PHP_{n}^{m}$ is of size $2^{\theta \left(n\log n\right)}$ , independently from $m$ , even if it is infinity. So far, the lower bound know has been $2^{\Omega \left(n\right)}$ . We also show that any, not necessarily optimal, regular tree-resolution proof $PHP_{n}^{m}$ is bounded by $2^{O\left(n\log m\right)}$ . To best of our knowledge, this is the first time, worst-case proofs have been considered, and a non-trivial upper bound has been proven. Finally, we discuss and conjecture some refinements of Riis' Complexity Gap theorem for tree-resolution complexity of Second Order Existential ($SO\exists $ ) sentences of predicate logic.

Keywords Propositional Proof Complexity, Tree-Resolution, Weak Pigeon-Hole Principle

AMS Subject Classification 03F20, 68Q17


S. Dantchev 2002-12-11