Theorem 4 — no deterministic CVRP reformulation over first-order generic ambiguity sets
ProvedDRCVRP.FirstOrder.no_deterministic_reformulationThere is an instance of the distributionally robust CVRP whose ambiguity set has the form of the first-order generic moment ambiguity set, that is, a number of customers, a number of vehicles of capacity , a risk level , a support box with , a mean in the interior of the box, customer subsets and bounds , with the following property: for every deterministic CVRP instance with the same customers and vehicles, i.e. every capacity and every demand vector ,
This contrasts with marginalized moment ambiguity sets, over which the distributionally robust CVRP is equivalent to a deterministic CVRP with altered demands: once the ambiguity set couples the demands of different customers, the feasible route sets need not be those of any deterministic instance.
Formalization Note Route sets are R : Fin m → List (Fin n); feasibility in requires for every distribution in the ambiguity set and every vehicle. The paper takes ; the statement asks for , which only restricts the witness.
import Mathlib import Definitions.Def_DRCVRP_FirstOrder_AmbiguitySet import Definitions.Def_DRCVRP_FirstOrder_RouteSet open MeasureTheory
namespace DRCVRP.FirstOrder
/-- Theorem 4 (§5.1, p. 726): there is an instance of the distributionally robust CVRP with an
ambiguity set of the form (12) (capacity `Q > 0`, risk level `ε ∈ (0,1)`, support `[qlo, qhi]`
with `qlo ≥ 0`, mean `μ` in the interior of the box, customer subsets `Sfam`, bounds `ν > 0`)
such that no deterministic CVRP instance with the same customers and vehicles (capacity
`Q' ≥ 0`, demands `q' ≥ 0`) has the same set of feasible route sets. -/
theorem no_deterministic_reformulation :
∃ (n m : ℕ) (Q ε : ℝ) (qlo qhi μ : Fin n → ℝ) (p : ℕ) (Sfam : Fin p → Finset (Fin n))
(ν : Fin p → ℝ),
0 < Q ∧ 0 < ε ∧ ε < 1 ∧ (∀ j, 0 ≤ qlo j) ∧ (∀ j, qlo j < μ j ∧ μ j < qhi j) ∧
(∀ l, 0 < ν l) ∧
∀ (Q' : ℝ) (q' : Fin n → ℝ), 0 ≤ Q' → (∀ i, 0 ≤ q' i) →
{R : Fin m → List (Fin n) |
IsRVRPFeasible (firstOrderAmbiguitySet qlo qhi μ Sfam ν) ε Q R} ≠
{R : Fin m → List (Fin n) | IsDeterministicFeasible Q' q' R} := by sorry
end DRCVRP.FirstOrder
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.