Atserias and Müller (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á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 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üller 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.

翻译：Atserias 和 Müller (JACM, 2020) 证明了对于每个不可满足的 CNF 公式 $\varphi$，陈述“$\varphi$ 具有小规模消解反驳”的公式 $\operatorname{Ref}(\varphi)$ 没有亚指数规模的消解反驳。相反，当 $\varphi$ 可满足时，Pudlák (TCS, 2003) 展示了如何根据 $\varphi$ 的一个满足赋值构造 $\operatorname{Ref}(\varphi)$ 的多项式规模消解反驳。一个尚待解决的问题是：$\operatorname{Ref}(\varphi)$ 的所有短消解反驳是否显式泄露 $\varphi$ 的一个满足赋值？我们给出肯定回答，通过提供一个多项式时间算法，该算法在给定 $\operatorname{Ref}(\varphi)$ 的任意短消解反驳时，提取出 $\varphi$ 的一个满足赋值。该算法源自 Atserias-Müller 下界的一个新的可行构造性证明，可在 Cook 的有界算术理论 $\mathsf{PV_1}$ 中形式化。受此启发，我们引入一个关于消解下界的计算问题：证明分析问题 (PAP)。对于证明系统 $Q$，$Q$ 的证明分析问题要求：给定一个 CNF 公式 $\varphi$ 以及一个关于 $\varphi$ 的消解下界（编码为 $\neg \operatorname{Ref}(\varphi)$）的 $Q$-证明，判断 $\varphi$ 是否可满足。与消解系统的 PAP 形成对比，我们证明扩展弗雷格系统 (EF) 的 PAP 是 NP 完全的。我们的结果为证明复杂性提供了新见解：(i) 每个模拟 EF 的证明系统是（弱）可自动化的，当且仅当它在陈述消解下界的公式上是（弱）可自动化的；(ii) 我们提供了对有界深度弗雷格系统指数级难的 Ref 公式；(iii) 对于每个足够强的算术理论 $T$，我们构造了对于消解系统指数级难的不可满足 CNF 公式，但 $T$ 甚至无法证明其二次下界。