Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Dantchev, Stefan; Galesi, Nicola; Martin, Barnaby http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-108287
URL:

; ;

Resolution and the Binary Encoding of Combinatorial Principles

pdf-format:


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.

BibTeX - Entry

@InProceedings{dantchev_et_al:LIPIcs:2019:10828,
  author =	{Stefan Dantchev and Nicola Galesi and Barnaby Martin},
  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 =	{Amir Shpilka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10828},
  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}
}

Keywords: Proof complexity, k-DNF resolution, binary encodings, Clique and Pigeonhole principle
Seminar: 34th Computational Complexity Conference (CCC 2019)
Issue date: 2019
Date of publication: 2019


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI