Automating Idealness Proofs for Binary Programs with Application to Rectangle Packing

TL;DR

This paper introduces a framework for automatically certifying the idealness of mixed binary linear programs, applied to rectangle packing problems, enabling computational proofs where manual proofs are infeasible.

Contribution

It develops a general verification framework for idealness in MBLPs and applies it to rectangle packing, including a new problem variant with edge clearances.

Findings

Successfully certified idealness of rectangle packing formulations.

Demonstrated computational proofs for conjectured idealness.

Analyzed the practical impact of idealness in packing problems.

Abstract

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.