License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CCC.2019.6
URN: urn:nbn:de:0030-drops-108287
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10828/
Dantchev, Stefan ;
Galesi, Nicola ;
Martin, Barnaby
Resolution and the Binary Encoding of Combinatorial Principles
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 |
|
Collection: |
|
34th Computational Complexity Conference (CCC 2019) |
|
Issue Date: |
|
2019 |
|
Date of publication: |
|
16.07.2019 |
