Cutting Planes and the Parameter Cutwidth

We introduce the parameter cutwidth for the Cutting Planes (CP) system of Gomory and Chv´atal. We provide linear lower bounds on cutwidth for two simple polytopes. Considering CP as a propositional refutation system, one can see that the cutwidth of a CNF contradiction F is always bound above by the Resolution width of F. We provide an example proving that the converse fails: there is an F which has constant cutwidth, but has Resolution width Ω(n). Following a standard method for converting an FO sentence ψ, without finite models, into a sequence of CNFs, Fψ,n, we provide a classification theorem for CP based on the sum cutwidth plus rank. Specifically, the cutwidth+rank of Fψ,n is bound by a constant c (depending on ψ only) iff ψ has no (infinite) models. This result may be seen as a relative of various gap theorems extant in the literature.

• Type: Conference
• Year: 2009
• Where: CIE
• Authors: Stefan S. Dantchev, Barnaby Martin
• Keywords: Applied Computing, CIE 2009, Linear Lower Bounds, Propositional Refutation System, Resolution Width