Hardness Amplification in Proof Complexity

Time
1:30 – 2:20pm, Tuesday, April 20, 2010
Place
CSE 305
Speaker
Trinh Huynh

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

These bounds are derived by analyzing two general families of proof systems that we introduce that include Th(k) proofs as a special case and require only that each proof line (or inference) be checkable (in a certain weak sense) by an efficient k-party randomized communication protocol.

For k=O(loglog n), we prove that from any unsatisfiable CNF formula F requiring resolution rank r, we can obtain a related CNF formula G=Lift_k(F) requiring refutation rank r/ log^O(1) n in the k-party versions of these proof systems (which include Th(k-1) proofs). Since many strong lower bounds are known for resolution rank, this yields strong rank lower bounds in all of the above proof systems for large classes of natural CNF formulas.

We also prove that there are strict hierarchies of these proof systems with respect to rank. We also apply our general method to give optimal integrality gaps for low rank Th(1) proofs (which include Cutting Plane) for MAX-t-SAT.

Joint work with Paul Beame and Toniann Pitassi.