Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #2 to TR09-072 | 3rd December 2009 00:19

Hardness Amplification in Proof Complexity

RSS-Feed




Revision #2
Authors: Paul Beame, Trinh Huynh, Toniann Pitassi
Accepted on: 3rd December 2009 00:19
Downloads: 1310
Keywords: 


Abstract:

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.



Changes to previous version:

Integrality gaps added


Revision #1 to TR09-072 | 5th October 2009 17:08

Hardness Amplification in Proof Complexity





Revision #1
Authors: Paul Beame, Trinh Huynh
Accepted on: 5th October 2009 17:08
Downloads: 1169
Keywords: 


Abstract:

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.


Paper:

TR09-072 | 3rd September 2009 09:14

Hardness Amplification in Proof Complexity





TR09-072
Authors: Paul Beame, Trinh Huynh
Publication: 3rd September 2009 21:10
Downloads: 2077
Keywords: 


Abstract:

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}


Comment(s):

Comment #1 to TR09-072 | 16th October 2009 19:17

A note on the Raz-McKenzie method and the pattern matrix method





Comment #1
Authors: Alexander A. Sherstov
Accepted on: 16th October 2009 19:17
Downloads: 1616
Keywords: 


Abstract:

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).


Comment #2 to TR09-072 | 30th June 2013 20:51

Erratum

Authors: Toniann Pitassi
Accepted on: 30th June 2013 20:51
Keywords: 


Comment:

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.




ISSN 1433-8092 | Imprint