arXiv subjects

Noel Arteche

Publications and source records attributed to Noel Arteche.

5 recordsLinked to original sources

arXiv2026

The Proof Analysis Problem for Constant-Depth Frege

We give a parallel algorithm for the Proof Analysis Problem of Arteche, Atserias, de Rezende, and Khaniki (FOCS 2025). The problem asks, given a CNF formula $φ$ on $n$ variables and a proof $π$ of a size-$s$ Resolution lower bound on $φ$, encoded as $\neg \mathrm{Ref}_s(φ)$, to extract a satisfying assignment for $φ$ when one exists. The original work gave a polynomial-time extraction algorithm for Resolution refutations that enabled a formalization of the Atserias-Müller lower bound (FOCS 2019) in Extended Frege, but it appeared inherently sequential. We devise a new algorithm that performs assignment extraction in low-depth circuit classes. Specifically, we give an assignment extraction algorithm computable by polynomial-size $\mathbf{TC}^0$ circuits and by quasipolynomial-size $\mathbf{AC}^0$ circuits, and we prove the correctness of the latter within quasipolynomial-size $\mathbf{AC}^0$-Frege. This is thanks to a new formalization of the Atserias-Müller lower bound in the relativized theory $\mathsf{T}^4_2(α)$ of bounded arithmetic, which corresponds to depth-$4$ Frege systems. This yields quasipolynomial-size $\mathbf{AC}^0$-Frege proofs for a broad class of Resolution lower bounds, making progress on a question of Pudlák. A key feature of our approach is an improved parameter regime where we get $\mathbf{AC}^0$-Frege formalizations of Resolution lower bounds $\neg \mathrm{Ref}_s(φ)$ for all $s$, including $s = n^{O(1)}$. W also show that the Proof Analysis Problem for $\mathbf{AC}^0$-Frege is $\mathbf{NP}$-hard under quasipolynomial-time reductions, which rules out certain Atserias-Müller-type approaches to the hardness of automating constant-depth Frege. Furthermore, automating $\mathbf{AC}^0$-Frege on Resolution lower bound formulas suffices to automate it on all formulas.

cs.CC↗

arXiv2026

The Proof Analysis Problem

Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula $φ$, the formula $\operatorname{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 $\operatorname{Ref}(φ)$ given a satisfying assignment of $φ$. A question that remained open is: do all short Resolution refutations of $\operatorname{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 $\operatorname{Ref}(φ)$. 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 $φ$ and a $Q$-proof of a Resolution lower bound for $φ$, encoded as $\neg \operatorname{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.

cs.CC↗

arXiv2025

Quantum Automating $\mathbf{TC}^0$-Frege Is LWE-Hard

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 $\mathbf{TC}^0$-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, $\mathbf{TC}^0$-Frege and $\mathbf{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.

cs.CC↗

arXiv2024

From Proof Complexity to Circuit Complexity via Interactive Protocols

Folklore in complexity theory suspects that circuit lower bounds against $\mathbf{NC}^1$ or $\mathbf{P}/\operatorname{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 $\mathbf{NEXP} \not\subseteq \mathbf{P}/\operatorname{poly}$, as recently observed by Pich and Santhanam (2023). We show such a connection conditionally for the Implicit Extended Frege proof system ($\mathsf{iEF}$) introduced by Krajíček (The Journal of Symbolic Logic, 2004), capable of formalizing most of contemporary complexity theory. In particular, we show that if $\mathsf{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 $\mathsf{iEF}$ proofs implies $\#\mathbf{P} \not\subseteq \mathbf{FP}/\operatorname{poly}$ (which would in turn imply, for example, $\mathbf{PSPACE} \not\subseteq \mathbf{P}/\operatorname{poly}$). Our proof exploits the formalization inside $\mathsf{iEF}$ of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan (Journal of the ACM, 1992). This has consequences for the self-provability of circuit upper bounds in $\mathsf{iEF}$. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.

cs.CC↗

arXiv2022

On the Complexity of Realizability for Safety LTL and Related Subfragments

We study the realizability problem for Safety LTL, the syntactic fragment of Linear Temporal Logic capturing safe formulas. We show that the problem is EXP-complete, disproving the existing conjecture of 2EXP-completeness. We achieve this by comparing the complexity of Safety LTL with seemingly weaker subfragments. In particular, we show that every formula of Safety LTL can be reduced to an equirealizable formula of the form $α\land \Box ψ$, where $α$ is a present formula over system variables and $ψ$ contains Next as the only temporal operator. The realizability problem for this new fragment, which we call $\mathsf{GX}_{\mathsf{0}}$, is also EXP-complete.

cs.LO↗