Automating Idealness Proofs for Binary Programs with Application to Rectangle Packing
An integer program is called ideal if its continuous relaxation coincides with its convex hull allowing the problem to be solved as a continuous program and offering substantial computational advantages. Proving idealness analytically can be extraordinarily tedious -- even for small formulations -- such proofs often span many pages of intricate case analysis which motivates the development of automated verification methods. We develop a general-purpose framework for certifying idealness in Mixed Binary Linear Programs (MBLPs), formulating the verification problem as a linear program when the data is fixed and as a nonconvex quadratic program when the data is parametric. We apply this framework to study several formulations of the rectangle packing problem that are conjectured to be pairwise-ideal, obtaining computational proofs where analytic proofs were previously unknown or impractical. As our second contribution, we introduce and model a novel generalization of the rectangle packing problem that enforces edge clearances between selected rectangles. We present both existing and novel MBLP formulations which arise from different encodings of the underlying disjunctive constraints. We perform some computational experiments on these formulations under a strip-packing objective to determine the importance of pairwise-idealness in practice.