[Rule] MinimumMetricDimension to ILP #964
Description
Motivation
Direct ILP formulation for MinimumMetricDimension. Companion issue for #880. Enables ILP-based solving.
Source
MinimumMetricDimension
Target
ILP (Integer Linear Programming)
Reference
Standard ILP formulation for metric dimension; see Chartrand, Eroh, Johnson, Oellermann (2000).
Reduction Algorithm
Input: Graph G = (V, E) with n = |V|.
- Precompute all-pairs shortest-path distances d(u, w) for all u, w ∈ V.
- Create binary variables z_v ∈ {0, 1} for each v ∈ V (z_v = 1 means v is in the resolving set).
- For each pair of distinct vertices (u, v) with u < v, add constraint: Σ_{w: d(u,w) ≠ d(v,w)} z_w ≥ 1 (at least one landmark distinguishes u from v).
- Objective: minimize Σ_v z_v.
Solution extraction: Read z_v = 1 to identify the resolving set.
Size Overhead
| Code metric | Formula |
|---|---|
num_variables |
n |
num_constraints |
n*(n-1)/2 |
Where n = number of vertices.
Validation Method
Closed-loop test: construct graph, reduce to ILP, solve, extract resolving set, verify all distance vectors are distinct.
Example
Source: Path P3: v0—v1—v2.
Distances: d(v0,v1)=1, d(v0,v2)=2, d(v1,v2)=1.
ILP: z_0, z_1, z_2 ∈ {0,1}. Minimize z_0+z_1+z_2.
- Pair (v0,v1): d differs at w=v0(0≠1), w=v1(1≠0), w=v2(2≠1) → z_0+z_1+z_2 ≥ 1
- Pair (v0,v2): d differs at w=v0(0≠2), w=v1(1≠1)✗, w=v2(2≠0) → z_0+z_2 ≥ 1
- Pair (v1,v2): d differs at w=v0(1≠2), w=v1(0≠1), w=v2(1≠0) → z_0+z_1+z_2 ≥ 1
Optimal: z_0=1, z_1=0, z_2=0 → Min(1).