ECCC-Report TR09-072https://eccc.weizmann.ac.il/report/2009/072Comments and Revisions published for TR09-072en-usSun, 30 Jun 2013 20:51:53 +0300
Comment 2
| Erratum |
Toniann Pitassi
https://eccc.weizmann.ac.il/report/2009/072#comment2We 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.Sun, 30 Jun 2013 20:51:53 +0300https://eccc.weizmann.ac.il/report/2009/072#comment2
Revision 2
| Hardness Amplification in Proof Complexity |
Paul Beame,
Trinh Huynh,
Toniann Pitassi
https://eccc.weizmann.ac.il/report/2009/072#revision2We 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.
Thu, 03 Dec 2009 00:19:36 +0200https://eccc.weizmann.ac.il/report/2009/072#revision2
Comment 1
| A note on the Raz-McKenzie method and the pattern matrix method |
Alexander A. Sherstov
https://eccc.weizmann.ac.il/report/2009/072#comment1This 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).Fri, 16 Oct 2009 19:17:54 +0200https://eccc.weizmann.ac.il/report/2009/072#comment1
Revision 1
| Hardness Amplification in Proof Complexity |
Paul Beame,
Trinh Huynh
https://eccc.weizmann.ac.il/report/2009/072#revision1We 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.
Mon, 05 Oct 2009 17:08:50 +0200https://eccc.weizmann.ac.il/report/2009/072#revision1
Paper TR09-072
| Hardness Amplification in Proof Complexity |
Paul Beame,
Trinh Huynh
https://eccc.weizmann.ac.il/report/2009/072We 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}Thu, 03 Sep 2009 21:10:03 +0300https://eccc.weizmann.ac.il/report/2009/072