$P \ne NP$, propositional proof complexity, and resolution lower bounds for the weak pigeonhole principle

TL;DR

This paper discusses recent exponential lower bounds on Resolution proof lengths for the weak pigeonhole principle, highlighting implications for propositional formulations of the $P e NP$ problem and proof complexity.

Contribution

It presents new exponential lower bounds for Resolution proofs of the weak pigeonhole principle and explores their implications for propositional proof complexity related to $P e NP$.

Findings

Resolution proofs for the weak pigeonhole principle require exponential length

Certain propositional formulations of $P e NP$ lack short Resolution proofs

Connections established between proof complexity and $P e NP$ hardness

Abstract

Recent results established exponential lower bounds for the length of any Resolution proof for the weak pigeonhole principle. More formally, it was proved that any Resolution proof for the weak pigeonhole principle, with $n$ holes and any number of pigeons, is of length $\Omega(2^{n^{\epsilon}})$, (for a constant $\epsilon = 1/3$). One corollary is that certain propositional formulations of the statement $P \ne NP$ do not have short Resolution proofs. After a short introduction to the problem of $P \ne NP$ and to the research area of propositional proof complexity, I will discuss the above mentioned lower bounds for the weak pigeonhole principle and the connections to the hardness of proving $P \ne NP$.