4 Search Results for "Thapen, Neil"

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-dev.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.SAT.2023.22
Even Shorter Proofs Without New Variables

Authors: Adrián Rebola-Pardo

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning. Interference-based methods have been proven effective, and some theoretical work has been undertaken to better explain their limits and semantics. In this work, we combine the subsumption redundancy notion from [Sam Buss and Neil Thapen, 2019] and the overwrite logic framework from [Adrián Rebola{-}Pardo and Martin Suda, 2018]. Natural generalizations then become apparent, enabling even shorter proofs of the pigeonhole principle (compared to those from [Marijn J. H. Heule et al., 2017]) and smaller unsatisfiable core generation.
Cite as

Adrián Rebola-Pardo. Even Shorter Proofs Without New Variables. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{rebolapardo:LIPIcs.SAT.2023.22,
  author =	{Rebola-Pardo, Adri\'{a}n},
  title =	{{Even Shorter Proofs Without New Variables}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.22},
  URN =		{urn:nbn:de:0030-drops-184844},
  doi =		{10.4230/LIPIcs.SAT.2023.22},
  annote =	{Keywords: Interference, SAT solving, Unsatisfiability proofs, Unsatisfiable cores}
}
Document
DOI: 10.4230/LIPIcs.CCC.2017.1
Random Resolution Refutations

Authors: Pavel Pudlák and Neil Thapen

Published in: LIPIcs, Volume 79, 32nd Computational Complexity Conference (CCC 2017)

Abstract
We study the random resolution refutation system definedin [Buss et al. 2014]. This attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. By proving the equivalence of several different definitions, we show that this concept is robust. On the other hand, if P does not equal NP, then random resolution cannot be polynomially simulated by any proof system in which correctness of proofs is checkable in polynomial time. We prove several upper and lower bounds on the width and size of random resolution refutations of explicit and random unsatisfiable CNF formulas. Our main result is a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which solves the problem stated in [Buss et al. 2014]. We also prove exponential size lower bounds on random resolution refutations of the pigeonhole principle CNFs, and of a family of CNFs which have polynomial size refutations in constant depth Frege.
Cite as

Pavel Pudlák and Neil Thapen. Random Resolution Refutations. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{pudlak_et_al:LIPIcs.CCC.2017.1,
  author =	{Pudl\'{a}k, Pavel and Thapen, Neil},
  title =	{{Random Resolution Refutations}},
  booktitle =	{32nd Computational Complexity Conference (CCC 2017)},
  pages =	{1:1--1:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-040-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{79},
  editor =	{O'Donnell, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2017.1},
  URN =		{urn:nbn:de:0030-drops-75235},
  doi =		{10.4230/LIPIcs.CCC.2017.1},
  annote =	{Keywords: proof complexity, random, resolution}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.433
The Space Complexity of Cutting Planes Refutations

Authors: Nicola Galesi, Pavel Pudlák, and Neil Thapen

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known. Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle. We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.
Cite as

Nicola Galesi, Pavel Pudlák, and Neil Thapen. The Space Complexity of Cutting Planes Refutations. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 433-447, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{galesi_et_al:LIPIcs.CCC.2015.433,
  author =	{Galesi, Nicola and Pudl\'{a}k, Pavel and Thapen, Neil},
  title =	{{The Space Complexity of Cutting Planes Refutations}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{433--447},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.433},
  URN =		{urn:nbn:de:0030-drops-50551},
  doi =		{10.4230/LIPIcs.CCC.2015.433},
  annote =	{Keywords: Proof Complexity, Cutting Planes, Space Complexity}
}
  • Refine by Author
  • 3 Thapen, Neil
  • 2 Pudlák, Pavel
  • 1 Galesi, Nicola
  • 1 Hubáček, Pavel
  • 1 Khaniki, Erfan
  • Show More...

  • Refine by Classification
  • 1 Hardware → Theorem proving and SAT solving
  • 1 Theory of computation → Complexity classes
  • 1 Theory of computation → Problems, reductions and completeness
  • 1 Theory of computation → Proof complexity

  • Refine by Keyword
  • 2 proof complexity
  • 1 Cutting Planes
  • 1 Interference
  • 1 Proof Complexity
  • 1 SAT solving
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2015
  • 1 2017
  • 1 2023
  • 1 2024

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 Imprint Privacy Contact