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 Refₛ(φ), 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 TC⁰ circuits and by quasipolynomial-size AC⁰ circuits, and we prove the correctness of the latter within quasipolynomial-size AC⁰-Frege. This is thanks to a new formalization of the Atserias-Müller lower bound in the relativized theory T⁴₂(α) of bounded arithmetic, which corresponds to depth-$4$ Frege systems. This yields quasipolynomial-size AC⁰-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 AC⁰-Frege formalizations of Resolution lower bounds Refₛ(φ) for all s, including s = nO(1). W also show that the Proof Analysis Problem for AC⁰-Frege is 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 AC⁰-Frege on Resolution lower bound formulas suffices to automate it on all formulas.