2025/06/20 by Arteche, Noel, Atserias, Albert, de Rezende, Susanna F. +1
Computer Science · #Complexity and Algorithms in Graphs #Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2506.16956
openalex publication_date 2025/06/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula φ, the formula Ref(φ), stating "φ has small Resolution refutations", does not have subexponential-size Resolution refutations. Conversely, when φ is satisfiable, Pudlák (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of Ref(φ) given a satisfying assignment of φ. A question that remained open is: do all short Resolution refutations of Ref(φ) explicitly leak a satisfying assignment of φ? We answer this question affirmatively by giving a polynomial-time algorithm that extracts a satisfying assignment for φ given any short Resolution refutation of Ref(φ). The algorithm follows from a new feasibly constructive proof of the Atserias-Müller lower bound, formalizable in Cook's theory PV1 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 φ and a Q-proof of a Resolution lower bound for φ, encoded as ¬ Ref(φ), whether φ 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.