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
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.  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 , 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)
|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
|Look up in GoogleScholar|