Cutting planes and the parameter cutwidth (Q693047)

From the text: The system of Cutting Planes [\dots] provides a method for solving integer linear programs [\dots] by iteratively deriving further constraints until the problem is reduced to a general linear program (for which a polynomial algorithm is known). In terms of feasible solutions, this equates to isolating the integer hull of the solution set of the defining inequalities. It is well-known that the question as to whether a given propositional formula has a satisfying assignment can be reduced to a feasibility question for a certain [integer linear program] -- the formula is therefore a contradiction iff the associated polytope has an empty integer hull. Thus [the system of cutting planes] gives rise to a refutation system for propositional CNF (conjunctive normal form) formulae [\dots]. Resolution is perhaps the best-known refutation system for CNF, and width -- that is the maximum number of variables in any derived clause -- has shown itself to be an important parameter in its study [\dots]. We initiate an investigation of the parameter cutwidth in [the system of cutting planes] -- that is, the maximum number of variables in an inequality on which a cut operation is performed. Cutwidth manifests as a more natural parameter than width as one may have a system of inequalities of large width that are inconsistent even as a linear program, i.e. can be refuted without recourse to a single cut -- for example this is the case for inequalities that encode a CNF contradiction \(F\) that may be refuted by unit clause propagation. When one has large initial clauses in \(F\), a large Resolution width is unavoidable; therefore, it becomes necessary to add `extension' axioms to mitigate this. An advantage in our definition of cutwidth is that this need not be necessary, since we can have inequalities of arbitrary width so long as we do not perform cuts on them. We provide linear lower bounds for two polytopes. The first has a non-empty integer hull, while the second has both an empty integer hull and is the associated polytope to a contradictory CNF (itself based on the well-known least number principle). For polytopes associated with contradictions \(F\), we prove that Resolution width always provides an upper bound on cutwidth. But, we prove that the converse does not hold. [\dots W]e generate a contradiction \(F\) whose Resolution width is \(\Omega(n)\) but whose cutwidth is constant. There is a standard mechanism for converting an FO sentence \(\psi\), without finite models, into a sequence of contradictory CNFs, \(F_{\psi,n}\). A series of papers in recent years has studied so-called gap phenomena in propositional refutation systems. [\dots] A complexity gap is given for two other refutation systems based on [integer linear program] -- namely those of Lovász-Schrijver and Sherali-Adams (SA) [\dots]. In each case the relevant parameter is rank and [\dots] the separating criterion is whether or not \(\psi\) has some (infinite) model. The search for a similar gap theorem for [the system of cutting planes] is ongoing. In this paper we provide a weaker classification theorem based on the sum of cutwidth and rank. Specifically, and using the gap theorem proved for SA, we prove that the cutwidth + rank of \(F_{\psi,n}\) is bound by a constant \(c\) (depending on \(\psi\) only) iff \(\psi\) has no (infinite) models.