Abstract:

Cutting planes procedures are techniques for solving, or approximating
the solutions to, integer linear programs.  As such, they are used in
practice to attack NP-hard optimization problems.  They can also be used
to prove the unsatisfiability of CNF formulas.  The most common examples
of such procedures, those defined by Gomory and Chvatal and by Lovasz
and Schrijver, are applied in rounds.  For a given input, the number of
rounds needed to solve the integer linear program, or to prove that the
CNF is unsatisfiable, is called the rank of the input.  We present a new
technique for proving rank lower bounds for these procedures when viewed
as proof systems for unsatisfiability.  We use this technique to prove
near-optimal rank bounds for Gomory-Chvatal and Lovasz-Schrijver proofs
of several prominent unsatisfiable CNF examples, including random kCNF
formulas and the Tseitin graph formulas. It follows from these lower
bounds that a linear number of rounds of these procedures when applied
to relaxations of integer linear programs is not sufficient for reducing
the integrality gap.

Joint work with: Josh Buresh-Oppenheim, Nicola Galesi, Avner Magen and
Toni Pitassi