Cliques enumeration and tree-like resolution proofs

We show the close connection between the enumeration of cliques in a k-clique free graph G, the running time of DPLL-style algorithms for k-clique problem, 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 said quantity.