We present a general method for converting any family of unsatisfiable CNF formulas that is hard for one of the simplest proof systems, tree resolution (ordinary backtracking search), into formulas that require largerank in very strong proof systems, which include any proof system that manipulates polynomials or polynomial threshold functions of degree at most k (known as Th(k) proofs). Such systems include: Lovasz-Schrijver and Cutting Planes proof systems as well as their high degree analogues (LS(k), LS+(k)), and CP(k) and Sherali-Adams and Lasserre proofs.

We introduce two very general families of these very strong proof systems, denotedby Tcc(k) and Rcc(k). The proof lines of Tcck are arbitrary Boolean functions, each of which can be evaluated by an efficient k-party randomized communication protocol. Tcc(k) proofs include Th{k−1} proofs as a special case. Rcc(k) proofs generalize Tcc(k) proofs and require only that each inference be checkable (in a certain weak sense) by an efficient k-party randomized communication protocol.

Our main results are the following:

(1) For kO(loglogn), we prove that from any unsatisfiable CNF formula F requiring resolution rank r, we can obtain a related CNF formula G=Liftk(F) requiring refutation rankr(1k)logO(1)n in all Rcc(k) systems. Since resolution rank is at least resolution width (for which many strong lower bounds are known), this yields strong rank lower bounds in all of the above proof systems for large classes of natural CNF formulas.

(2) There are strict hierarchies for Tcc(k) and Rcc(k)systems with respect to k. Specifically, for kO(loglogn), we produce unsatisfiable CNF formulas whose proofs require large rank in Rcc(k) but which can be refuted via polylogarithmic rank CP(k) proofs. Rank separations between CP(k−1) and CP(k), between Th(k−1) and Th(k), and between Rcc(k) and Tcc(k+1) follow immediately.

(3) When k is O(loglogn) we also derive 2n(1k) lower bounds on the size of tree-like Tcc(k) refutations for large classes of lifted CNF formulas. Moreover, the rank hierarchies we prove extend to nearly exponential separations in tree-like proof size.

(4)A general method for producing integrality gaps for low rank Rcc(2) inference based on related gaps for low rank resolution. This yields integrality gaps for low rank Cutting Planes and more general Th(1) inference. These gaps are optimal for MAX-2t-SAT.