8 Search Results for "Khaniki, Erfan"

Document
DOI: 10.4230/LIPIcs.ITCS.2026.8
Intersection Theorems: A Potential Approach to Proof Complexity Lower Bounds

Authors: Yaroslav Alekseev and Nikita Gaevoy

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
Recently, Göös et al. [Göös et al., 2024] showed that Res ⋏ uSA = RevRes in the following sense: if a formula φ has refutations of size at most s and width/degree at most w in both Res and uSA, then there is a refutation for φ of size at most poly(s ⋅ 2^w) in RevRes. Their proof relies on the TFNP characterization of the aforementioned proof systems. In our work, we give a direct and simplified proof of this result, simultaneously achieving better bounds: we show that if for a formula φ there are refutations of size at most s in both Res and uSA, then there is a refutation of φ of size at most poly(s) in RevRes. This potentially allows us to "lift" size lower bounds from RevRes to Res for the formulas for which there are upper bounds in uSA. This kind of lifting was not possible before because of the exponential blow-up in size from the width. Similarly, we improve the bounds in another intersection theorem from [Göös et al., 2024] by giving a direct proof of Res ⋏ uNS = RevResT. Finally, we generalize those intersection theorems to some proof systems for which we currently do not have a TFNP characterization. For example, we show that Res(⊕) ⋏ u-wRes(⊕) = RevRes(⊕), which effectively allows us to reduce the problem of proving Pigeonhole Principle lower bounds in Res(⊕) to proving Pigeonhole Principle lower bounds in RevRes(⊕), a potentially weaker proof system.
Cite as

