Symbolic growth, exact Pareto path search, and deterministic solver backends

[isPANN]

Closes #1075, #1078, #1076, #788, and #1090.

This PR combines the work previously split across #1083 and #1091.

1. Symbolic growth domain

• Adds a conservative symbolic growth representation for exponential, polynomial, and logarithmic factors.
• Replaces the old canonicalization/sampling path used by Big-O rendering and dominance checks.
• Prevents expression-expansion blowups such as pred path --all OOMs/hangs: big_o_normal_form exponentially expands composed overhead expressions #1069 while preserving symbolic exponential bases.
• Reuses the same growth domain in reduction-overhead comparison and redundancy analysis.

2. Exact and explicitly approximate path search

• Replaces scalar path selection with Pareto-aware search for concrete sizes and asymptotic growth vectors.
• Makes completeness explicit through exact versus bounded approximate search outcomes.
• Uses elementary paths and avoids unsound intermediate dominance/branch-and-bound assumptions.
• Makes bounded path enumeration and ordering deterministic.
• Exposes completeness, limit reasons, and search statistics through the CLI and MCP APIs.
• Restores saved-path round trips for pred reduce --via and gives pred path --all canonical Big-O output.

3. Deterministic solver backend registry

• Removes runtime reduction-graph search from solve; path discovery remains a separate path operation.
• Keys solver registrations by the complete source variant so capabilities cannot leak between representations.
• Registers seven native solver implementations and 151 fixed reduction-to-ILP workflows.
• Supports direct ILP<bool> and ILP<i32> terminals without forcing an additional normalization reduction.
• Uses stable default selection: native, then registered ILP workflow, then brute force.
• Adds structured solver metadata to CLI/MCP results and exact capability reporting to inspect.
• Removes the ambiguous CustomizedSolver dispatch and the old reduced_to output field.

Integration decision

The two branches overlapped in solver-side path selection. The combined implementation keeps the new growth/Pareto engine for explicit path queries, while solve uses only the fixed exact-variant registry introduced by #1091. This preserves the path-analysis work without reintroducing runtime route discovery into deterministic solving.

Verification after combining

• cargo fmt --all -- --check
• cargo check --workspace --all-targets --features ilp-highs
• make check
  • Clippy clean with -D warnings
  • 5,431 library tests passed
  • 75 integration tests passed
  • 162 CLI unit tests passed
  • 330 CLI integration tests passed
  • 17 pred-sym tests passed
  • 26 macro tests passed
  • 153 documentation tests passed

The merge commit is 3ff2300f; no force-push was used.

[codecov]

Codecov Report

❌ Patch coverage is 97.59930% with 110 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.94%. Comparing base (cb54ea0) to head (3ff2300).

Files with missing lines	Patch %	Lines
src/rules/graph.rs	94.81%	29 Missing ⚠️
src/unit_tests/growth.rs	96.17%	24 Missing ⚠️
src/unit_tests/rules/pareto.rs	98.22%	22 Missing ⚠️
src/growth.rs	98.22%	11 Missing ⚠️
src/solvers/registry.rs	95.73%	9 Missing ⚠️
src/solvers/ilp/solver.rs	86.20%	4 Missing ⚠️
src/rules/pareto.rs	97.95%	3 Missing ⚠️
src/unit_tests/solvers/brute_force.rs	83.33%	3 Missing ⚠️
src/unit_tests/solvers/registry.rs	98.70%	3 Missing ⚠️
src/solvers/resolver.rs	98.71%	1 Missing ⚠️
... and 1 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1083      +/-   ##
==========================================
- Coverage   98.00%   97.94%   -0.07%     
==========================================
  Files        1044     1051       +7     
  Lines      107366   110605    +3239     
==========================================
+ Hits       105228   108328    +3100     
- Misses       2138     2277     +139     

☔ 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.

[GiggleLiu]

Review result: request changes.

I found the following correctness blockers and significant regressions:

1. [P1] Mixed multivariate logarithms are underestimated. src/growth.rs:583 turns log(2^n * m) into O(n), dropping the required log(m) term. This invalid upper bound can corrupt Pareto dominance and pruning.

2. [P1] Measured branch-and-bound is unsound. src/rules/graph.rs:566 and :603 prune according to the current measured problem size, but reductions can shrink that size. A pruned partial route may therefore have produced the optimal final result, including with exhaustive=true.

3. [P1] Scalar cheapest-path dominance is still unsound for path-dependent costs. src/rules/pareto.rs:187 compares only accumulated cost, although future edge costs depend on current size. A cheap-but-large prefix can incorrectly delete the globally optimal cheap-and-small continuation.

4. [P1] Asymptotic fronts leak intermediate-only variables. pred path KSatisfiability QUBO --json returned bounds involving num_encoding_bits, num_vertices, and tseitin_* even though these are not KSatisfiability size fields. src/rules/pareto.rs:397 passes missing intermediate fields through as if they were source variables, making the bounds unevaluable and Pareto comparisons unreliable.

