Cookies

We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.


Durham Research Online
You are in:

Resolution and the binary encoding of combinatorial principles.

Dantchev, Stefan and Galesi, Nicola and Martin, Barnaby (2019) 'Resolution and the binary encoding of combinatorial principles.', in 34th Computational Complexity Conference (CCC 2019). Saarbrücken/Wadern: Dagstuhl Publishing, 6:1-6:25. Leibniz International Proceedings in Informatics (LIPIcs)., 137

Abstract

Res(s) is an extension of Resolution working on s-DNFs. We prove tight n (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. [27] 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 [35], 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-PHPmn for m > n. Using the the same recursive approach we prove the new result that for any > 0, Bin-PHPmn requires proofs of size 2n1− in Res(s) for s = o(log1/2 n). Our lower bound is almost optimal since for m 2 p n log n there are quasipolynomial size proofs of Bin-PHPmn 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 2-form and with no finite model.

Item Type:Book chapter
Full text:(VoR) Version of Record
Available under License - Creative Commons Attribution.
Download PDF
(594Kb)
Status:Peer-reviewed
Publisher Web site:https://doi.org/10.4230/LIPIcs.CCC.2019.6
Publisher statement:© Stefan Dantchev and Nicola Galesi and Barnaby Martin; licensed under Creative Commons License CC-BY.
Date accepted:30 April 2019
Date deposited:21 May 2019
Date of first online publication:16 July 2019
Date first made open access:16 July 2019

Save or Share this output

Export:
Export
Look up in GoogleScholar