Resolution and the binary encoding of combinatorial principles

We investigate the size complexity of proofs in $Res(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 usual unary encoding. Our main interest is the $k$-Clique Principle, whose Resolution complexity is still unknown. Our main result is a $n^{\mathrm{\Omega }(k)}$ lower bound for the size of refutations of the binary $k$-Clique Principle in $Res(\lfloor \frac{1}{2}\log \log n\rfloor)$. This improves the result of Lauria, Pudl'ak et al. [24] who proved the lower bound for Resolution, that is $Res(1)$. Our second lower bound proves that in $RES(s)$ for $s\leq \log^{\frac{1}{2-\epsilon}}(n)$,theshortestproofsofthe$BinPHP^m_n$, requires size $2^{n^{1-\delta }}$, for any $\delta >0$. Furthermore we prove that $BinPH{P}_n^m$ can be refuted in size $2^{\mathrm{\Theta }(n)}$ in treelike $Res(1)$, contrasting with the unary case, where $PH{P}_n^m$ requires treelike $RES(1)$
refutations of size $2^{\mathrm{\Omega }(n\log n)}$ [9,16]. Furthermore 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 ${\mathrm{\Pi }}_2$-formula and involving {\em total variable comparisons}. We then show that this is true, from binary to unary, when one considers the \emph{functional unary encoding}. Finally we prove that the binary encoding of the general Ordering principle $OP$ – with no total ordering constraints – is polynomially provable in Resolution.