Separate reduction semantics from solver execution and adopt sparse QUBO storage

[isPANN]

This PR separates mathematical model/reduction semantics from backend execution and brute-force search limits. Each executed reduction owns one target instance and the state needed to recover source solutions and interpret target optima. It also fixes affected mathematical constructions and replaces dense QUBO storage with sprs CSR matrices.

This includes behavior and public API changes, not only performance improvements.

Reduction construction, solving, and recovery

The typed mathematical API remains reduce_to() -> ReductionResult, with target_problem() and extract_solution(). Problem::evaluate() remains the model's feasibility/objective operation. A trait declares the methods an implementation supplies; it does not itself run a solver.

For a path a—b—c, reducing minimum vertex cover to maximum independent set produces a target optimum {a,c}. extract_solution() complements that assignment to recover the minimum cover {b}, whose source cost is 1.

source problem
  -> registered fixed ILP pipeline: construct and retain each reduction result
  -> native ILP
  -> HighsAdapter: encode, solve, decode, validate the terminal ILP assignment
  -> reverse traversal: interpret each optimum, then extract its source solution
  -> original problem solution and evaluation

Previously, solver completion could invoke the aggregate reduction constructor again after constructing the witness reduction. ExecutedStep now shares one result through Rc witness/value views and an optional interpret_optimum operation. The target and reverse-mapping state are constructed once. Executed-path prefix caches retain individual steps instead of copying whole chains for every prefix.

For Decision<MinimumVertexCover> on the same path with bound 0, the target optimizer returns cost 1. The stored bound establishes NO before witness extraction. A timeout or backend error remains an error; it does not become NO. Penalty reductions such as ILP→QUBO similarly use their mathematical energy relationship to distinguish source infeasibility from a recoverable target optimum.

AggregateReductionResult maps target values to source values. SolutionAggregate, which compares candidate values with an aggregate optimum, now belongs only to brute-force witness selection. Dynamic model evaluation no longer requires it.

Direct extract_solution() and pred extract assume the rule's documented witness premises, including optimality when needed. They map the supplied solution; they do not certify feasibility/optimality or repair arbitrary assignments. Redundant extractor validation and forwarding branches are removed. Typed, dynamic, and JSON recovery share the same reverse mapping.

Native ILP execution and numerical boundaries

• Fixed ILP pipelines terminate at their native integer or floating-point ILP. Runtime type dispatch stays at the registry boundary; HighsAdapter owns backend encoding, execution, decoding, and original-ILP validation.
• The adapter uses highs directly. Explicit integer-to-float mathematical reduction edges remain available independently of backend transport.
• An integer coefficient 2^53 + 1 is valid model data but cannot be transported exactly into a backend f64; the adapter reports InexactTransport instead of rejecting the mathematical model or reporting infeasibility.
• Float ILP model evaluation uses comparisons of computed floating-point values without an added feasibility tolerance. For example, 1 <= 0.9999999995 is false; the old model tolerance could accept it.
• Backend optimality remains subject to HiGHS numerical behavior. Checking a returned assignment against the original ILP is not an independent proof of exact global optimality.

Solver availability still comes from exact-variant registrations and fixed pipelines, not arbitrary reduction-graph reachability. Once a solver is selected, execution failures are returned without fallback.

Model evaluation and enumeration

BruteForceProblem::dimensions() -> Vec<usize> is replaced by fallible num_variables() and dimension(variable) methods. Models and callers are migrated together. Mixed-radix iteration no longer requires the total Cartesian product to fit usize.

For 100 Boolean coordinates, the model can evaluate a supplied assignment and the iterator can generate a prefix even though 2^100 does not fit a machine-size count. This does not make exhaustive solving practical. Unrepresentable coordinates, masks, or search tables report errors in their owning search/construction layer.

CVP now evaluates exact squared distance as Min<BigRational> and checks basis rank with arbitrary-precision integers. Its existing rational sphere-enumeration solver consumes stored coordinates directly without the previous float-transport restrictions. A displacement (3,4) has value 25 instead of the previous floating-point distance 5. Squaring preserves the mathematical minimizers but changes objective values, return types, serialized values, and numerical computation costs. Dependent thresholds and QUBO mappings are updated accordingly.

Mathematical construction and domain fixes

Area	Resulting behavior
TSP→QUBO	Signed-cost shifts, checked penalties, energy gaps, and objective offsets support optimum recovery and source-infeasibility interpretation; small instances and parallel edges follow source semantics.
MultiwayCut→QUBO	Negative-cost edges are always deleted; the QUBO optimizes the remaining nonnegative cut costs.
Discrete inverse kinematics→QUBO	Omitted constants are restored and the feasibility gap is interpreted before decoding orientations.
PCSF→SteinerTree	Prize gadgets cannot bypass component charges. With adjacent vertices, edge cost 0, prizes (1,2), beta=1, and component charge 5, every target optimum has cost 15 and extracts to source cost 3 after the offset 12.
Steiner models	SteinerTree is canonical; duplicate SteinerTreeInGraphs and its rule are removed. Signed weights are accepted, terminals must be nonempty and distinct, and selected edges must form one tree containing the terminals. A single-terminal empty tree is feasible.
Other affected rules/domains	Normalize equal-size 3-Partition pairings; register the unit-weight Decision endpoint for the Hamiltonian-circuit rule; correct set-packing parameter bounds; enforce the documented nonnegative MinimumMatrixCover and PCSF inputs.

