Ricerc@Sapienza

We show the close connection between the enumeration of cliques in a k-clique free graph G and the length of tree-like resolution refutations for formula Clique(G,k), which claims that G has a k-clique. The length of any such tree-like refutation is within a "fixed parameter tractable" factor from the number of cliques in the graph. We then proceed to drastically simplify the proofs of the lower bounds for the length of tree-like resolution refutations of Clique(G,k) shown in [Beyersdorff et at. 2013, Lauria et al. 2017], which now reduce to a simple estimate of the number of cliques.

Res(s) is an extension of Resolution working on s-DNFs. We prove tight nΩ(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, Pudlák 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.