Proof complexity and the binary encoding of combinatorial principles

We consider proof complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this proof complexity with the normal unary encoding in several refutation systems, based on Resolution and Sherali-Adams. We first consider Res(s), which is an extension of Resolution working on s-DNFs (Disjunctive Normal Form formulas). We prove an exponential lower bound of (Formula presented) for the size of refutations of the binary version of the k-Clique Principle in Res(s), where (Formula presented) and d(s) is a doubly exponential function. Our result improves that of Lauria et al., who proved a similar lower bound for Res(1), i.e., Resolution. For the k-Clique and other principles we study, we show how lower bounds in Resolution for the unary version follow from lower bounds in Res(log n) for the binary version, so 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 . We prove that for any (Formula presented) requires refutations of size (Formula presented) in Res(s) for (Formula presented). Our lower bound cannot be improved substantially with the same method since for (Formula presented) we can prove there are (Formula presented) size refutations of Bin - PHPmn in Res(log n). This is a consequence of the same upper bound for the unary weak Pigeonhole Principle of Buss and Pitassi. We contrast unary versus binary encoding in the Sherali-Adams (SA) refutation system where we prove lower bounds for both rank and size. For the unary encoding of the Pigeonhole Principle and the Ordering Principle, it is known that linear rank is required for refutations in SA, although both admit refutations of polynomial size. We prove that the binary encoding of the (weak) Pigeonhole Principle Bin - PHPmn requires exponentially sized (in n) SA refutations, whereas the binary encoding of the Ordering Principle admits logarithmic rank, polynomially sized SA refutations. We continue by considering a natural refutation system we call ``SA+Squares,"" which is intermediate between SA and Lasserre (Sum-of-Squares). This has been studied under the name static-LS\infty+ by Grigoriev et al. In this system, the unary encoding of the Linear Ordering Principle LOPn requires O(n) rank while the unary encoding of the Pigeonhole Principle becomes constant rank. Since Potechin has shown that the rank of LOPn in Lasserre is (Formula presented), we uncover an almost quadratic separation between SA+Squares and Lasserre in terms of rank. Grigoriev et al. noted that the unary Pigeonhole Principle has rank 2 in SA+Squares and therefore polynomial size. Since we show the same applies to the binary Bin - PHPnn+1, we deduce an exponential separation for size between SA and SA+Squares.