Replace scalar Dijkstra with measured Pareto label-setting search (concrete-instance mode)

[isPANN]

Background

ReductionGraph::find_cheapest_path (src/rules/graph.rs) currently runs scalar Dijkstra where each edge's cost is evaluated at the problem size accumulated along the path. Two structural problems:

1. Path-dependent costs break Dijkstra. When two paths reach the same node, only the cheaper-so-far one's size is kept (graph.rs:535–539); a cheaper-but-larger intermediate state can poison downstream choices. Issue [Enhancement] ILP path selector over-prioritizes step count over final output size #788 documents a real symptom: best_path_to_ilp selects a 2-step path yielding an ILP with total size 366 where a 3-step path yields 60.
2. Formulas are not ground truth for instances. Overhead expressions are scaling upper bounds over the declared size fields (see CLAUDE.md and Complexity metadata correctness review: best-known algorithm complexities and reduction overheads #107); on structure-dependent constructions they can be arbitrarily loose, so any ranking computed purely from formulas can miss the true winner for a concrete instance.

The fix combines the standard algorithm for partial-order path costs — multi-label Pareto search (Martins 1984; McRAPTOR-style per-node bags) — with measured semantics: for a concrete instance, extending a label means actually executing the reduction and measuring the constructed target's real size. Formulas serve as pre-execution guards and ordering heuristics only.

Full design (shared overview for this batch): docs/design/symbolic-growth-domain.md, section M3 (F3b).

Objective

Replace the scalar Dijkstra with a generic Pareto label-setting search, and implement the measured concrete-instance label domain wired through all existing consumers. This fixes the correctness hole, makes OOM structurally impossible during path selection, and closes #788. (The asymptotic/instance-free label domain is a separate, later issue.)

Interface (Input → Output)

pub trait PathLabel: Clone {
    fn extend(&self, edge: &ReductionEdge) -> Option<Self>; // None = pruned by a guard; must be isotone w.r.t. dominates
    fn dominates(&self, other: &Self) -> bool;              // partial order
}

• A search function generic over L: PathLabel: In source/target node, mode, initial label → Out the Pareto front as Vec<(ReductionPath, L)>, deterministically ordered.
• Measured instance label: carries the actual constructed intermediate problem (via the existing dynamic registry dispatch) and its measured ProblemSize. extend runs the following pruning stack, in order:
  1. Symbolic pre-flight guard: evaluate the edge's overhead formula at the current measured size; if the (upper-bound) prediction already exceeds the hard size budget, return None without executing — catastrophic constructions (e.g. the 2^num_vertices edge on a large instance) are never started.
  2. Execute reduce_to(), measure the real target size; over budget → None.
  3. Branch-and-bound: prune labels whose measured size already exceeds the best completed path's final size.
  4. Componentwise measured-size dominance in the per-node bag (heuristic under a documented size-monotone-future assumption; an --exhaustive/API flag disables this one, keeping guards 1–3, which are sound).
• The winning path's constructed reduction chain is returned/reusable (no re-execution for subsequent solve/witness extraction).
• find_cheapest_path / find_cheapest_path_mode keep their signatures and return the front's best element under a deterministic tie-break (smallest final size by the existing cost function, then fewest hops, then lexicographic node names) — so src/solvers/ilp/solver.rs (best_path_to_ilp), problemreductions-cli/src/commands/reduce.rs, dispatch.rs, and mcp/tools.rs keep compiling with at most mechanical changes.

Technical recommendations (non-binding)

• Per-node bag = antichain of labels, each with a predecessor pointer for path reconstruction.
• Deterministic safety caps: hop cap 16, per-node bag cap 32 with the deterministic tie-break — never iteration-order truncation.
• Default size budget: generous (e.g. 10^7 total size units) and user-overridable; the point is refusing astronomic constructions, not micro-managing.
• Use formula-predicted sizes only to order the exploration frontier (better B&B pruning); ordering never changes the answer.
• Keep find_all_paths / find_paths_up_to untouched (they serve the --all listing use case only).
• Related: the per-edge overhead calibration test (separate issue in this milestone) is what keeps the pre-flight guard trustworthy — formulas proven to be genuine upper bounds on canonical examples.

Verification

1. [Enhancement] ILP path selector over-prioritizes step count over final output size #788 known-answer check: the reproduction from issue [Enhancement] ILP path selector over-prioritizes step count over final output size #788 — HamiltonianCircuit on the prism graph (6 vertices, 9 edges), path search to ILP — now selects the path whose measured final ILP total size is 60 (HC → HP → ConsecutiveOnesSubmatrix → ILP), not 366. Add this as a unit test; it fails on the current MinimizeStepsThenOverhead-driven Dijkstra and passes with the measured Pareto search.
2. OOM guard is real: a unit test routes an instance through a subgraph containing the 2^num_vertices overhead edge (highlyconnecteddeletion_ilp) with an instance large enough that executing that edge would allocate far beyond the budget (e.g. 64 vertices). The search completes in < 1 s, returns only within-budget alternatives (or an empty result with a clear message), and peak behavior confirms the exponential construction was never started — which proves guard 1 works. Without the pre-flight guard this test OOMs/hangs.
3. Existing behavior preserved: cargo test is green — in particular the closed-loop reduce tests that route through find_cheapest_path (e.g. minimumvertexcover_qubo, maximumindependentset_ilp) still pass.

Negative control: a unit test with a hand-built 4-node diamond graph where path P1 has lower first-edge cost but larger measured intermediate size, and P2 has higher first-edge cost but strictly better final measured size. Assert the search returns P2 as optimal. Under the old Dijkstra this test fails (it commits to P1's prefix and discards P2's state) — proving the fix is behavioral, not cosmetic.

Dependencies

None (independent of the growth domain — measured labels are numeric; the pre-flight guard uses plain Expr::eval). Milestone: Symbolic Growth Domain & Pareto Search. Closes #788.

Out of scope

Asymptotic (instance-free) search and CLI Pareto-front output — a follow-up issue depends on this one plus the growth domain. Fixing miscalibrated overhead formulas — surfaced by the calibration-test issue in this milestone.