We investigate the size complexity of proofs in RE S ( s ) -- an extension of Resolution working on s -DNFs instead of clauses -- for families of contradictions given in the {\em unusual binary} encoding. A motivation of our work is size lower bounds of refutations in Resolution for families of contradictions in the {\em usual unary} encoding. Our main interest is the k -Clique Principle, whose Resolution complexity is still unknown. The approach is justified by the observation that for a large class of combinatorial principles (those expressible as 2 first-order formulae) short RE S ( log n ) refutations for the binary encoding are reducible to short Resolution refutations of the unary encoding.

Our main result is a n ( k ) lower bound for the size of refutations of the binary k -Clique Principle in RE S ( 2 1 log log n ) . This improves the result of Lauria, Pudl\'ak et al. [24] who proved the lower bound for Resolution, that is \RES (1) . A lower bound in RE S ( log n ) for the binary k -Clique Principle would prove a lower bound in Resolution for its unary version. Resolution lower bounds for the (unary) k -Clique Principle are known only when refutations are either treelike [10] or read-once [4] (regular Resolution).

To contrast the proof complexity between the unary and binary encodings of combinatorial principles, we consider the binary (weak) Pigeonhole principle BinPH P n m for n"> m n . Our second lower bound proves that in RE S ( s ) for s log 1 2 − ( n ) , the shortest proofs of the BinPH P n m , requires size 2 n 1 − , for any 0"> 0 . By a result of Buss and Pitassi [15] we know that for the (unary, weak) Pigeonhole principle PH P n m , exponential lower bounds (in the size of PH P n m ) are not possible in Resolution when m 2 n log n since there is an upper bound of 2 O ( n log n ) . Our lower bound for BinPH P n m , together with the fact short RE S (1) refutations for PH P n m can be translated into short RE S ( log n ) proofs for \BinPHP n m , shows a form of tightness of the upper bound of [15]. Furthermore we prove that BinPH P n m can be refuted in size 2 ( n ) in treelike RE S (1) , contrasting with the unary case, where PH P n m requires treelike RE S (1) refutations of size 2 ( n log n ) [9,16].

In order to compare the complexity of refuting binary encodings in Resolution with respect to their unary version, we study under what conditions the complexity of refutations in Resolution will not increase significantly (more than a polynomial factor) when shifting between the unary encoding and the binary encoding. We show that this is true, from unary to binary, for propositional encodings of principles expressible as a 2 -formula and involving total variable comparisons. We then show that this is true, from binary to unary, when one considers the {\em functional unary encoding}. In particular, we derive a polynomial upper bound in RE S (1) for the binary version bRLO P of a variant of the Linear Ordering principle, RLO P , which exponentially separates read-once Resolution from Resolution (see [2]). Finally we prove that the binary encoding of the general Ordering principle O P -- with no total ordering constraints -- is polynomially provable in Resolution. These last results can be interpreted as addressing the property that shifting to the binary encoding is preserving the proof hardness of the corresponding unary encodings when working in Resolution.