Dantchev, Stefan ;
Galesi, Nicola ;
Martin, Barnaby
Resolution and the Binary Encoding of Combinatorial Principles
Abstract
Res(s) is an extension of Resolution working on sDNFs. We prove tight n^{Omega(k)} lower bounds for the size of refutations of the binary version of the kClique 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) kClique 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 kClique 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 Resolutionbased systems for families of contradictions given in the binary encoding.
We go on to consider the binary version of the weak Pigeonhole Principle BinPHP^m_n for m>n. Using the the same recursive approach we prove the new result that for any delta>0, BinPHP^m_n requires proofs of size 2^{n^{1delta}} 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 BinPHP^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_2form 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:16:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771160},
ISSN = {18688969},
year = {2019},
volume = {137},
editor = {Amir Shpilka},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10828},
URN = {urn:nbn:de:0030drops108287},
doi = {10.4230/LIPIcs.CCC.2019.6},
annote = {Keywords: Proof complexity, kDNF resolution, binary encodings, Clique and Pigeonhole principle}
}
2019
Keywords: 

Proof complexity, kDNF resolution, binary encodings, Clique and Pigeonhole principle 
Seminar: 

34th Computational Complexity Conference (CCC 2019)

Issue date: 

2019 
Date of publication: 

2019 