Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2611.08305

The Proof Analysis Problem for Constant-Depth Frege

Noel Arteche·Susanna F. de Rezende·Erfan Khaniki·Kilian Risse
View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.CC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Noel Arteche, Susanna F. de Rezende, Erfan Khaniki, Kilian Risse. 2026-11-05. The Proof Analysis Problem for Constant-Depth Frege. https://arxiv.org/abs/2611.08305

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A note on a problem in communication complexity

We study bounded-error randomization and majority operators in structural communication complexity. We give a communication-complexity formulation of Tarui's theorem and identify the bounded-error closure of weakly unbounded-error communication with a distributional perturbation of logarithmic margin complexity. Retaining the Boolean guarantee in Tarui's probabilistic polynomials yields the stronger inclusion $\mathsf{PH}^{\mathrm{cc}} \subseteq \mathsf{ZP}\mathbin{\cdot} \mathsf{PP}^{\mathrm{cc}} \subseteq \mathsf{BP}\mathbin{\cdot} \mathsf{PP}^{\mathrm{cc}}$. We also define a majority operator satisfying $\mathsf{PP}\mathbin{\cdot} \mathsf{P}^{\mathrm{cc}} = \mathsf{PP}^{\mathrm{cc}}$ and use Sasaki's majority formula to prove that $\mathord{\oplus}\mathsf{P}^{\mathrm{cc}} \subseteq \mathsf{PP}\mathbin{\cdot} \mathsf{PP}^{\mathrm{cc}}$. For the inner-product function modulo two, both the outer index and each inner protocol have logarithmic cost. Together with Forster's lower bound, this gives an explicit witness to the non-idempotence of the majority operator and to $\mathsf{PP}\mathbin{\cdot} \mathsf{PP}^{\mathrm{cc}} \not\subseteq \mathsf{UPP}^{\mathrm{cc}}$. Both the bounded-error closure and the two-level majority class are contained in $\mathsf{PSPACE}^{\mathrm{cc}}$.

cs.CC↗
arXiv2026

High Precision Multiplicative-Error Approximation of $\#$SAC$^1$ Functions in Logspace Uniform AC$^1$

We show that approximations of $\#\mathsf{SAC}^1$ functions (i.e. functions computed by logspace-uniform polynomial-size positive semi-unbounded arithmetic circuits of depth $O(\log n)$) can be computed in logspace uniform $\mathsf{AC}^1$ (denoted as $\mathsf{L}\text{-}\mathsf{AC}^1$) with multiplicative error $2^{-\operatorname{poly}\log n}$.Previously, approximations of $\#\mathsf{SAC}^1$ functions were known to be in logspace-uniform $\mathsf{TC}^1$ via exact computation given by Allender, Jiao, Mahajan, and Vinay (TCS'98). A main corollary of our result is that the following models beyond $\mathsf{BPL}$ are computable by $\mathsf{L}\text{-}\mathsf{AC}^1$ with multiplicative error $2^{-\operatorname{poly}\log n}$: - Probabilistic Auxiliary Push-down Machines (Probabilistic $\mathsf{AuxPDM}$s), which are polynomial time logspace Turing Machines (TMs) with an auxiliary stack having unbounded size and a read-once random tape; - Read-$k$ Probabilistic TMs with polynomial time and logarithmic space, where $k$ is a constant and Read-$k$ means the random tape is two-way accessible and each cell can be visited for at most $k$ times. Notice that this is a direct generalization and improvement for $\mathsf{BPL}\subseteq\mathsf{L}\text{-}\mathsf{AC}^1$ of Cheng and Wang (CCC'24), and the approximation error is improved from additive reverse polynomial to multiplicative reverse quasi-polynomial. $\mathsf{AuxPDM}$ was introduced by Cook (JACM'71) and its probabilistic version was first studied by Macarie and Ogihara (TCS'98). Read-$k$ Probabilistic logspace TMs was studied by Impagliazzo, Nisan, Wigderson (STOC'94) where a pseudorandom generator for this model was given. We mention that multiplicative error approximations are stronger than additive error approximations in the sense that they can even be used to decide non-deterministic computations.

cs.CC↗
arXiv2026

Two-colour crossing minimization in complete geometric graphs is NP-hard

Given a fixed straight-line drawing of a complete graph, we seek a two-colouring of its edges that minimizes monochromatic crossing pairs. We prove that the threshold decision problem is NP-complete, even for points in general position with integer coordinates. Thus exact minimization is NP-hard, resolving the complexity question posed at the Crossing Number Workshop in 2019. We reduce from MaxCut on permutation graphs by representing source vertices with classes of geometric edges, whose crossings encode source adjacencies. The target complete graph also contains every other edge between its points, and their freely chosen colours can affect the encoded cost. To control these interactions, we construct a large comparison grid with two stable colour phases and use program points to turn this reference into colour preferences on other edges. The optimum differs from a computable baseline plus the amplified minimum number of uncut source edges by an error small enough to distinguish consecutive source values. The reduction is deterministic, with polynomially many points and polynomial coordinate bit length.

cs.CC↗