Monotonicity of the bin-packing number:
ProvedLysgaardCVRP.Shrink.binPackingNumber_union_gebin-packingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1vehicle-routing
Let be the vehicle capacity and let every customer have an integer demand with . For any two sets of customers, with the bin-packing number,
This is the step of the proof of Proposition 1 that compares the right-hand sides of the capacity inequalities on and on .
Formalization Note The hypothesis makes a genuine minimum; the positivity of demands and capacity are the paper's standing assumptions.
Preamble
import Mathlib import Definitions.Def_LysgaardCVRP_Shrink_binPackingNumber
Formal statement
namespace LysgaardCVRP.Shrink
/-- Monotonicity of the bin-packing number, in the form used in the proof of Proposition 1 of
Lysgaard, Letchford & Eglese, *A new branch-and-cut algorithm for the capacitated vehicle
routing problem*, Math. Program. Ser. A 100 (2004), p. 426 (PDF p. 4) (unnumbered): "It is trivially true that
$2r(S\cup T) - 2r(T) \ge 0$".
**Formalization Note.** Stated for customer sets `S`, `T` (not containing the depot `0`) under
the paper's standing hypotheses $Q > 0$ and $0 < q_i \le Q$ for every customer (§1, p. 423); the
hypothesis $q_i \le Q$ is what makes `binPackingNumber` a genuine minimum rather than the junk
value `sInf ∅ = 0`. -/
theorem binPackingNumber_union_ge {n : ℕ} (q : Fin (n + 1) → ℕ) (Q : ℝ) (hQ : 0 < Q)
(hq : ∀ i : Fin (n + 1), i ≠ 0 → 0 < q i ∧ (q i : ℝ) ≤ Q)
(S T : Finset (Fin (n + 1))) (hS0 : (0 : Fin (n + 1)) ∉ S) (hT0 : (0 : Fin (n + 1)) ∉ T) :
0 ≤ 2 * (binPackingNumber q Q (S ∪ T) : ℝ) - 2 * (binPackingNumber q Q T : ℝ) := by sorry
end LysgaardCVRP.Shrink
Source
Lysgaard, Letchford & Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Math. Program. Ser. A 100 (2004), p. 426 (PDF p. 4), proof of Proposition 1
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.