Overview
This work addresses a problem related to the analysis of Resolution refutations and introduces a new computational problem called the Proof Analysis Problem (PAP). It confirms that all short Resolution refutations of $\operatorname{Ref}(\varphi)$, a formula stating that $\varphi$ has small Resolution refutations, explicitly leak a satisfying assignment for $\varphi$. The authors developed a polynomial-time algorithm for this extraction, which stems from a new feasibly constructive proof of the Atserias-Müller lower bound. The lower bound proof is formalizable within Cook's theory $\mathsf{PV_1}$ of bounded arithmetic.
The Proof Analysis Problem (PAP) is defined for a proof system $Q$. For a given CNF formula $\varphi$ and a $Q$-proof encoded as $\neg \operatorname{Ref}(\varphi)$ (a Resolution lower bound for $\varphi$), PAP asks whether $\varphi$ is satisfiable. While PAP for Resolution is addressed by the extraction algorithm, the research establishes that PAP for Extended Frege (EF) is NP-complete.
Research Context
Prior work by Atserias and Müller (2020) demonstrated that for any unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$ does not possess subexponential-size Resolution refutations. Conversely, Pudlák (2003) showed that if $\varphi$ is satisfiable, a polynomial-size Resolution refutation of $\operatorname{Ref}(\varphi)$ can be constructed from a satisfying assignment of $\varphi$. A question that remained open concerned whether all short Resolution refutations of $\operatorname{Ref}(\varphi)$ implicitly reveal a satisfying assignment for $\varphi$. This current research directly answers that question.
Approach
The core of the research involves the development of a polynomial-time algorithm. This algorithm is designed to extract a satisfying assignment for a CNF formula $\varphi$ when provided with any short Resolution refutation of $\operatorname{Ref}(\varphi)$. The algorithm's foundation is a novel feasibly constructive proof for the Atserias-Müller lower bound. This proof is described as being formalizable within Cook's theory $\mathsf{PV_1}$ of bounded arithmetic. The explicit construction of this algorithm and the formalization within $\mathsf{PV_1}$ contribute to answering the open question regarding the leakage of satisfying assignments.
In addition to the algorithmic approach, the researchers introduced and analyzed the Proof Analysis Problem (PAP). This problem is conceptualized for a generic proof system $Q$. Their methodology involved contrasting the computational complexity of PAP for different proof systems, specifically Resolution and Extended Frege (EF).
Findings
- A polynomial-time algorithm exists that extracts a satisfying assignment for a CNF formula $\varphi$ from any short Resolution refutation of $\operatorname{Ref}(\varphi)$. This affirmatively answers the question regarding the explicit leakage of satisfying assignments.
- The algorithm is derived from a new feasibly constructive proof of the Atserias-Müller Resolution lower bound, which is formalizable in Cook's theory $\mathsf{PV_1}$.
- The Proof Analysis Problem (PAP) for Extended Frege (EF) is NP-complete. This contrasts with PAP for Resolution, for which the developed algorithm provides a solution.
- The research suggests that any proof system simulating EF is (weakly) automatable if and only if it is (weakly) automatable on formulas that express Resolution lower bounds.
- Formulas of the $\operatorname{Ref}$ type are exponentially hard for bounded-depth Frege systems.
- For every sufficiently strong theory of arithmetic $T$, there exist unsatisfiable CNF formulas that are exponentially hard for Resolution, yet $T$ cannot prove even a quadratic lower bound for these formulas.
Why This Matters
These findings offer new insights into proof complexity. They establish a fundamental connection between the structure of short Resolution refutations for hardness statements and the satisfiability of the underlying CNF formulas. The introduction and analysis of the Proof Analysis Problem provide a new framework for understanding the computational properties of different proof systems, particularly concerning their ability to analyze lower bound proofs. The results regarding automation and the hardness of $\operatorname{Ref}$ formulas for Frege systems contribute to the theoretical understanding of proof complexity boundaries.
Potential Applications
- The developed algorithm could potentially be applied in scenarios where short Resolution refutations of $\operatorname{Ref}(\varphi)$ are available, allowing for the extraction of satisfying assignments.