The Proof Analysis Problem

Abstract

Atserias and M\"uller (JACM, 2020) proved that for every unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$, stating "$\varphi$ has small Resolution refutations", does not have subexponential-size Resolution refutations. Conversely, when $\varphi$ is satisfiable, Pudl\'ak (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of $\operatorname{Ref}(\varphi)$ given a satisfying assignment of $\varphi$. A question that 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 giving 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\"uller lower bound, formalizable in Cook's theory $\mathsf{PV_1}$ of bounded arithmetic. Motivated by this, we introduce a computational problem concerning Resolution lower bounds: the Proof Analysis Problem (PAP). For a 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 \operatorname{Ref}(\varphi)$, whether $\varphi$ is satisfiable. In contrast to PAP for Resolution, we prove that PAP for Extended Frege (EF) is NP-complete. Our results yield new insights into proof complexity: (i) every proof system simulating EF is (weakly) automatable if and only if it is (weakly) automatable on formulas stating Resolution lower bounds; (ii) we provide Ref formulas exponentially hard for bounded-depth Frege systems; and (iii) for every strong enough theory of arithmetic $T$ we construct unsatisfiable CNF formulas exponentially hard for Resolution but for which $T$ cannot prove even a quadratic lower bound.