5. [P2] path --all truncates before sorting. With KSatisfiability to QUBO and max-paths 20, the response omitted a three-step route while returning ten-step routes. The cap is applied in discovery order at src/rules/graph.rs:856 / problemreductions-cli/src/commands/graph.rs:735 and only then sorted. CLI and MCP also return different truncated route sets.

6. [P2] The documented saved-path workflow is broken. The help still advertises pred path MIS QUBO -o path.json for reduce --via, but bare path now writes a front envelope without a path array. reduce --via exits with Path file missing path array.

7. [P2] src/growth.rs:493 classifies 0.5^(-n) as O(1), although it equals 2^n, because bases in (0,1] are handled before the exponent sign.

8. [P2] The claimed memory/OOM guarantee is not established. Dominated measured instances remain owned by the permanent arena, while preflight relies on uncalibrated asymptotic formulas; the bag cap therefore does not bound retained instance memory.

Verification: make test passed, including 5,386 library tests plus CLI, integration, and doc tests. Focused CLI/MCP scenarios and git diff --check also passed. The green suite does not cover the counterexamples above.

[isPANN]

Direct code review

I found four correctness/performance blockers and one documentation issue.

P1 — Exponential-base rounding breaks Big-O soundness

src/growth.rs:349-356 rounds reconstructed exponential bases to 9 decimal places. Rounding downward changes the asymptotic class, rather than merely changing presentation.

Confirmed reproducer:

pred-sym big-o '1.0000000001^n'
O(1^n)

This also affects existing declarations such as 2^(num_items / 2): it renders with base 1.414213562, which is below sqrt(2), so the displayed expression is not an upper bound. Preserve the rate symbolically, or use a representation that cannot round an exponential base downward.

P1 — The bounded path API still enumerates every simple path

src/rules/graph.rs:927-943 retains only limit paths in memory, but consumes all_simple_paths to exhaustion. Consequently, find_paths_up_to(..., 20) and the default pred path --all still perform exponential/factorial work over every simple path. This contradicts the method's "stops enumeration" contract and can reintroduce hangs as the reduction graph grows. The traversal needs to be bounded in time/work as well as retained memory, for example with a deterministic k-shortest traversal that can stop.

P1 — Size-only dominance can discard the true measured winner

src/rules/pareto.rs:329-333 compares measured labels only through coarse ProblemSize, with equality counting as dominance. Two different constructed instances at the same node can have equal component sizes but yield very different sizes under a later structure-dependent reduction. One is therefore discarded before that downstream reduction is measured. The ILP solver calls this search with exhaustive = false while the public API describes the result as the measured-smallest path. This pruning should not be enabled by default unless the label contains sufficient state or the required isotonicity is proven.

P1 — Asymptotic overhead is not a concrete budget bound

src/rules/pareto.rs:285-293 treats evaluated overhead as a pointwise upper bound. Repository semantics define these expressions as asymptotic scaling bounds, so predicted_total > budget does not prove that the actual constructed target exceeds the budget. This can prune a valid in-budget route and surface NoReductionPath. Conversely, a prediction below the budget cannot make OOM structurally impossible. The guard needs certified concrete-bound metadata or must be documented and surfaced as an incomplete heuristic rather than a sound guard.

P2 — New rustdoc links are broken

src/growth.rs:4 links to the deleted crate::canonical module. A rustdoc check also reports new unresolved/private links around ReductionGraph::pareto_search and Growth::Unknown.

Verification

• GitHub CI is green.
• Focused growth, pareto, analysis, issue-1069, and CLI-front tests passed from a clean export.
• The exponential-rounding failure above was reproduced directly.
• The randomized growth tests only generate exponential bases 2 and e, so they do not cover the rounding failure.

No branch changes were made during this review.

[isPANN]

Follow-up on Exponential-base rounding breaks Big-O soundness:

I have implemented the fix. The patch now:

• stores each exponential base symbolically together with its exponent coefficient, instead of normalizing through a floating-point log2 rate;
• renders the authoritative base directly, with no 2^rate reconstruction, decimal rounding, or epsilon snapping;
• preserves cases such as 1.0000000001^n, 3^n, 2^(n / 2), and exp(n) across parse/render/parse;
• combines only structurally identical bases and uses conservative comparison rules, returning incomparable when dominance cannot be proved;
• handles fractional-base/negative-exponent cases such as 0.5^(-n) as exponential;
• serializes the symbolic form and rejects the old transient rate-only JSON rather than guessing a base;
• adds deterministic regression, comparison, widening, Serde, and randomized round-trip tests, including bases near 1 and e.

Local verification completed:

• cargo fmt --all -- --check
• git diff --check
• cargo clippy --lib --features ilp-highs -- -D warnings
• library suite with ilp-highs: 5,301 passed, 2 ignored
• main integration suite: 75 passed
• macro suite: 26 passed
• focused growth suite: 37 passed

The full Make targets are not claimed as passing in this worktree because an unrelated pre-existing untracked tests/test_50_rules.rs currently fails to compile; that file was not modified by this patch.