Resolution and the Binary Encoding of Combinatorial Principles

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, Pudlak 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-PHPnm for m > n. Using the the same recursive approach we prove the new result that for any delta > 0, Bin-PHPnm requires proofs of size 2(n1-delta) in Res(s) for s = o(log(1/2) n). Our lower bound is almost optimal since for m >= 2(root n log n) there are quasipolynomial size proofs of Bin-PHPnm 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.