Logic seminar

Nisan-Wigderson generators in Proof Complexity: New lower bounds

Erfan Khaniki

Institute of Mathematics

Monday, 14. March 2022 - 16:00 to 17:30

Main lecture room in the rear building at Zitna; online at https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join on zoom

A map g:{0,1}^n --> {0,1}^m (m>n) is a hard proof complexity generator for a proof system P iff for every string b in {0,1}^m\Rng(g) the formula \tau_b(g), naturally expressing b \not \in Rng(g), requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is the Nisan-Wigderson generator. Razborov (Annals of Mathematics 2015) conjectured that if A is a suitable matrix and f is a NP \cap CoNP function hard-on-average for P/poly, then NW_{f, A} is a hard proof complexity generator for Extended Frege.

In this talk, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP \cap CoNP function f that is exponentially hard for depth two AC0 circuits, NW_{f, A} is a hard proof complexity generator for AC0-Frege in a natural setting.

In this talk, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP \cap CoNP function f that is exponentially hard for depth two AC0 circuits, NW_{f, A} is a hard proof complexity generator for AC0-Frege in a natural setting.