Rule tests include tied qualifying optima, not just one solver-selected witness. Construction/evaluation/representation errors stay separate from backend limitations.

Sparse QUBO storage

QUBO stores sprs::CsMat<W> in CSR order. Inbound rules, casts, evaluation, and outgoing reductions consume sparse coefficients directly. Coefficient accumulation, checked integer arithmetic, floating-point summation order, and QUBO::new last-assignment semantics are preserved.

For E(x) = 3x0 + 5x0*x2 - 2x2, the three nonzero coefficients replace a 3×3 dense matrix; evaluating (1,0,1) still gives 6.

For a complete 100-city unit-cost TSP construction:

Quantity	Result
QUBO variables	10,000
Stored nonzero coefficients	1,990,000
CSR array bytes	31,920,008
Equivalent old dense coefficient payload, calculated	800,000,000 bytes
New process peak RSS, measured	104,677,376 bytes
Known-tour QUBO energy / recovered source cost	-990100 / 100

This experiment constructed the QUBO and evaluated/extracted a known tour; it did not solve the 10,000-variable QUBO. CSR does not guarantee lower memory for genuinely dense matrices.

Compatibility and review scope

• QUBO::matrix() returns &CsMat<W>; get(i,j) returns an owned coefficient, with zero for an unstored in-bounds entry.
• from_matrix and CLI --matrix still accept dense construction input; from_sparse accepts CSR/CSC input and normalizes storage.
• Persisted QUBO JSON uses the sprs matrix object (storage, nrows, ncols, indptr, indices, data). Variable count comes from matrix dimensions. Old dense QUBO JSON is not supported.
• CVP value types/units, brute-force capability methods, removed Steiner model names, dynamic evaluation, and direct extraction premises require caller updates. Public error handling is also updated; the PR does not promise unchanged exhaustive error matches.
• Documentation, paper examples, registration macros, CLI/MCP callers, and tests follow these contracts. Numerical and review guidance no longer imposes backend policy or arbitrary test-count gates on mathematical definitions.

The broad file count largely reflects coordinated model/caller migrations. Review the lifecycle and contracts first, then mathematical/numerical changes, and finally mechanical migrations and storage changes.

Validation

• Full make check, make mcp-test, and make paper passed during implementation.
• After the final code cleanup in 597ba9fc, focused QUBO tests (116), all-target Clippy, formatting, and the full coverage workflow passed.
• Local changed-line coverage against origin/main: 5,765 / 6,024 lines, 95.70%, without lowering the threshold or excluding changed files.
• PR CI at that revision passed tests, formatting, Clippy, coverage, and Windows/macOS/RISC-V checks.

These checks establish regression coverage and backend integration; they do not substitute for reviewing the mathematical guarantees of the changed rules.

[codecov]

Codecov Report

❌ Patch coverage is 94.11491% with 253 lines in your changes missing coverage. Please review.
✅ Project coverage is 96.30%. Comparing base (7dd5fcd) to head (bbc543d).

Files with missing lines	Patch %	Lines
src/models/misc/conjunctive_boolean_query.rs	78.31%	18 Missing ⚠️
...isc/minimum_code_generation_unlimited_registers.rs	65.95%	16 Missing ⚠️
...odels/misc/minimum_code_generation_one_register.rs	76.36%	13 Missing ⚠️
src/models/graph/minimum_edge_cost_flow.rs	78.57%	12 Missing ⚠️
src/models/misc/minimum_axiom_set.rs	74.46%	12 Missing ⚠️
src/models/graph/integral_flow_bundles.rs	85.52%	11 Missing ⚠️
src/models/graph/integral_flow_homologous_arcs.rs	84.05%	11 Missing ⚠️
src/models/graph/bounded_diameter_spanning_tree.rs	83.63%	9 Missing ⚠️
...els/graph/hamiltonian_path_between_two_vertices.rs	83.01%	9 Missing ⚠️
src/models/graph/integral_flow_with_multipliers.rs	88.15%	9 Missing ⚠️
... and 41 more

❌ Your patch status has failed because the patch coverage (94.11%) is below the target coverage (95.00%). You can increase the patch coverage or adjust the target coverage.

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1147      +/-   ##
==========================================
+ Coverage   95.93%   96.30%   +0.37%     
==========================================
  Files        1074     1072       -2     
  Lines      132106   135540    +3434     
==========================================
+ Hits       126730   130537    +3807     
+ Misses       5376     5003     -373     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.