Abstract
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 Pproofs. One of the wellstudied maps in the theory of proof complexity generators is NisanWigderson generator. Razborov [A. A. {Razborov}, 2015] conjectured that if A is a suitable matrix and f is a NP∩CoNP function hardonaverage 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 1o(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].
BibTeX  Entry
@InProceedings{khaniki:LIPIcs.CCC.2022.17,
author = {Khaniki, Erfan},
title = {{NisanWigderson Generators in Proof Complexity: New Lower Bounds}},
booktitle = {37th Computational Complexity Conference (CCC 2022)},
pages = {17:117:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772419},
ISSN = {18688969},
year = {2022},
volume = {234},
editor = {Lovett, Shachar},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16579},
URN = {urn:nbn:de:0030drops165799},
doi = {10.4230/LIPIcs.CCC.2022.17},
annote = {Keywords: Proof complexity, Bounded arithmetic, Bounded depth Frege, NisanWigderson generators, Metacomplexity, Lower bounds}
}
Keywords: 

Proof complexity, Bounded arithmetic, Bounded depth Frege, NisanWigderson generators, Metacomplexity, Lower bounds 
Collection: 

37th Computational Complexity Conference (CCC 2022) 
Issue Date: 

2022 
Date of publication: 

11.07.2022 