2026-07-24T08:01:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16579 2024-03-06T10:57:51Z ddc:004 open_access

Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds Khaniki, Erfan Proof complexity Bounded arithmetic Bounded depth Frege Nisan-Wigderson generators Meta-complexity Lower bounds A map g:{0,1}ⁿ → {0,1}^m (m > n) is a hard proof complexity generator for a proof system P iff for every string b ∈ {0,1}^m ⧵ Rng(g), formula τ_b(g) naturally expressing b ∉ Rng(g) requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is Nisan-Wigderson generator. Razborov [A. A. {Razborov}, 2015] conjectured that if A is a suitable matrix and f is a NP∩CoNP function hard-on-average for 𝖯/poly, then NW_{f, A} is a hard proof complexity generator for Extended Frege. In this paper, we prove a form of Razborov’s conjecture for AC⁰-Frege. We show that for any symmetric NP∩CoNP function f that is exponentially hard for depth two AC⁰ circuits, NW_{f,A} is a hard proof complexity generator for AC⁰-Frege in a natural setting. As direct applications of this theorem, we show that: 1) For any f with the specified properties, τ_b(NW_{f,A}) (for a natural formalization) based on a random b and a random matrix A with probability 1-o(1) is a tautology and requires superpolynomial (or even exponential) AC⁰-Frege proofs. 2) Certain formalizations of the principle f_n ∉ (NP∩CoNP)/poly requires superpolynomial AC⁰-Frege proofs. These applications relate to two questions that were asked by Krajíček [J. {Krajíček}, 2019]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Erfan Khaniki 2022 Is Part Of LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2022.17 urn:nbn:de:0030-drops-165799 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.17 eng https://creativecommons.org/licenses/by/4.0/legalcode