∑math20

Theoretical computer science · Result 118

Bin packing and unbounded configuration-LP gaps

1 paperLean

Disproves the modified integer round-up conjecture of Scheithauer and Terno: the integral bin-packing optimum can exceed its configuration linear-programming value by an arbitrarily large additive constant. Approximating the optimum within any fixed additive constant is also NP-hard, even when every item exceeds 1/6 and each bin holds at most five items.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of Additive hardness and unbounded configuration gaps in bin packing

Additive hardness and unbounded configuration gaps in bin packing

OpenAI · September 24, 2026

We disprove the Modified Integer Round-Up Conjecture for bin packing by constructing instances with arbitrarily large additive gaps between the configuration-LP value and the integral optimum. We also prove that, for every fixed nonnegative integer c, distinguishing instances that fit in B bins from those requiring more than \(B+c\) bins is NP-hard. Both results hold with rational item sizes greater than 1/6, so each bin contains at most five items.

Read PDF Download Source

Cite
@misc{OAI:Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026,
  author = {{OpenAI}},
  title = {{Additive hardness and unbounded configuration gaps in bin packing}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026.pdf}{OAI:Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized results rule out a universal additive bound for the configuration linear program in bin packing. For every integer \(c\ge0\), there are an integer \(B\) and a rational instance with \(5B\) items whose individual-copy and size-type configuration-LP values both equal \(B\), but whose integral optimum is greater than \(B+c\). Distinguishing a packing in \(B\) bins from the absence of one in \(B+c\) bins is NP-hard for each fixed \(c\). A deterministic polynomial-time algorithm with a fixed absolute additive allowance exists exactly when \(P=NP\); under that equality, an optimal algorithm is constructed.

Comparator links

ResultComparator statement
Unbounded configuration gaps and additive hardnessBinPackingGap.lean

Scope note on GitHub →