Abstrakt
A map g : {0, 1}n RIGHTWARDS ARROW {0, 1}m (m > n) is a hard proof complexity generator for a proof system P iff for every string b ELEMENT OF {0, 1}m \ Rng(g), formula τb(g) naturally expressing b NOT AN ELEMENT OF 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 [37] conjectured that if A is a suitable matrix and f is a NP INTERSECTION CoNP function hard-on-average for P/poly, then NWf,A is a hard proof complexity generator for Extended Frege. In this paper, we prove a form of Razborov's conjecture for AC0-Frege.
We show that for any symmetric NP INTERSECTION CoNP function f that is exponentially hard for depth two AC0 circuits, NWf,A is a hard proof complexity generator for AC0-Frege in a natural setting. As direct applications of this theorem, we show that: 1.
For any f with the specified properties, τb(NWf,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) AC0-Frege proofs. 2. Certain formalizations of the principle fn NOT AN ELEMENT OF (NP INTERSECTION CoNP)/poly requires superpolynomial AC0-Frege proofs.
These applications relate to two questions that were asked by Krajíček [21].