Yaroslav Alekseev and Nikita Gaevoy. Intersection Theorems: A Potential Approach to Proof Complexity Lower Bounds. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{alekseev_et_al:LIPIcs.ITCS.2026.8,
  author =	{Alekseev, Yaroslav and Gaevoy, Nikita},
  title =	{{Intersection Theorems: A Potential Approach to Proof Complexity Lower Bounds}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.8},
  URN =		{urn:nbn:de:0030-drops-252953},
  doi =		{10.4230/LIPIcs.ITCS.2026.8},
  annote =	{Keywords: proof complexity, intersection theorems}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.79
Range Avoidance and Remote Point: New Algorithms and Hardness

Authors: Shengtang Huang, Xin Li, and Yan Zhong

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
The Range Avoidance (Avoid) problem C-Avoid[n,m(n)] asks that, given a circuit in a class C with input length n and output length m(n) > n, find a string not in the range of the circuit. This problem has been a central piece in several recent frameworks for proving circuit lower bounds and constructing explicit combinatorial objects. Previous work by Korten (FOCS' 21) and by Ren, Santhanam, and Wang (FOCS' 22) showed that algorithms for Avoid are closely related to circuit lower bounds. In particular, Korten’s work reinterpreted an earlier result from bounded arithmetic, originally proved by Jeřábek (Ann. Pure Appl. Log. 2004), as an equivalence in computational complexity between the existence of FP^NP algorithms for the general Avoid problem and 2^{Ω(n)} lower bounds against general Boolean circuits for the class 𝐄^NP. In this work, we significantly complement these works by generalizing the equivalence result to restricted circuit classes and obtain the following: - For any constant depth unbounded fan-in circuit class C ⊇ AC⁰, there is an FP^NP algorithm for C-Avoid[n,n^{1+ε}] (for any constant ε > 0) if and only if 𝐄^NP cannot be computed by C circuits of size 2^{o(n)}. This addresses an open problem by Korten (Bulletin of EATCS' 25). - If 𝐄^NP cannot be computed by o(2ⁿ/n) size formulas, then there is an FP^NP algorithm for NC⁰-Avoid[n,2n]. Note that by an extension of Ren, Santhanam, and Wang (FOCS' 22), an FP^NP algorithm for NC⁰₄-Avoid[n,n+n^δ] for any constant δ ∈ (0,1) implies 𝐄^NP cannot be computed by o(2ⁿ/n) size formulas. These results yield the first characterizations of FP^NP C-Avoid algorithms for low-complexity circuit classes such as AC⁰. We also consider the average-case analog of Avoid, the Remote Point (Remote-Point) problem, and establish: - For some suitable function c(n) and constant γ > 0, there is an FP^NP algorithm for Remote-Point[n,n^{6+γ},c(O_{γ}(log n))] if and only if 𝐄^NP cannot be (1/2-c(n))-approximated by circuits of size 2^{o(n)}. Finally, we also present two improved algorithms for NC⁰-Avoid: - A family of 2^{n^{1 - ε/(k-1) +o(1)}} time algorithms for NC⁰_k-Avoid[n,n^{1+ε}] for any ε > 0, exhibiting the first subexponential-time algorithm for any super-linear stretch. - Faster local algorithms for NC⁰_k-Avoid[n,n+1] running in time O(n2^{(k-2)/(k-1) n}), improving the naive 2ⁿ⋅ poly(n) bound.
Cite as

Shengtang Huang, Xin Li, and Yan Zhong. Range Avoidance and Remote Point: New Algorithms and Hardness. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 79:1-79:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{huang_et_al:LIPIcs.ITCS.2026.79,
  author =	{Huang, Shengtang and Li, Xin and Zhong, Yan},
  title =	{{Range Avoidance and Remote Point: New Algorithms and Hardness}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{79:1--79:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.79},
  URN =		{urn:nbn:de:0030-drops-253662},
  doi =		{10.4230/LIPIcs.ITCS.2026.79},
  annote =	{Keywords: Circuit Lower Bounds, Range Avoidance Problem, Remote Point Problem}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.60
Total Search Problems in ZPP

Authors: Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Morgan Shirley, and Weiqiang Yuan

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
We initiate a systematic study of TFZPP, the class of total NP search problems solvable by polynomial time randomized algorithms. TFZPP contains a variety of important search problems such as Bertrand-Chebyshev (finding a prime between N and 2N), refuter problems for many circuit lower bounds, and Lossy-Code. The Lossy-Code problem has found prominence due to its fundamental connections to derandomization, catalytic computing, and the metamathematics of complexity theory, among other areas. While TFZPP collapses to FP under standard derandomization assumptions in the white-box setting, we are able to separate TFZPP from the major TFNP subclasses in the black-box setting. In fact, we are able to separate it from every uniform TFNP class assuming that NP is not in quasi-polynomial time. To do so, we extend the connection between proof complexity and black-box TFNP to randomized proof systems and randomized reductions. Next, we turn to developing a taxonomy of TFZPP problems. We highlight a problem called Nephew, originating from an infinity axiom in set theory. We show that Nephew is in PWPP∩ TFZPP and conjecture that it is not reducible to Lossy-Code. Intriguingly, except for some artificial examples, most other black-box TFZPP problems that we are aware of reduce to Lossy-Code: - We define a problem called Empty-Child capturing finding a leaf in a rooted (binary) tree, and show that this problem is equivalent to Lossy-Code. We also show that a variant of Empty-Child with "heights" is complete for the intersection of SOPL and Lossy-Code. - We strengthen Lossy-Code with several combinatorial inequalities such as the AM-GM inequality. Somewhat surprisingly, we show the resulting new problems are still reducible to Lossy-Code. A technical highlight of this result is that they are proved by formalizations in bounded arithmetic, specifically in Jeřábek’s theory APC₁ (JSL 2007). - Finally, we show that the Dense-Linear-Ordering problem reduces to Lossy-Code.
Cite as

Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Morgan Shirley, and Weiqiang Yuan. Total Search Problems in ZPP. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 60:1-60:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.ITCS.2026.60,
  author =	{Fleming, Noah and Grosser, Stefan and Jain, Siddhartha and Li, Jiawei and Ren, Hanlin and Shirley, Morgan and Yuan, Weiqiang},
  title =	{{Total Search Problems in ZPP}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{60:1--60:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.60},
  URN =		{urn:nbn:de:0030-drops-253473},
  doi =		{10.4230/LIPIcs.ITCS.2026.60},
  annote =	{Keywords: TFNP, lossy code, randomized proof systems, query complexity}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.111
Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits

Authors: Hanlin Ren, Yichuan Wang, and Yan Zhong

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
Given a circuit G: {0, 1}ⁿ → {0, 1}^m with m > n, the range avoidance problem (Avoid) asks to output a string y ∈ {0, 1}^m that is not in the range of G. Besides its profound connection to circuit complexity and explicit construction problems, this problem is also related to the existence of proof complexity generators - circuits G: {0, 1}ⁿ → {0, 1}^m where m > n but for every y ∈ {0, 1}^m, it is infeasible to prove the statement "y ̸ ∈ Range(G)" in a given propositional proof system. This paper connects these two problems with the existence of demi-bits generators, a fundamental cryptographic primitive against nondeterministic adversaries introduced by Rudich (RANDOM '97). - We show that the existence of demi-bits generators implies Avoid is hard for nondeterministic algorithms. This resolves an open problem raised by Chen and Li (STOC '24). Furthermore, assuming the demi-hardness of certain LPN-style generators or Goldreich’s PRG, we prove the hardness of Avoid even when the instances are constant-degree polynomials over 𝔽₂. - We show that the dual weak pigeonhole principle is unprovable in Cook’s theory PV₁ under the existence of demi-bits generators secure against AM/_{O(1)}, thereby separating Jeřábek’s theory APC₁ from PV₁. Previously, Ilango, Li, and Williams (STOC '23) obtained the same separation under different (and arguably stronger) cryptographic assumptions. - We transform demi-bits generators to proof complexity generators that are pseudo-surjective in certain parameter regime. Pseudo-surjectivity is the strongest form of hardness considered in the literature for proof complexity generators. Our constructions are inspired by the recent breakthroughs on the hardness of Avoid by Ilango, Li, and Williams (STOC '23) and Chen and Li (STOC '24). We use randomness extractors to significantly simplify the construction and the proof.
Cite as

Hanlin Ren, Yichuan Wang, and Yan Zhong. Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 111:1-111:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ren_et_al:LIPIcs.ITCS.2026.111,
  author =	{Ren, Hanlin and Wang, Yichuan and Zhong, Yan},
  title =	{{Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{111:1--111:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.111},
  URN =		{urn:nbn:de:0030-drops-253982},
  doi =		{10.4230/LIPIcs.ITCS.2026.111},
  annote =	{Keywords: Range Avoidance, Proof Complexity Generators}
}
Document
DOI: 10.4230/LIPIcs.CCC.2024.15
Quantum Automating TC⁰-Frege Is LWE-Hard

Authors: Noel Arteche, Gaia Carenini, and Matthew Gray

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC⁰-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC⁰-Frege and AC⁰-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.
Cite as

Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum Automating TC⁰-Frege Is LWE-Hard. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 15:1-15:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.CCC.2024.15,
  author =	{Arteche, Noel and Carenini, Gaia and Gray, Matthew},
  title =	{{Quantum Automating TC⁰-Frege Is LWE-Hard}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{15:1--15:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.15},
  URN =		{urn:nbn:de:0030-drops-204117},
  doi =		{10.4230/LIPIcs.CCC.2024.15},
  annote =	{Keywords: automatability, post-quantum cryptography, feasible interpolation}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.12
From Proof Complexity to Circuit Complexity via Interactive Protocols

Authors: Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Folklore in complexity theory suspects that circuit lower bounds against NC¹ or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Krajíček, 2004], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [Lund et al., 1992]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.
Cite as

Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.ICALP.2024.12,
  author =	{Arteche, Noel and Khaniki, Erfan and Pich, J\'{a}n and Santhanam, Rahul},
  title =	{{From Proof Complexity to Circuit Complexity via Interactive Protocols}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.12},
  URN =		{urn:nbn:de:0030-drops-201557},
  doi =		{10.4230/LIPIcs.ICALP.2024.12},
  annote =	{Keywords: proof complexity, circuit complexity, interactive protocols}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2024.63
TFNP Intersections Through the Lens of Feasible Disjunction

Authors: Pavel Hubáček, Erfan Khaniki, and Neil Thapen

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
The complexity class CLS was introduced by Daskalakis and Papadimitriou (SODA 2010) to capture the computational complexity of important TFNP problems solvable by local search over continuous domains and, thus, lying in both PLS and PPAD. It was later shown that, e.g., the problem of computing fixed points guaranteed by Banach’s fixed point theorem is CLS-complete by Daskalakis et al. (STOC 2018). Recently, Fearnley et al. (J. ACM 2023) disproved the plausible conjecture of Daskalakis and Papadimitriou that CLS is a proper subclass of PLS∩PPAD by proving that CLS = PLS∩PPAD. To study the possibility of other collapses in TFNP, we connect classes formed as the intersection of existing subclasses of TFNP with the phenomenon of feasible disjunction in propositional proof complexity; where a proof system has the feasible disjunction property if, whenever a disjunction F ∨ G has a small proof, and F and G have no variables in common, then either F or G has a small proof. Based on some known and some new results about feasible disjunction, we separate the classes formed by intersecting the classical subclasses PLS, PPA, PPAD, PPADS, PPP and CLS. We also give the first examples of proof systems which have the feasible interpolation property, but not the feasible disjunction property.
Cite as

Pavel Hubáček, Erfan Khaniki, and Neil Thapen. TFNP Intersections Through the Lens of Feasible Disjunction. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 63:1-63:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hubacek_et_al:LIPIcs.ITCS.2024.63,
  author =	{Hub\'{a}\v{c}ek, Pavel and Khaniki, Erfan and Thapen, Neil},
  title =	{{TFNP Intersections Through the Lens of Feasible Disjunction}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{63:1--63:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.63},
  URN =		{urn:nbn:de:0030-drops-195917},
  doi =		{10.4230/LIPIcs.ITCS.2024.63},
  annote =	{Keywords: TFNP, feasible disjunction, proof complexity, TFNP intersection classes}
}
Document
DOI: 10.4230/LIPIcs.CCC.2022.17
Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds

Authors: Erfan Khaniki

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

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

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)

Copy BibTex To Clipboard

@InProceedings{khaniki:LIPIcs.CCC.2022.17,
  author =	{Khaniki, Erfan},
  title =	{{Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{17:1--17:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.17},
  URN =		{urn:nbn:de:0030-drops-165799},
  doi =		{10.4230/LIPIcs.CCC.2022.17},
  annote =	{Keywords: Proof complexity, Bounded arithmetic, Bounded depth Frege, Nisan-Wigderson generators, Meta-complexity, Lower bounds}
}
  • Refine by Type
  • 8 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 4 2026
  • 3 2024
  • 1 2022

  • Refine by Author
  • 3 Khaniki, Erfan
  • 2 Arteche, Noel
  • 2 Ren, Hanlin
  • 2 Zhong, Yan
  • 1 Alekseev, Yaroslav
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs

  • Refine by Classification
  • 7 Theory of computation → Proof complexity
  • 3 Theory of computation → Circuit complexity
  • 3 Theory of computation → Complexity classes
  • 2 Theory of computation → Complexity theory and logic
  • 2 Theory of computation → Expander graphs and randomness extractors
  • Show More...

  • Refine by Keyword
  • 3 proof complexity
  • 2 TFNP
  • 1 Bounded arithmetic
  • 1 Bounded depth Frege
  • 1 Circuit Lower Bounds
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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