Document Open Access Logo

Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds

Author Erfan Khaniki

PDF
Thumbnail PDF

File

LIPIcs.CCC.2022.17.pdf
  • Filesize: 0.79 MB
  • 15 pages

Document Identifiers

Author Details

Erfan Khaniki
  • Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic
  • Institute of Mathematics of the Czech Academy of Sciences, Prague, Czech Republic

Funding

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.

Acknowledgements

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.

Cite As Get BibTex

Erfan Khaniki. Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CCC.2022.17

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 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].

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Complexity theory and logic
Keywords
  • Proof complexity
  • Bounded arithmetic
  • Bounded depth Frege
  • Nisan-Wigderson generators
  • Meta-complexity
  • Lower bounds

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14(4):417-433, 1994. Google Scholar
  2. 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. Google Scholar
  3. E. Ben-Sasson and R. Impagliazzo. Random CNF’s are hard for the polynomial calculus. Computational Complexity, 19(4):501-519, 2010. Google Scholar
  4. 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. Google Scholar
  5. S. R. Buss. Bounded arithmetic. Studies in Proof Theory. Lecture Notes, 3. Napoli: Bibliopolis. VII, 221 p. (1986)., 1986. Google Scholar
  6. 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. Google Scholar
  7. E. Jeřábek. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Annals of Pure and Applied Logic, 129(1-3):1-37, 2004. Google Scholar
  8. E. Jeřábek. Approximate counting in bounded arithmetic. The Journal of Symbolic Logic, 72(3):959-993, 2007. Google Scholar
  9. J. Krajíček. Bounded arithmetic, propositional logic, and complexity theory, volume 60. Cambridge: Cambridge Univ. Press, 1995. Google Scholar
  10. 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. Google Scholar
  11. J. Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-2):123-140, 2001. Google Scholar
  12. J. Krajíček. Tautologies from pseudo-random generators. The Bulletin of Symbolic Logic, 7(2):197-212, 2001. Google Scholar
  13. J. Krajíček. Diagonalization in proof complexity. Fundamenta Mathematicae, 182(2):181-192, 2004. Google Scholar
  14. 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. Google Scholar
  15. J. Krajíček. Structured pigeonhole principle, search problems and hard tautologies. The Journal of Symbolic Logic, 70(2):616-630, 2005. Google Scholar
  16. 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. Google Scholar
  17. J. Krajíček. A form of feasible interpolation for constant depth Frege systems. The Journal of Symbolic Logic, 75(2):774-784, 2010. Google Scholar
  18. J. Krajíček. Forcing with random variables and proof complexity, volume 382. Cambridge: Cambridge University Press, 2011. Google Scholar
  19. 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. Google Scholar
  20. 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. Google Scholar
  21. J. Krajíček. Proof complexity, volume 170. Cambridge: Cambridge University Press, 2019. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. J. Krajíček and P. Pudlák. Some consequences of cryptographical conjectures for S₂¹ and EF. Information and Computation, 140(1):82-94, 1998. Google Scholar
  25. 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. Google Scholar
  26. N. Nisan and A. Wigderson. Hardness vs randomness. Journal of Computer and System Sciences, 49(2):149-167, 1994. Google Scholar
  27. 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. Google Scholar
  28. J. Pich. Nisan-Wigderson generators in proof systems with forms of interpolation. Mathematical Logic Quarterly (MLQ), 57(4):379-383, 2011. Google Scholar
  29. J. Pich. Circuit lower bounds in bounded arithmetics. Annals of Pure and Applied Logic, 166(1):29-45, 2015. Google Scholar
  30. 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. Google Scholar
  31. J. Pich. Learning algorithms from circuit lower bounds. arXiv, 2020. URL: http://arxiv.org/abs/2012.14095.
  32. 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. Google Scholar
  33. T. Pitassi, P. Beame, and R. Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity, 3(2):97-140, 1993. Google Scholar
  34. P. Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, 1997. Google Scholar
  35. P. Pudlák. Incompleteness in the finite domain. The Bulletin of Symbolic Logic, 23(4):405-441, 2017. Google Scholar
  36. P. Pudlák. The canonical pairs of bounded depth Frege systems. Annals of Pure and Applied Logic, 172(2):42, 2021. Id/No 102892. Google Scholar
  37. A. A. Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics. Second Series, 181(2):415-472, 2015. Google Scholar
  38. 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.
  39. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact