DROPS

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

Search Results

Documents authored by Dantchev, Stefan

Depth Lower Bounds in Stabbing Planes for Combinatorial Principles

Abstract

Cite as

Resolution and the Binary Encoding of Combinatorial Principles

Abstract

Cite as

Thanks for your feedback!

Could not send message