Nisan-Wigderson Generators in Proof Complexity: New 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].
Proof complexity
Bounded arithmetic
Bounded depth Frege
Nisan-Wigderson generators
Meta-complexity
Lower bounds
Theory of computation~Proof complexity
Theory of computation~Complexity theory and logic
17:1-17:15
Regular Paper
This work was supported by the GACR grant 19-27871X, the institute grant RVO: 67985840, and the Specific university research project SVV-2020-260589. Part of this work was done while the author was participating in the program Satisfiability: Theory, Practice, and Beyond at the Simons Institute for the Theory of Computing.
We are grateful to Jan Bydžovský, Susanna de Rezende, Emil Jeř{á}bek, Jan Krajíček, Jan Pich and Pavel Pudlák for their different forms of help in different stages of this work. We are also indebted to anonymous referees for their helpful suggestions, which led to a better presentation of the paper.
Erfan
Khaniki
Erfan Khaniki
Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic
Institute of Mathematics of the Czech Academy of Sciences, Prague, Czech Republic
https://orcid.org/0000-0002-5843-7315
10.4230/LIPIcs.CCC.2022.17
M. Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14(4):417-433, 1994.
M. Alekhnovich, E. Ben-Sasson, A. A. Razborov, and A. Wigderson. Pseudorandom generators in propositional proof complexity. SIAM Journal on Computing, 34(1):67-88, 2004.
E. Ben-Sasson and R. Impagliazzo. Random CNF’s are hard for the polynomial calculus. Computational Complexity, 19(4):501-519, 2010.
M. L. Bonet, C. Domingo, R. Gavaldà, A. Maciel, and T. Pitassi. Non-automatizability of bounded-depth Frege proofs. Computational Complexity, 13(1-2):47-68, 2004.
S. R. Buss. Bounded arithmetic. Studies in Proof Theory. Lecture Notes, 3. Napoli: Bibliopolis. VII, 221 p. (1986)., 1986.
R. Fagin. Generalized first-order spectra and polynomial-time recognizable sets. Complexity of Comput., Proc. Symp. appl. Math., New York City 1973, 43-73 (1974)., 1974.
E. Jeřábek. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Annals of Pure and Applied Logic, 129(1-3):1-37, 2004.
E. Jeřábek. Approximate counting in bounded arithmetic. The Journal of Symbolic Logic, 72(3):959-993, 2007.
J. Krajíček. Bounded arithmetic, propositional logic, and complexity theory, volume 60. Cambridge: Cambridge Univ. Press, 1995.
J. Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997.
J. Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-2):123-140, 2001.
J. Krajíček. Tautologies from pseudo-random generators. The Bulletin of Symbolic Logic, 7(2):197-212, 2001.
J. Krajíček. Diagonalization in proof complexity. Fundamenta Mathematicae, 182(2):181-192, 2004.
J. Krajíček. Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds. The Journal of Symbolic Logic, 69(1):265-286, 2004.
J. Krajíček. Structured pigeonhole principle, search problems and hard tautologies. The Journal of Symbolic Logic, 70(2):616-630, 2005.
J. Krajíček. A proof complexity generator. In Logic, methodology and philosophy of science. Proceedings of the 13th international congress, Beijing, China, August 2007, pages 185-190. London: College Publications, 2009.
J. Krajíček. A form of feasible interpolation for constant depth Frege systems. The Journal of Symbolic Logic, 75(2):774-784, 2010.
J. Krajíček. Forcing with random variables and proof complexity, volume 382. Cambridge: Cambridge University Press, 2011.
J. Krajíček. On the proof complexity of the Nisan-Wigderson generator based on a hard NP ∩ coNP function. Journal of Mathematical Logic, 11(1):11-27, 2011.
J. Krajíček. A reduction of proof complexity to computational complexity for AC⁰[p] Frege systems. Proceedings of the American Mathematical Society, 143(11):4951-4965, 2015.
J. Krajíček. Proof complexity, volume 170. Cambridge: Cambridge University Press, 2019.
J. Krajíček. Small Circuits and Dual Weak PHP in the Universal Theory of P-Time Algorithms. ACM Transactions on Computational Logic, 22(2), 2021.
J. Krajíček and P. Pudlák. Propositional proof systems, the consistency of first order theories and the complexity of computations. The Journal of Symbolic Logic, 54(3):1063-1079, 1989.
J. Krajíček and P. Pudlák. Some consequences of cryptographical conjectures for S₂¹ and EF. Information and Computation, 140(1):82-94, 1998.
J. Krajíček, P. Pudlák, and A. Woods. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures & Algorithms, 7(1):15-39, 1995.
N. Nisan and A. Wigderson. Hardness vs randomness. Journal of Computer and System Sciences, 49(2):149-167, 1994.
J. Paris and A. Wilkie. Counting problems in bounded arithmetic. Methods in mathematical logic, Proc. 6th Latin Amer. Symp., Caracas/Venez. 1983, Lect. Notes Math. 1130, 317-340 (1985)., 1985.
J. Pich. Nisan-Wigderson generators in proof systems with forms of interpolation. Mathematical Logic Quarterly (MLQ), 57(4):379-383, 2011.
J. Pich. Circuit lower bounds in bounded arithmetics. Annals of Pure and Applied Logic, 166(1):29-45, 2015.
J. Pich. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic. Logical Methods in Computer Science, 11(2):38, 2015.
J. Pich. Learning algorithms from circuit lower bounds. arXiv, 2020. URL: http://arxiv.org/abs/2012.14095.
http://arxiv.org/abs/2012.14095
J. Pich and R. Santhanam. Strong Co-Nondeterministic Lower Bounds for NP Cannot Be Proved Feasibly. In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021, pages 223-233, 2021.
T. Pitassi, P. Beame, and R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity, 3(2):97-140, 1993.
P. Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, 1997.
P. Pudlák. Incompleteness in the finite domain. The Bulletin of Symbolic Logic, 23(4):405-441, 2017.
P. Pudlák. The canonical pairs of bounded depth Frege systems. Annals of Pure and Applied Logic, 172(2):42, 2021. Id/No 102892.
A. A. Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics. Second Series, 181(2):415-472, 2015.
D. Sokolov. Pseudorandom Generators, Resolution and Heavy Width. In S. Lovett, editor, 37th Computational Complexity Conference (CCC 2022), volume 234 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:22, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CCC.2022.15.
https://doi.org/10.4230/LIPIcs.CCC.2022.15
A. R. Woods. Approximating the structures accepted by a constant depth circuit or satisfying a sentence - a nonstandard approach. In Logic and random structures. DIMACS workshop, November 5-7, 1995, pages 109-130. DIMACS/AMS, 1997.
Erfan Khaniki
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode