Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds

TL;DR

This paper explores the computational complexity of refuter problems related to proof lower bounds in resolution, introducing new classes and showing how they relate to bounded arithmetic theories, leading to efficient proofs of lower bounds.

Contribution

It introduces a new class $ ext{rwPHP}( ext{PLS})$ for resolution refuter problems and links their complexity to bounded arithmetic, enabling more efficient proofs of resolution lower bounds.

Findings

Defined a new class $ ext{rwPHP}( ext{PLS})$ in decision-tree $ ext{TFNP}$.

Connected the complexity of refuter problems to theories in bounded arithmetic.

Proved many resolution lower bounds can be established in low-width random resolution.

Abstract

We study the *refuter* problems for proof complexity lower bounds. Suppose $\varphi$ is a hard tautology that does not admit any length-$s$ proof in some proof system $P$. In the corresponding refuter problem, we are given (query access to) a purported length-$s$ proof $\pi$ in $P$ that claims to have proved $\varphi$, and our goal is to find an invalid derivation step within $\pi$. As suggested by witnessing theorems in bounded arithmetic, the *computational complexity* of these refuter problems is closely tied to the *metamathematics* of the underlying lower bounds. We focus on refuter problems corresponding to lower bounds for *resolution*, which is arguably the single most studied system in proof complexity. To capture the complexity of refuter problems for resolution *size* lower bounds, we introduce a new class $\mathrm{rwPHP}(\mathsf{PLS})$ in decision-tree $\mathsf{TFNP}$, which can be seen as a randomized version of $\mathsf{PLS}$. Interpreted in bounded arithmetic, our results show that the theory $\mathsf{T}^1_2(\alpha) + \mathrm{dwPHP}(\mathsf{PV}(\alpha))$ characterizes the "reasoning power" required to prove (the "easiest") resolution size lower bounds. As a corollary, we obtain surprisingly efficient proofs of resolution lower bounds. In particular, we show that many resolution size lower bounds can be proved in low-width *random resolution* [Pudl\'ak--Thapen, CCC'17].