Resolution and the binary encoding of combinatorial principles

Dantchev, Stefan; Galesi, Nicola; Martin, Barnaby

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.

Citation

Dantchev, S., Galesi, N., & Martin, B. (2019, July). Resolution and the binary encoding of combinatorial principles. Presented at Computational Complexity Conference, New Brunswick, New Jersey, USA

• Presentation Conference Type: Conference Paper (published)
• Conference Name: Computational Complexity Conference
• Acceptance Date: Apr 30, 2019
• Online Publication Date: Jul 16, 2019
• Publication Date: Jul 31, 2019
• Deposit Date: May 19, 2019
• Publicly Available Date: Jul 16, 2019
• Volume: 137
• Pages: 6:1-6:25
• Series Title: Leibniz International Proceedings in Informatics (LIPIcs)
• Series ISSN: 1868-8969
• Book Title: 34th Computational Complexity Conference (CCC 2019).
• DOI: https://doi.org/10.4230/lipics.ccc.2019.6
• Public URL: https://durham-repository.worktribe.com/output/1142143