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 large
rank in very strong proof systems, which include any proof system that manipulates polynomials or polynomial threshold functions of degree at most $k$ (known as ${\rm Th}(k)$ proofs). Such systems include: Lovasz-Schrijver and Cutting Planes proof systems as well as their high degree analogues (LS($k$), $\mathrm{LS}_+(k)$), and CP($k$) and Sherali-Adams and Lasserre proofs.
We introduce two very general families of these very strong proof systems, denoted
by $T^{cc}(k)$ and $R^{cc}(k)$. The proof lines of $T^{cc}{k}$ are arbitrary Boolean functions, each of which can be evaluated by an efficient $k$-party randomized communication protocol. $T^{cc}(k)$ proofs include Th{$k-1$} proofs as a special case. $R^{cc}(k)$ proofs generalize $T^{cc}(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 $k \in O(\log\log n)$, we prove that from any unsatisfiable CNF formula $F$ requiring resolution rank $r$, we can obtain a related CNF formula $G=\mbox{Lift}_k (F)$ requiring refutation rank
$r^{\Omega(1/k)}/\log^{O(1)} n$ in all $R^{cc}(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 $T^{cc}(k)$ and $R^{cc}(k)$
systems with respect to $k$. Specifically, for $k\in O(\log\log n)$, we produce unsatisfiable CNF formulas whose proofs require large rank in $R^{cc}(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 $R^{cc}(k)$ and $T^{cc}(k+1)$ follow immediately.
(3) When $k$ is $O(\log\log n)$ we also derive $2^{n^{\Omega(1/k)}}$ lower bounds on the size of tree-like $T^{cc}(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 $R^{cc}(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.
Integrality gaps added
We present a generic method for converting any family of unsatisfiable CNF formulas that require large resolution rank into CNF formulas whose refutation requires large rank for proof systems that manipulate polynomials or polynomial threshold functions of degree at most $k$ (known as ${\rm Th}(k)$ proofs). Such systems include: Lovasz-Schrijver and Cutting Planes proof systems as well as their high degree analogues (LS($k$), $\mathrm{LS}_+(k)$), and CP($k$) and Sherali-Adams and Lasserre proofs.
These bounds are derived by analyzing two very general families of proof systems that we introduce, denoted by $T^{cc}(k)$ and $R^{cc}(k)$. The proof lines of $T^{cc}{k}$ are arbitrary Boolean functions, each of which can be evaluated by an efficient $k$-party randomized communication protocol. $T^{cc}(k)$ proofs include Th{$k-1$} proofs as a special case. $R^{cc}(k)$ proofs generalize $T^{cc}(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:
For $k \in O(\log\log n)$, we prove that from any unsatisfiable CNF formula $F$ requiring resolution rank $r$, we can obtain a related CNF formula $G=\mbox{Lift}_k (F)$ requiring refutation rank
$r^{\Omega(1/k)}/\log^{O(1)} n$ in all $R^{cc}(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.
We prove that there are strict hierarchies for $T^{cc}(k)$ and $R^{cc}(k)$
systems with respect to $k$. Specifically, for $k\in O(\log\log n)$, we produce unsatisfiable CNF formulas whose proofs require large rank in $R^{cc}(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 $R^{cc}(k)$ and $T^{cc}(k+1)$ follow immediately.
For $k\in O(\log\log n)$ we also derive $2^{n^{\Omega(1/k)}}$ lower bounds on the size of tree-like $T^{cc}(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.
We present a generic method for converting any family of unsatisfiable CNF formulas that require large resolution rank into CNF formulas whose refutation requires large rank for proof systems that manipulate polynomials or polynomial threshold functions of degree at most $k$ (known as ${\rm Th}(k)$ proofs). Such systems include: Lovasz-Schrijver and Cutting Planes proof systems as well as their high degree analogues (LS($k$), $\mathrm{LS}_+(k)$), and CP($k$) and Sherali-Adams and Lasserre proofs.
These bounds are derived by analyzing two very general families of proof systems that we introduce, denoted by $T^{cc}(k)$ and $R^{cc}(k)$. The proof lines of $T^{cc}{k}$ are arbitrary Boolean functions, each of which can be evaluated by an efficient $k$-party randomized communication protocol. $T^{cc}(k)$ proofs include Th{$k-1$} proofs as a special case. $R^{cc}(k)$ proofs generalize $T^{cc}(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:
\begin{itemize}
\item For $k \in O(\log\log n)$, we prove that from any unsatisfiable CNF formula $F$ requiring resolution rank $r$, we can obtain a related CNF formula $G=\mbox{Lift}_k (F)$ requiring refutation rank
$r^{\Omega(1/k)}/\log^{O(1)} n$ in all $R^{cc}(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.
\item We prove that there are strict hierarchies for $T^{cc}(k)$ and $R^{cc}(k)$
systems with respect to $k$. Specifically, for $k\in O(\log\log n)$, we produce unsatisfiable CNF formulas whose proofs require large rank in $R^{cc}(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 $R^{cc}(k)$ and $T^{cc}(k+1)$ follow immediately.
\item For $k\in O(\log\log n)$ we also derive $2^{n^{\Omega(1/k)}}$ lower bounds on the size of tree-like $T^{cc}(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.
\end{itemize}
This short note relates and contrasts two methods in communication complexity, a method due to
Raz and McKenzie (1997) and the pattern matrix method (2007, 2008).
We have found a mistake in our paper. Namely, Lemma 3.5 is incorrect and this renders many of the theorems in the paper incorrect. (While we still believe that the theorem statements are true, the proofs are not valid.) We refer the reader to the more recent STOC 2012 paper by Huynh and Nordstrom, ``On the Virtue of Succinct Proofs: Amplifying Communication Complexity Hardness to Time-Space Tradeoffs in Proof Complexity" where they develop this approach, using many new ideas, in order to obtain similar results for the 2-player communication complexity of search problems.
