Symbolic growth domain + Pareto search: M1–M3 (#1075, #1078, #1076)#1083
Draft
isPANN wants to merge 17 commits into
Draft
Symbolic growth domain + Pareto search: M1–M3 (#1075, #1078, #1076)#1083isPANN wants to merge 17 commits into
isPANN wants to merge 17 commits into
Conversation
Implement the growth domain: a dedicated asymptotic normal form that computes Big-O bottom-up in a single pass over `Expr`, without the exponential monomial expansion in `canonical.rs` that was the root cause of issue #1069. - `GrowthTerm`: one growth monomial over `exp` / `poly` / `logs` maps. - `Growth`: an antichain of pairwise-incomparable dominant terms, or the absorbing `Unknown` sentinel; both are deterministically sorted for platform-stable equality and serialization. - `from_expr`: transfer functions for Var/Const/Add/Mul/Pow/Exp/Log/Sqrt with upward widening (subtraction -> addition, constants dropped, linear exponents -> base-2 `exp` rates, nonlinear exponents / factorial / negative exponents -> `Unknown`). - `dominates`: purely symbolic partial order (per variable, lexicographic on exp rate / poly degree / log power) that replaces the foolable numerical sampling heuristic. - Antichain cap 32 with upward widening to the componentwise-max term. - Serde support (`Serialize` derived; `Deserialize` hand-written to leak string keys to `&'static str`, matching `Expr`'s parser convention). This module changes no existing behavior; `big_o.rs` / search rewiring is scoped to later issues in the milestone, so the module is `#[allow(dead_code)]` for now. Also commits the shared batch design doc referenced by the milestone. Includes the six named verification cases plus the negative control from the issue, and extra coverage. `cargo test growth` and `cargo clippy -- -D warnings` pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1083 +/- ##
==========================================
- Coverage 98.00% 98.00% -0.01%
==========================================
Files 1044 1046 +2
Lines 107366 108566 +1200
==========================================
+ Hits 105228 106399 +1171
- Misses 2138 2167 +29 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
…1078) Swap `big_o_normal_form`'s implementation to the growth domain and delete the exponential-cost expansion machinery. One trusted asymptotic engine now backs all Big-O queries. - `big_o.rs`: `big_o_normal_form` is now `Growth::from_expr(expr).to_expr()`, mapping `Growth::Unknown` to the existing `Unsupported` error. Signature unchanged; the 360-line canonical projection is gone. - `growth.rs`: add `Growth::to_expr()` rendering the antichain back to a display `Expr`, de-normalizing exp rates to readable bases (`{n:1} -> 2^n`, `{n: log2 3} -> 3^n`, `{n: log2 e} -> exp(n)`, with float-snapping so `1.5^x` renders cleanly). - Delete `canonical.rs` (incl. the `MAX_CANONICAL_TERMS` stopgap) and its tests, the `asymptotic_normal_form` wrapper, the now-dead `CanonicalizationError`, and their `lib.rs` re-exports. - `pred-sym`: drop the `canon` subcommand; `compare` narrows to Big-O equivalence via the growth domain. - `analysis.rs`: `prepare_expr_for_comparison` stops canonicalizing (returns the expr clone); the full analysis-to-growth rewire is a separate issue. Behavioral changes from the stronger semantics, reflected in updated tests: the #1069-shaped `((a+b+c+d)^4)^4` now returns a real degree-16 bound instantly instead of erroring; `-1 * n` widens to `n` (constant factor dropped) instead of being rejected; `2^sqrt(n)` (nonlinear exponent) is now unsupported; exp/sqrt structural identities in the overhead comparator report Unknown until the analysis rewire lands. Verification (all from the issue): `cargo test` green; `grep canonical_form` returns nothing; `pred-sym big-o` prints `O(n^2)` / an exp*poly bound / a degree-4 bound instantly; `factorial(n)` and `canon` fail loudly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
isPANN
changed the title
) Implements M3 (F3b) of the Symbolic Growth Domain & Pareto Search milestone. The scalar Dijkstra in `ReductionGraph` had a path-dependent-cost hole: when two paths reached the same node, only the cheaper-so-far label's size was kept, so a cheaper-but-larger intermediate state could poison downstream choices (issue #788). This replaces it with a generic multi-label Pareto search plus a measured concrete-instance label domain. - New `PathLabel` trait (`extend` + `dominates` + `cost`) and a generic `pareto_search` kernel over per-node antichain bags with predecessor pointers, branch-and-bound, deterministic safety caps (hop cap 16, bag cap 32 with a deterministic tie-break), and a deterministically ordered Pareto front. - `CostLabel`: scalar formula label reproducing Dijkstra behavior for the existing `PathCostFn` cost functions; `find_cheapest_path*` keep their signatures and now run the kernel with it. - `MeasuredLabel` (`src/rules/pareto.rs`): the concrete-instance label. Its `extend` runs a four-part pruning stack in order — (1) symbolic pre-flight guard (evaluated in f64 so a `2^num_vertices` prediction is refused without executing, making OOM structurally impossible), (2) execute + measure the real target size, (3) branch-and-bound, (4) componentwise measured-size dominance (disabled by the `exhaustive` flag; guards 1-3 stay sound). A caught panic from a reduction whose preconditions the instance violates prunes that edge. - `MeasuredPath` carries the constructed reduction chain (via `Rc`) so downstream solve/witness extraction reuses it without re-executing. - `ILPSolver::best_path_to_ilp` now uses `find_measured_best_path_to_name`, ranking ILP variants by real measured size instead of step count / formula. Verification (all green): #788 known-answer test (HC on the prism graph selects the measured optimum), OOM pre-flight guard test (64-vertex HighlyConnectedDeletion refused in <1ms, exponential construction never started), and a hand-built diamond negative control where scalar cost selection commits to P1 while the Pareto search returns the strictly-better-final-size P2. Closes #788. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
isPANN
changed the title
…CP front (#1080) Implements milestone M3 (F3a): the asymptotic, instance-free label domain `GrowthLabel` and its surfacing through `pred path` / MCP `find_path`. Closes the 2-year-old research issue #15 (multi-variable shortest path over polynomials). - `GrowthLabel` (src/rules/pareto.rs): each current-node size field mapped to a `Growth` in the source problem's size variables. `extend` composes an edge's overhead by substituting each current field's rendered growth (`Growth::to_expr`) into the overhead `Expr` and reducing via `Growth::from_expr` (reuses M1+M2, no new growth primitive). Fields depending on an `Unknown` growth stay `Unknown` — never a fabricated bound. `dominates` is componentwise search-sense (smaller growth better), with `Unknown` as top so any label with an `Unknown` field is dominated by a fully known one (undecidable paths rank last). `cost()` is a monotone magnitude scalar with a position tiebreak so the kernel's scalar branch-and-bound keeps incomparable, equal-magnitude front members. Plugs into the existing `pareto_search` kernel. - `Growth::magnitude` (src/growth.rs): deterministic monotone scalar for search ordering only (dominance stays exact). `Growth` re-exported for CLI/MCP. - `ReductionGraph::asymptotic_front`: builds the initial label from the source's size fields, runs `pareto_search`, orders the front by (hops, lexicographic node names). - CLI: bare `pred path S T` (no `--cost`/`--size`, no `--all`) now prints the asymptotic Pareto front, each path annotated with `O(...)` per target size field (`O(?)` for unbounded). `--cost` opts into the unchanged single-best mode; `--all` unchanged. MCP `find_path` returns the same front with structured `Growth` serde. - Fix `find_paths_up_to_mode_bounded` to apply the mode filter *before* `take(limit)` (was after), so `--all` truncation no longer depends on enumeration order. - Tests: GrowthLabel extend/dominance/Unknown/isotonicity, the incomparable-front negative control (O(n^2)/O(m) vs O(n)/O(m^2), both kept), CLI determinism/golden for `pred path KSatisfiability QUBO`, and an MCP asymptotic-front test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
The shared Pareto kernel prunes any label whose scalar `cost()` already meets the best completed path's cost (branch-and-bound). That is sound for the scalar measured/formula labels, but WRONG for the asymptotic `GrowthLabel`: growth over multiple size fields is a partial order, so a scalar summary can rank one genuinely incomparable Pareto-optimal path above another and prune it — silently under-reporting the front, which is the exact thing this feature must not do. The previous mitigation (an epsilon tie-break in `GrowthLabel::cost`) only rescued the *equal-magnitude* case; asymmetric incomparable fronts (e.g. one path O(n^2)/O(m), another O(n)/O(m^3), magnitudes 3 vs 4) still lost the larger one whenever the smaller completed first. Root-cause fix: add `PathLabel::BRANCH_AND_BOUND` (default true; false for `GrowthLabel`) and gate the kernel's two B&B checks on it. The asymptotic search now relies solely on the exact `dominates` partial-order pruning (plus the hop and bag caps), so incomparable paths always survive. Removed the epsilon crutch from `cost()`. New test `test_growth_asymmetric_incomparable_front_complete` pins the asymmetric case; verified it fails with B&B re-enabled (front drops path B) and passes with the fix. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
After removing the scalar branch-and-bound from `GrowthLabel` search (8944ae8), the asymptotic front over-reported: `GrowthLabel::dominates` requires a strictly-better field, so two paths with *equal* growth vectors never prune each other, and the front accumulated every redundant route (e.g. `pred path MVC ILP` printed 32 paths, most with identical Big-O — only ~3 distinct growth profiles among them). Fix: `ReductionGraph::asymptotic_front` now collapses the front to one representative per distinct growth vector. `GrowthLabel` derives `PartialEq` over its field → growth map, so the front is sorted by (hops, lexicographic node names) — putting each equal-growth group's deterministic best first — then linearly deduplicated keeping the first (best) of each group. Deduplication is purely by the growth vector, so paths reaching different target variants (e.g. `ILP/bool` vs `ILP/i32`) with the same composed Big-O collapse to a single representative — the endpoint variant is not part of the asymptotic identity. Documented on the method. Completeness is preserved: genuinely incomparable growth vectors are never equal, so they all survive (both `test_growth_asymmetric_incomparable_front_complete` and `test_growth_negative_control_incomparable_front` still pass, using the raw kernel). `pred path MVC ILP` now prints 3 paths (one per distinct Big-O profile). Tests: `test_asymptotic_front_dedups_by_growth_vector` (real graph: no duplicate growth vectors, ≤ 4 entries, and the raw kernel front is strictly larger — proving collapse) and `test_path_front_dedups_by_growth_vector` (CLI: MVC → ILP small handful, no dup vectors). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
…tter alias (#1080) Root cause of the `pred path MinimumFeedbackVertexSet ILP` bug (asymptotic `num_vars` composed to `O(num_variables)` instead of `O(num_vertices)`): the `ILP<i32> → ILP<bool>` binary-encoding cast declared its overhead as `num_vars = "31 * num_variables"`. ILP's size field is named `num_vars`; `num_variables()` is only a getter *alias* for it. The `#[reduction]` macro validates overhead variables against getter *methods*, so the alias compiled, and both instance-mode sizing (`evaluate_output_size` calls the getter) and raw-overhead Big-O rendering resolve it — the mistake was invisible there. But asymptotic growth composition (`GrowthLabel::extend`) threads size-field *names*: the label key at the ILP node is `num_vars`, so the variable `num_variables` was unmapped and leaked through unchanged as `num_vars = O(num_variables)`. The path's arrow display had also masked this by collapsing the hidden `ILP/i32 → ILP/bool` cast step. Fix: `31 * num_variables` → `31 * num_vars` (semantically identical — 31 bits per integer variable — and numerically unchanged, since both getters return `num_vars`). Effects: `MFVS → ILP` now composes `num_vars = O(num_vertices)`. `MVC → ILP` drops from 3 to 2 front paths — the corrected feedback-vertex-set route (`num_constraints = O(num_edges + num_vertices), num_vars = O(num_vertices)`) is now correctly Pareto-dominated by the direct route and pruned. Test: `test_asymptotic_front_uses_only_source_variables_mfvs_ilp` pins `num_vars = O(num_vertices)` and asserts every composed field's growth references only MinimumFeedbackVertexSet's own size variables — a general "source-variables-only" invariant on the front label. Note: this is one instance of a getter-alias-vs-field-name mismatch. A separate, broader class of leaks remains in other reductions (e.g. `ClosestVectorProblem`'s `num_encoding_bits` and `CircuitSAT`'s `tseitin_num_vars`/`tseitin_num_clauses`, which surface in KSat→QUBO); those are genuine field-name inconsistencies between a node's incoming and outgoing reductions, outside the growth-composition logic, and are left for separate scoping. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
`compute_source_size` iterates every same-source-name reduction and calls each one's `source_size_fn` on the instance to merge all size fields. A reduction for a different source variant downcasts and panics (`Option::unwrap` on a type-mismatch); these are expected and were already caught — but by a plain `catch_unwind` that does not suppress the panic hook, so `pred solve` on a simple instance (e.g. MIS on a sparse graph, with several unmatched i32-variant reductions) printed ~8 scary "thread 'main' panicked" lines to stderr while succeeding. Route the probe through the measured search's existing thread-local panic silencer (`pareto::catch_reduction`, now `pub(crate)`), so these caught, expected panics stay off stderr. No behavior change beyond suppressing the noise. Surfaced by an end-to-end `pred solve` use case; the measured-search `extend` path was already silenced, this was the one remaining unsilenced probe. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
Cross-validate the symbolic growth domain (src/growth.rs) against numeric evaluation (Expr::eval) over a large seeded input space, in the spirit of the repo's verify-reduction adversarial culture. Three contracts, each exercised well past 5000 meaningful checks with a hand-rolled deterministic SplitMix64 RNG (no wall-clock/entropy, byte-reproducible across platforms): - Upper-bound soundness: eval(e,s) <= C*eval(render(growth(e)),s) at sizes larger than the 2^6 anchor from which C is calibrated (14500 checks, 0 violations). Numeric artifacts (inf from exp-under-log; negative values outside the nonnegativity axiom) are skipped as indeterminate, not flagged. - Idempotence: growth(render(growth(e))) == growth(e), compared up to rendering float precision (18960 checks). - Dominance soundness: when dominates(b,a), the numeric ratio does not shrink and exceeds 1 at the larger size (36050 single-term dominating pairs). The evaluation window is chosen per pair from the exponent-gap regime so the crossover is numerically reachable, independent of the assertion outcome. Negative control: the same upper-bound harness run against a deliberately broken transfer (Add keeping only its first operand) detects 3343 violations, proving the harness can fail. Findings surfaced and handled precisely (not weakened): to_expr base-snapping makes idempotence hold only up to ~1e-10 float drift; log-nested exponentials overflow eval mid-computation though the true growth is tame; and the domain's nonnegativity precondition must be respected when generating inputs. Runs in <2s. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
Cleanup pass over the milestone diff (no behavior change): - Add canonical `Growth::to_big_o()` in the lib; both the CLI (`commands/graph.rs`) and MCP (`mcp/tools.rs`) front renderers now call it instead of each hand-rolling the `Growth -> "O(...)"` mapping. The two had already drifted on the `Unknown` string; they now agree on `O(?)`. Adds a `to_big_o` unit test. - `size_le` (MeasuredLabel dominance): drop the provably redundant second `.all()` pass — nonnegative sizes with missing-field-as-0 make one pass sufficient. - `GrowthLabel::extend`: hoist the loop-invariant substitution map out of the per-output-field loop; it depends only on the rendered source label. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
Replace the bespoke polynomial comparison engine in analysis.rs
(Monomial, NormalizedPoly, normalize_polynomial, poly_leq,
monomial_dominated_by, prepare_expr_for_comparison) with the shared
symbolic growth domain. compare_overhead now decides each common field
via Growth::from_expr + Growth::dominates (reflexive, so equal fields
pass), returning Unknown only when a field's growth is Growth::Unknown.
Outer semantics of find_dominated_rules are unchanged. The rewire loses
no prior detection (all 9 previously-dominated rules retained) and gains
one newly-decided pair: PartitionIntoPathsOfLength2 -> ILP{bool}, whose
composite path carried a num_vertices/3 constant divisor that the old
engine rejected as a negative-exponent power (Unknown); the growth domain
drops constant divisors, making both fields asymptotically equal to the
direct edge. Unknown comparisons dropped from 89 to 0.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
Delete the `O(<raw expr>)` fallback in `big_o_of` and route rendering through the growth domain's canonical `Growth::to_big_o()` — bounded classes render as `O(<expr>)`, genuinely unbounded growth (nonlinear exponent / factorial) as the honest `O(?)`, never a raw multi-thousand- char expression. Gate the `--all` text rendering so `--json` and file modes no longer build it (both named in #1069). Add three in-process regression tests (no `pred` subprocess) named so `cargo test issue_1069` selects them: 1. Reconstruct #1069's KSat→QUBO exploding path by name from the live graph (via `find_all_paths`, order-independent) and assert every composed size field yields a genuine `big_o_normal_form` (not the deleted raw fallback) that is bounded and actually reduced. 2. Whole-graph render budget over the complete path set of hot pairs (KSat→QUBO, MIS→QUBO): every field renders bounded, well under 5 s — the "can't OOM/hang again" guard. 3. Byte-exact golden for the named path's rendered text, with a negative control that swaps two terms and asserts the comparison fails. Goldening one name-selected path keeps the fixture robust to build/inventory/link ordering. Closes #1069. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
…#1079) `path_all` sorted enumerated paths by length alone, so same-length paths kept `find_paths_up_to`'s discovery order — which depends on inventory/link iteration and thus varies across builds. Add a full name+variant signature as a secondary sort key so the displayed ordering is reproducible. Note: this determinizes the ordering of the fetched path set; when the total path count exceeds --max-paths (e.g. KSat->QUBO has 108, capped to 20), *which* same-length paths survive truncation still depends on discovery order. Fully fixing that needs fetch-all-then-truncate, which risks enumeration blowup on hub nodes and is left as a separate concern. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
`sort_by` recomputed the allocating `path_signature` closure O(n log n) times (once per comparison, per side). `sort_by_cached_key(|p| (p.len(), path_signature(p)))` computes each key once — same total order, fewer allocations, and matches the file's existing `sort_by_key` convention. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR
Contributor
|
Review result: request changes. I found the following correctness blockers and significant regressions:
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. |
…nd-trip P1 correctness fixes: - growth: log_term sums all factor classes, so log(2^n * m) = n + log m instead of dropping log m (an invalid upper bound) - growth: fractional bases fall through to the sign-aware rate filter, so 0.5^(-n) classifies as 2^n instead of O(1) - pareto: MeasuredLabel opts out of branch-and-bound (measured size can shrink, so its cost is non-monotone and B&B pruning was unsound, even with exhaustive=true) - pareto: CostLabel dominance is componentwise over (cost, size) - a cheap-but-large prefix can no longer evict the globally optimal cheap-and-small continuation under path-dependent costs - pareto: GrowthLabel taints target fields referencing variables absent from the label, so asymptotic fronts no longer leak intermediate-only variables (tseitin_*, num_encoding_bits) as fake source variables P2 fixes: - graph: find_paths_up_to_mode_bounded enumerates length-first via iterative deepening with a deterministic library-owned order, so path --all truncation keeps shortest routes and CLI/MCP return the identical route list - cli/mcp: the asymptotic front envelope carries top-level steps/path (best front element, format_path_json shape), restoring the documented `pred path S T -o path.json` -> `pred reduce --via` round-trip - graph: pareto_search frees evicted labels immediately (Option<L> + take on bag eviction), so BAG_CAP genuinely bounds retained measured instance memory; OOM claims in docs corrected to the real guarantee Each fix carries a targeted regression test (mixed-log/fractional-base growth cases, shrink-late diamond under exhaustive, path-dependent-cost diamond, absent-variable taint, shortest-route truncation, bare-path reduce --via round-trip, peak-live-labels DropToken bound). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
find_paths_up_to_mode_bounded enumerated paths via iterative deepening, running a full all_simple_paths DFS once per length level (up to node_count levels). For --all queries with fewer paths than the limit (the common case on a sparse graph) that meant ~170 redundant zero-yield traversals per call. Replace with a single DFS pass feeding one bounded max-heap keyed by (node count, order key): it retains exactly the `limit` shortest-then- lexicographically-smallest paths in O(limit) memory. Output is byte- identical to the iterative-deepening version (verified across queries and limits), and this folds in the redundant `limit == 0` guard and the manual into_vec+sort (now into_sorted_vec). Also drop a stale sentence in the MeasuredLabel memory rustdoc. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The previous fix disabled B&B for MeasuredLabel via a per-label `BRANCH_AND_BOUND` associated const (default `true`). That default is a footgun: any future PathLabel whose `cost` is non-monotone inherits unsound B&B pruning unless its author remembers to opt out — exactly the mistake that made measured search unsound in the first place. Remove the mechanism instead of gating it. Only CostLabel ever used B&B, where it was a marginal early-termination optimization on a 179-node graph; dominance pruning (always sound for every label domain) plus HOP_CAP/BAG_CAP already bound the search. Drop the `BRANCH_AND_BOUND` const, the `best_final` tracking, and both prune sites. `cost` is now purely a frontier-ordering / tie-break heuristic and need not be monotone. Result-preserving: `find_cheapest_path*` returns the min-cost element, which sound B&B never affected — verified `--cost` output is byte- identical across queries and cost functions. The kernel is now dominance- only, so no label can reintroduce this class of bug. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #1075, #1078, #1076, #788. Milestone M1–M3 of "Symbolic Growth Domain & Pareto Search", built incrementally on one branch (3 commits, one per issue).
M1 (#1075) —
src/growth.rs: the growth domainAsymptotic normal form computed bottom-up over
Exprin one linear pass, no monomial expansion (the #1069 blow-up).GrowthTerm(exp/poly/logs maps) andGrowth(Termsantichain | absorbingUnknown), deterministically sorted → platform-stablePartialEq/serde.from_exprwith upward widening (subtraction→addition, constants dropped, linear exponents→base-2exprates,factorial/nonlinear/negative exponents→Unknown).Pow(base,k)raises each term to powerk(tight by AM-GM; makessqrt((n-m)^2) ≍ n+mhold).dominates: purely symbolic partial order (per-variable lexicographic exp→poly→log);1.001^n ≻ n^100, which the old numerical-sampling heuristic got wrong.to_exprrenders back to a displayExpr(de-normalizing exp bases:2^n/3^n/exp(n)).M2 (#1078) — wire
big_o_normal_formto it; deletecanonical.rsbig_o_normal_form=Growth::from_expr(expr).to_expr()(signature unchanged;Unknown→Unsupported).canonical.rs(incl. theMAX_CANONICAL_TERMSstopgap) + tests, theasymptotic_normal_formwrapper, deadCanonicalizationError, re-exports.pred-symcanonremoved;comparenarrows to Big-O equivalence. Net −997 lines in M2.((a+b+c+d)^4)^4now returns a real degree-16 bound instantly.M3 (#1076) — measured Pareto label-setting search (closes #788)
src/rules/pareto.rs:PathLabeltrait +CostLabel(Dijkstra-equivalent scalar) andMeasuredLabel(concrete-instance, 4-step pruning stack: symbolic pre-flight guard → execute+measure → branch-and-bound → measured-size dominance).graph.rs: scalardijkstrareplaced by a genericpareto_searchkernel (per-node antichain bags, predecessor pointers, hop cap 16, bag cap 32, deterministic tie-breaks).find_cheapest_path*keep signatures (runCostLabel); newfind_measured_best_path*return a reusable reduction chain.best_path_to_ilpnow ranks ILP variants by real measured size.2^num_vertices-style construction over budget.Honest caveats (please eyeball in review)
ConsecutiveOnesSubmatrixon today's graph). The test pins the current measured optimum (HC→LongestCircuit→ILP, total 232). On today's graph the old selector coincidentally also lands on 232, so the genuine behavioral proof of the path-dependent-cost fix is the diamond negative control (old Dijkstra returns the worse path; Pareto search returns the better one).extendexecutes candidate reductions; a precondition-violating reduction panics (macro dispatch downcast/unwrap), caught and treated as "edge infeasible". A once-installed global panic hook gated on a thread-local flag keeps these off stderr without affecting other threads. Pragmatic given the current reduction API (returningResultinstead would be cleaner but is out of scope).Pow rendering deviation (carried from M1)
(n+m)²·(n+m)²renders as the 3-termO(m²·n² + m⁴ + n⁴)(raise-each-term, tight) rather than the design doc's 5-term binomial — both valid degree-4 bounds. Documented in the module.Verification
cargo testgreen (5265 lib + 75 integration + 495 CLI);cargo clippy --all-targets --features ilp-highs -- -D warningsclean;cargo fmt --checkclean.grep canonical_form→ nothing.pred-sym big-ospot checks pass (O(n^2),O(1.5^num_subsets * num_subsets^2), instant degree-4). New tests: 14 growth, 24 big_o, 4 pareto (incl. #788 known-answer, OOM guard, diamond negative control).Also commits the shared batch design doc (
docs/design/symbolic-growth-domain.md).🤖 Generated with Claude Code
https://claude.ai/code/session_01EgxSbn5gwizTBkC22eyWXR