Metamathematics of Resolution Lower Bounds: A TFNP Perspective

TL;DR

A new class of decision-tree problems in decision-tree $\mathsf{TFNP}$ is introduced, which can be seen as a randomized version of $\mathsf{PLS}$, and it is argued that this class effectively captures the metamathematics of proving resolution lower bounds.

Abstract

This paper studies the *refuter* problems, a family of decision-tree $\mathsf{TFNP}$ problems capturing the metamathematical difficulty of proving 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 $π$ in $P$ that claims to have proved $\varphi$, and our goal is to find an invalid derivation inside $π$. As suggested by witnessing theorems in bounded arithmetic, the *computational complexity* of these refuter problems is closely tied to the *metamathematics* of the underlying proof complexity lower bounds. We focus on refuter problems corresponding to lower bounds for *resolution*, which is arguably the single most studied system in proof complexity. 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}$, and argue that this class effectively captures the metamathematics of proving resolution lower bounds. We view these results as a contribution to the *bounded reverse mathematics* of complexity lower bounds: when interpreted in relativized bounded arithmetic, our results show that the theory $\mathsf{T}^1_2(α) + \mathrm{dwPHP}(\mathsf{PV}(α))$ characterizes the "reasoning power" required to prove (the "easiest") resolution lower bounds. An intriguing corollary of our results is that the combinatorial principle, "the pigeonhole principle requires exponential-size resolution proofs", captures the class of $\mathsf{TFNP}$ problems whose totality is provable in $\mathsf{T}^1_2 + \mathrm{dwPHP}(\mathsf{PV})$.

Figures (5)

• Figure 1: Translations of the main results in different languages. A one-way arrow represents an implication, and a two-way arrow indicates an equivalence.
• Figure 2: The $\mathrm{rwPHP}(\PLS)$ instance constructed from $\textsc{Refuter}(s(\mathrm{PHP}_{(n+1)\to n}\vdash_\mathsf{Res} \bot) \le c^n)$.
• Figure 3: The brute-force resolution proof for a CNF $F = C_1 \land C_2 \land C_3 \land C_4$ when $n = 3$.
• Figure 4: The gadget to embed an $\mathrm{rwPHP}(\PLS)$ instance.
• Figure 5: An illustration of our reduction from $\mathrm{rwPHP}(\PLS)$ to the size refuter problem. All gray arrows are valid resolution derivations (and the last layer is weakening from axioms). Every dashed box uses the gadget to embed an $\mathrm{rwPHP}(\PLS)$ instance that enforces every layer to have at most $2M$ clauses. Thus the only possible invalid derivations are those inside the gadget which, once found, would directly imply a solution of the original $\mathrm{rwPHP}(\PLS)$ instance. The overall reduction will produce a purported resolution refutation of size $O(nLM+|F|)$.

Theorems & Definitions (117)

• Example 1.2
• Remark 1: Why resolution?
• Theorem 1.3: Main Result; Informal
• Remark 2: Type-$1$ vs. Type-$2$ $\TFNP$ Problems
• Remark 3: Further motivations for refutation of width lower bounds
• Remark 4: How Strong is $\mathrm{rwPHP}(\PLS)$?
• Remark 5: Uniform vs. non-uniform reductions
• Theorem 1.4: Informal version of \ref{['thm: refuting Res lb for PHP is in rwPHP(PLS)']}
• Theorem 1.5: Informal version of \ref{['thm: rwPHP(PLS)-hardness of refuters']}
• Remark 6