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: | |
Look up in GoogleScholar |