# 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](comparison.json).

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](budget_limited_24-input.json), [dual](budget_limited_24-dual.json), [completed independent result](budget_limited_24-dual-result.json).

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](../../snapshots/2026-10-08-baseline/metric-facility-reference-validation-2026-10-09-v1.json), [34 solver controls](../../snapshots/2026-10-08-baseline/metric-facility-solver-validation-2026-10-09-v1.json), [four added dual controls](../../snapshots/2026-10-08-baseline/metric-facility-dual-extension-validation-2026-10-09-v1.json). 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](../../opportunities/011-facility-placement-planner/2026-10-09-v2.md).