MathIdeasResearch in progressRepository ↗
← Research catalogOriginal Markdown ↓

Facility-plan checking against an existing solver

Eight generated unweighted metric instances compare a bounded exact reference with OR-Tools 9.15.6755, using the preserved isolated Python3.12 environment, a two-second time limit, one worker and seed125. Costs are scaled by their exact common denominator, without rounding; adapter scales above one million or coefficient sums above2^60 are refused. Timings and solver bounds are diagnostic reports, not certified interval quantities or general benchmarks.

Generated case Solver status Independently checked proposal cost Bounded enumeration optimum Reference subsets examined
line_distinct OPTIMAL 17 17 6
rational_line OPTIMAL 16/7 16/7 6
grid_25 OPTIMAL 37 37 120
empty_clients OPTIMAL 0 0 0
zero_optimum OPTIMAL 0 0 2
dual_tight_line OPTIMAL 3 3 2
restricted_candidates OPTIMAL 18 18 3
budget_limited_24 FEASIBLE 12 unknown 10

The first seven cases already match conventional solver results. The 24-location/12-site case has 2,704,156 possible exactly-k subsets; this control caps enumeration at ten. Its initial independent result stays unknown even though the solver proposes a cost 12 plan. Full comparison/runtime record.

A separate exact certificate closes that particular gap: assign alpha_j = 1 for each of 24 clients, beta_jf = 1 only at the same client/facility index and zero otherwise, and lambda = 1. All distinct line distances are at least 1, so the dual inequalities hold. Its lower bound is24 - 12 = 12. The checked solver proposal also costs12; therefore the finite optimum is 12 even though the solver status is FEASIBLE. Exact input, dual, completed independent result.

This dual was constructed for the generated instance, not extracted from or authenticated by OR-Tools. It does not automatically certify arbitrary solver best bounds. Another three-point example closes a gap from lower 1 to exact 3. Equal primal/dual costs establish an optimum for the exact declared model; they establish no physical distance, demand or omitted-constraint fidelity.

5,127 reference controls, 34 solver controls, four added dual controls. Exhaustion grants only completed bounds/witnesses. The current utility is strict, unweighted and uncapacitated, with48location,128-bit rational and enumeration caps. Source construction/kernel/program, formal Python proof, real customer workload and commercial advantage remain unverified. Product decision.