Email Gateway (Aug 07 2026 at 14:27): Email Gateway (Aug 07 2026 at 14:27):From: Lawrence Paulson <lp15@cam.ac.uk>
Subject: [isabelle] New in the AFP: Cost-Preserving Single-Source Unsplittable Flow
The AI cascade continues. Another counterexample found using AI is now verified using AI.
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Dinitz, Garg, and Goemans proved that a feasible fractional single-source flow can be rounded to an unsplittable flow with additive congestion bounded by the largest demand. Goemans conjectured that the rounding can simultaneously preserve cost. This entry verifies the finite counterexample announced by Dmitry Rybin in July 2026. It defines a generic finite path-flow model and realizes the displayed instance as a directed graph with seven vertices, nine arcs, and three terminal demands. Isabelle classifies every source-to-terminal path and checks a feasible fractional flow of cost that saturates every arc. The maximum demand is . Any unsplittable routing whose load on every arc is at most the fractional load plus must choose at least two positive-cost routes, each costing , and therefore costs at least . Consequently no cost-preserving rounding exists, even under the weaker non-strict congestion bound.
https://isa-afp.org/entries/Dinitz_Garg_Goemans_Counterexample.html
Last updated: Aug 12 2026 at 20:47 UTC