3 Search Results for "Dantchev, Stefan"

Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.21
Multiparty Communication Complexity of Collision-Finding and Cutting Planes Proofs of Concise Pigeonhole Principles

Authors: Paul Beame and Michael Whitmeyer

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We prove several results concerning the communication complexity of a collision-finding problem, each of which has applications to the complexity of cutting-plane proofs, which make inferences based on integer linear inequalities. In particular, we prove an Ω(n^{1-1/k} log k /2^k) lower bound on the k-party number-in-hand communication complexity of collision-finding. This implies a 2^{n^{1-o(1)}} lower bound on the size of tree-like cutting-planes refutations of the bit pigeonhole principle CNFs, which are compact and natural propositional encodings of the negation of the pigeonhole principle, improving on the best previous lower bound of 2^{Ω(√n)}. Using the method of density-restoring partitions, we also extend that previous lower bound to the full range of pigeonhole parameters. Finally, using a refinement of a bottleneck-counting framework of Haken and Cook and Sokolov for DAG-like communication protocols, we give a 2^{Ω(n^{1/4})} lower bound on the size of fully general (not necessarily tree-like) cutting planes refutations of the same bit pigeonhole principle formulas, improving on the best previous lower bound of 2^{Ω(n^{1/8})}.
Cite as

Paul Beame and Michael Whitmeyer. Multiparty Communication Complexity of Collision-Finding and Cutting Planes Proofs of Concise Pigeonhole Principles. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{beame_et_al:LIPIcs.ICALP.2025.21,
  author =	{Beame, Paul and Whitmeyer, Michael},
  title =	{{Multiparty Communication Complexity of Collision-Finding and Cutting Planes Proofs of Concise Pigeonhole Principles}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.21},
  URN =		{urn:nbn:de:0030-drops-233982},
  doi =		{10.4230/LIPIcs.ICALP.2025.21},
  annote =	{Keywords: Proof Complexity, Communication Complexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2022.24
Depth Lower Bounds in Stabbing Planes for Combinatorial Principles

Authors: Stefan Dantchev, Nicola Galesi, Abdul Ghani, and Barnaby Martin

Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

Abstract
Stabbing Planes is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system established via communication complexity arguments. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner’s Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon’s combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.
Cite as

Stefan Dantchev, Nicola Galesi, Abdul Ghani, and Barnaby Martin. Depth Lower Bounds in Stabbing Planes for Combinatorial Principles. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dantchev_et_al:LIPIcs.STACS.2022.24,
  author =	{Dantchev, Stefan and Galesi, Nicola and Ghani, Abdul and Martin, Barnaby},
  title =	{{Depth Lower Bounds in Stabbing Planes for Combinatorial Principles}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.24},
  URN =		{urn:nbn:de:0030-drops-158349},
  doi =		{10.4230/LIPIcs.STACS.2022.24},
  annote =	{Keywords: proof complexity, computational complexity, lower bounds, cutting planes, stabbing planes}
}
Document
DOI: 10.4230/LIPIcs.CCC.2019.6
Resolution and the Binary Encoding of Combinatorial Principles

Authors: Stefan Dantchev, Nicola Galesi, and Barnaby Martin

Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)

Abstract
Res(s) is an extension of Resolution working on s-DNFs. We prove tight n^{Omega(k)} lower bounds for the size of refutations of the binary version of the k-Clique Principle in Res(o(log log n)). Our result improves that of Lauria, Pudlák et al. [Massimo Lauria et al., 2017] who proved the lower bound for Res(1), i.e. Resolution. The exact complexity of the (unary) k-Clique Principle in Resolution is unknown. To prove the lower bound we do not use any form of the Switching Lemma [Nathan Segerlind et al., 2004], instead we apply a recursive argument specific for binary encodings. Since for the k-Clique and other principles lower bounds in Resolution for the unary version follow from lower bounds in Res(log n) for their binary version we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the weak Pigeonhole Principle Bin-PHP^m_n for m>n. Using the the same recursive approach we prove the new result that for any delta>0, Bin-PHP^m_n requires proofs of size 2^{n^{1-delta}} in Res(s) for s=o(log^{1/2}n). Our lower bound is almost optimal since for m >= 2^{sqrt{n log n}} there are quasipolynomial size proofs of Bin-PHP^m_n in Res(log n). Finally we propose a general theory in which to compare the complexity of refuting the binary and unary versions of large classes of combinatorial principles, namely those expressible as first order formulae in Pi_2-form and with no finite model.
Cite as

Stefan Dantchev, Nicola Galesi, and Barnaby Martin. Resolution and the Binary Encoding of Combinatorial Principles. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dantchev_et_al:LIPIcs.CCC.2019.6,
  author =	{Dantchev, Stefan and Galesi, Nicola and Martin, Barnaby},
  title =	{{Resolution and the Binary Encoding of Combinatorial Principles}},
  booktitle =	{34th Computational Complexity Conference (CCC 2019)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-116-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{137},
  editor =	{Shpilka, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.6},
  URN =		{urn:nbn:de:0030-drops-108287},
  doi =		{10.4230/LIPIcs.CCC.2019.6},
  annote =	{Keywords: Proof complexity, k-DNF resolution, binary encodings, Clique and Pigeonhole principle}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2022
  • 1 2019

  • Refine by Author
  • 2 Dantchev, Stefan
  • 2 Galesi, Nicola
  • 2 Martin, Barnaby
  • 1 Beame, Paul
  • 1 Ghani, Abdul
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 1 Mathematics of computing
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Computational complexity and cryptography
  • 1 Theory of computation → Proof complexity

  • Refine by Keyword
  • 1 Clique and Pigeonhole principle
  • 1 Communication Complexity
  • 1 Proof Complexity
  • 1 Proof complexity
  • 1 binary encodings
  • 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