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.

Abstract We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate $${\rm TC}^0$$ TC 0 -Frege. This extends the line of results of Krajííček and Pudlík( Information and Computation , 1998), Bonet, Pitassi, and Raz ( SIAM Journal on Computing , 2000),and Bonet, Domingo, Gavaldá, Maciel, and Pitassi ( Computational Complexity, 2004 ), who showed that ExtendedFrege, $${\rm TC}^0$$ TC 0 -Frege and $${\rm AC}^0$$ AC 0 -Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.

The complexity class CLS was introduced by Daskalakis and Papadimitriou (SODA 2010) to capture the computational complexity of important TFNP problems solvable by local search over continuous domains and, thus, lying in both PLS and PPAD. It was later shown that, e.g., the problem of computing fixed points guaranteed by Banach’s fixed point theorem is CLS-complete by Daskalakis et al. (STOC 2018). Recently, Fearnley et al. (J. ACM 2023) disproved the plausible conjecture of Daskalakis and Papadimitriou that CLS is a proper subclass of PLS∩PPAD by proving that CLS = PLS∩PPAD. To study the possibility of other collapses in TFNP, we connect classes formed as the intersection of existing subclasses of TFNP with the phenomenon of feasible disjunction in propositional proof complexity; where a proof system has the feasible disjunction property if, whenever a disjunction F ∨ G has a small proof, and F and G have no variables in common, then either F or G has a small proof. Based on some known and some new results about feasible disjunction, we separate the classes formed by intersecting the classical subclasses PLS, PPA, PPAD, PPADS, PPP and CLS. We also give the first examples of proof systems which have the feasible interpolation property, but not the feasible disjunction property.

Folklore in complexity theory suspects that circuit lower bounds against NC1 or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [58]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [45], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [54]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.

We study the realizability and strong satisfiability problems for SAFETY LTL, a syntactic fragment of Linear Temporal Logic ([Formula presented]) capturing safe formulas. While it is well-known that realizability for this fragment lies in [Formula presented], the best-known lower bound is [Formula presented]-hardness. Surprisingly, closing this gap has proven an elusive task. Previous works have claimed first [Formula presented]-completeness [1] and later [Formula presented]-completeness [2] for this problem, but both of these proofs turned out to be incorrect. We revisit the problem of the exact classification of the complexity of realizability for [Formula presented] through the lens of seemingly weaker fragments. While we cannot settle the question for [Formula presented], we study a subfragment of it consisting of formulas of the form [Formula presented], where α is a present formula over system variables and ψ contains Next as the only temporal operator. We prove that the realizability problem for this new fragment, which we call [Formula presented], is [Formula presented]-complete, and observe that this fragment is equirealizable to existing more expressive fragments, such as the class [Formula presented] [3]. Furthermore, we revisit the techniques used in the purported proof of [Formula presented]-completeness of Arteche and Hermo [1], and observe that, while incorrect in their original claims, their proofs can be modified to classify the complexity of strong satisfiability, a necessary condition for realizability introduced by Kupferman, Sadigh, and Seshia [4]. We prove that, with regards to strong satisfiability, the fragments [Formula presented] and [Formula presented] are in fact equivalent under polynomial-time many-one reductions.