A Checkable Proof of the Best Solution to One Optimization Benchmark

From a candidate answer to a proof

An optimization solver can find a feasible solution without establishing that it is the best possible one. For a minimization problem, that solution supplies an upper bound. Proving optimality also requires a lower bound that rules out every better feasible answer.

In a preprint, Jingyang Du, Zixiong Yi and Yang Shen report matching bounds for a frozen version of QPLIB_2096, a quadratic optimization benchmark. Their certified minimum is 7,025,720. The contribution is an exact mathematical reconstruction and computational validation of this particular instance, not evidence of a generally superior optimization algorithm.

The authors attribute exploration and refinement of the solution and certification approach to ZiYor, described as a self-evolving AI system. They distinguish that discovery process from the mathematical account and exact checks reported in the manuscript.

The partition hidden inside the model

The original formulation contains 300 binary variables, 6,900 triangle inequalities and 25 nonconvex quadratic constraints. The authors reconstruct those variables as decisions about every unordered pair among 25 items.

A zero means two items belong to the same group, or block; a one means they belong to different blocks. The triangle inequalities make these decisions consistent. If two items each share a block with a third, they must also share a block with each other. Together, the pair decisions therefore describe a partition of all 25 items.

Two separate systems of edge weights then determine what makes a partition allowable and how much it costs. Capacity weights govern feasibility. Objective costs govern the quantity being minimized. The paper emphasizes that confusing these systems would solve a different problem.

For each block, its incident capacity weight counts every edge touching the block, including internal edges, once. The authors show that the original quadratic constraints are equivalent to requiring this total to be no greater than 40,876.

The objective has another useful interpretation. Starting from the total edge cost of 9,255,176, subtract the costs of edges lying inside blocks. Minimizing the original objective is therefore equivalent to maximizing this total internal gain.

Checking every allowable block

That reformulation replaces the original model with a set-partitioning problem: choose allowable blocks so that every item appears exactly once.

The completeness of the block list is crucial. Checking only some allowable blocks could miss a better partition and would not certify the original problem.

The reported checker examines all 245,505 subsets containing between one and six items. It finds 14,981 feasible blocks, none larger than five items. Every six-item subset fails the capacity condition: the smallest incident weight among them is 47,232, above the limit of 40,876.

Because all capacity weights are nonnegative, adding items cannot reduce a block’s incident weight. Every larger block contains a six-item subset, so the six-item checks also exclude every larger possibility. This closes the completeness argument without examining all binary assignments individually.

Twenty-five prices close the gap

The remaining certificate assigns an integer price to each item. For every feasible block, the sum of its item prices must be at least its internal objective gain. These prices are mathematical quantities, not currency.

Any feasible partition covers each item exactly once. Adding its block inequalities therefore limits its total internal gain to the sum of all 25 prices: 2,229,456.

Subtracting that bound from the total edge cost gives a lower bound of 7,025,720. The supplied partition—one five-item block and five four-item blocks—achieves exactly that objective. The matching feasible solution and global lower bound establish optimality under the reported checks.

What was verified—and what was not

The authors report four fresh solver-free acceptance checks covering agreement between two frozen model formats, candidate feasibility in each format, and the integer certificate. They report zero observed constraint, bound and integrality violations. The original optimization search was not rerun.

There are important limits. Some checkers share a parser, and the validation is not a formally verified proof-assistant development. The manuscript also states that its local reproducibility delivery has no public repository or persistent identifier.

Complete enumeration remains exponential in the worst case. The small feasible blocks and exact bound closure are properties of this instance, not general guarantees. The result illustrates a narrower distinction: a numerical search can suggest an answer, while a separately checked certificate explains why no better feasible answer exists.