Automating Idealness Proofs for Binary Programs with Application to Rectangle Packing

TL;DR

The paper introduces Ideal O'Matic, a framework for certifying idealness in mixed binary linear programs by translating the verification into a linear program for fixed data and a nonconvex quadratic program for parametric data. It applies this framework to rectangle packing formulations with clearances, providing computational proofs that several previously conjectured pairwise-ideal designs are indeed ideal, and identifies a counterexample to an existing binary formulation. A novel clearance-enabled rectangle packing variant is developed, and different MBLP embeddings (unary and binary with selector functions) are analyzed, including a new multilinear selector approach. Extensive computational experiments assess the practical impact of pairwise idealness and demonstrate how sequence-pair inequalities and branching strategies influence solver performance. The work combines (i) a principled, automated proof framework, (ii) novel formulations for RPP with edge clearances, and (iii) critical insights into when idealness translates into practical performance gains.

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.

Figures (9)

• Figure 1: Some options for the penalty function $\phi$. We use (\ref{['PenFunc:Abs']}) as it can be encoded with linear constraints, whereas the quadratic version (\ref{['PenFunc:Quad']}) introduces unnecessary nonlinearities.
• Figure 2: Examples of Clearance Occlusion
• Figure 3: Visualization of the parameters
• Figure 4: The four disjunctive cases for non-overlapping rectangles $i$ (blue) and $j$ (orange), with their corresponding binary encodings $\boldsymbol{\delta} = (\delta_{ij}, \delta_{ji})$ used in the binary formulations.
• Figure 5: Two possible initial solutions to the $N=50$ Strip Packing Problem.

Theorems & Definitions (36)

• Definition 1: Ideal
• Definition 2
• Definition 3: Alternate Ideal Definition
• Proposition 1
• Corollary 1
• proof
• Remark 1
• Remark 2
• Remark 3
• Remark 4