Search Results

Documents authored by Khaniki, Erfan

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}
}
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