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 {\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 $\Pi_2$ first-order formulae) short $RES(\log n)$ refutations for the binary encoding are reducible to short Resolution refutations of the unary encoding.
Our main result is a $n^{\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)$. A lower bound in $RES(\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 $BinPHP^m_n$ for $m>n$. Our second lower bound proves that in $RES(s)$ for $s\leq \log^{\frac{1}{2-\epsilon}}(n)$, the shortest proofs of the $BinPHP^m_n$, requires size $2^{n^{1-\delta}}$, for any $\delta>0$.
By a result of Buss and Pitassi [15] we know that for the (unary, weak) Pigeonhole principle $PHP^m_n$, exponential lower bounds (in the size of $PHP^m_n$) are not possible in Resolution when $m \geq 2^{\sqrt{n\log n}}$ since there is an upper bound of $2^{O(\sqrt{n\log n})}$. Our lower bound for $BinPHP^m_n$, together with the fact short $RES(1)$ refutations for $PHP^m_n$ can be translated into short $RES(\log n)$ proofs for $\BinPHP^m_n$, shows a form of tightness of the upper bound of [15]. Furthermore we prove that $BinPHP^m_n$ can be refuted in size $2^{\Theta(n)}$ in treelike $RES(1)$, contrasting with the unary case, where $PHP^m_n$ requires treelike $RES(1)$ refutations of size $2^{\Omega(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
$\Pi_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 $RES(1)$ for the binary version $bRLOP$ of a variant of the Linear Ordering principle, $RLOP$, which exponentially separates read-once Resolution from Resolution (see [2]). Finally we prove that the binary encoding of the general Ordering principle $OP$ -- 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.
