2026-07-31T10:55:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10828 2024-03-06T10:46:48Z ddc:004 open_access

Resolution and the Binary Encoding of Combinatorial Principles Dantchev, Stefan Galesi, Nicola Martin, Barnaby Proof complexity k-DNF resolution binary encodings Clique and Pigeonhole principle Res(s) is an extension of Resolution working on s-DNFs. We prove tight n^{Omega(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. [Massimo Lauria et al., 2017] 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 [Nathan Segerlind et al., 2004], 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-PHP^m_n for m>n. Using the the same recursive approach we prove the new result that for any delta>0, Bin-PHP^m_n requires proofs of size 2^{n^{1-delta}} 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 Bin-PHP^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_2-form and with no finite model. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefan Dantchev and Nicola Galesi and Barnaby Martin 2019 Is Part Of LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2019.6 urn:nbn:de:0030-drops-108287 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.6 eng https://creativecommons.org/licenses/by/3.0/legalcode