The Proof Analysis Problem

Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$ stating that “$\varphi$ has small Resolution refutations"-does not have subexponential-size Resolution refutations. Conversely, when $\varphi$ is satisfiable, Pudlák (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of $\operatorname{REF}(\varphi)$ given a satisfying assignment of $\varphi$. A question that had remained open is: do all short Resolution refutations of $\operatorname{Ref}(\varphi)$ explicitly leak a satisfying assignment of $\varphi$?We answer this question affirmatively by providing a polynomial-time algorithm that extracts a satisfying assignment for $\varphi$ given any short Resolution refutation of $\operatorname{REF}(\varphi)$. The algorithm follows from a new feasibly constructive proof of the Atserias-Müller lower bound, formalizable in Cook’s theory PV1of bounded arithmetic. This implies that Extended Frege can efficiently prove (a suitable formalization of the statement) that automating Resolution is NP-hard.Motivated by this algorithm, we introduce a new metacomputational problem concerning Resolution lower bounds: the Proof Analysis Problem (PAP). For a fixed proof system Q, the Proof Analysis Problem for Q asks, given a CNF formula $\varphi$ and a Q-proof of a Resolution lower bound for $\varphi$, encoded as $\neg \boldsymbol{REF}(\varphi)$, whether $\varphi$ is satisfiable. In contrast to the Proof Analysis Problem for Resolution, which is in P, we prove that PAP for Extended Frege (EF) is NP-complete. In particular, EF can prove Resolution lower bounds on satisfiable formulas without necessarily revealing a satisfying assignment.Our results yield new insights into proof search and the meta-mathematics of Resolution lower bounds: (i) for every proof system that simulates EF as well as for Resolution, the system is (weakly) automatable if and only if it can be (weakly) automated exclusively on formulas stating Resolution lower bounds; (ii) we provide explicit Ref formulas that are exponentially hard for bounded-depth Frege systems; and (iii) for every strong enough theory of arithmetic T we construct explicit unsatisfiable CNF formulas that are exponentially hard for Resolution but for which T cannot prove even a quadratic Resolution lower bound. This latter result applies to arbitrarily strong theories like PA or ZFC, and does not require any complexity-theoretic assumptions.