Background
Each registered reduction declares symbolic output-size formulas through #[reduction(overhead = { ... })]. The Pareto path search introduced by #1093 and PR #1083 correctly compares completed paths rather than greedily choosing the smallest intermediate step, but the size data it compares still has an ambiguous contract: documentation calls it asymptotic scaling, while ReductionOverhead::evaluate_output_size and the generated overhead_eval_fn evaluate it as a concrete size using f64, round(), missing-variable defaults, and unchecked casts.
That ambiguity loses useful information before terminal comparison. For example, MaximumIndependentSet → MaximumClique has the exact edge-count transfer n(n-1)/2 - m; asymptotic widening turns the subtraction into addition and cannot represent that denser inputs produce smaller complement graphs. Conversely, some quantities that affect solver difficulty, such as exact treewidth, are not cheap structural size fields and must not be required by this system.
The current graph is small enough for terminal-only exact search: 239 variant nodes, 290 edges, maximum SCC size 5, and representative exact CLI queries expand fewer than 350 states locally. This issue therefore prioritizes trustworthy terminal size data over intermediate pruning.
Objective
Give reduction overhead a testable contract for cheap structural target sizes:
- A field advertised as exact must evaluate to the constructed target's corresponding registered size field.
- Exact evaluation must use checked integer semantics and expose missing inputs, non-integral results, negative results, division errors, and overflow instead of rounding, saturating, or substituting zero.
- Big-O growth is a derived, instance-free view of an exact formula; it is not the source of concrete size predictions.
- If a target size cannot be predicted from cheap source statistics, exact symbolic propagation must report that field/edge as unavailable. It must not invent a value or require solver-hard parameters such as exact treewidth.
- Path search must continue to retain distinct intermediate paths and apply Pareto dominance only to completed paths. Equal or locally smaller intermediate size vectors are not sufficient for pruning.
The result should make complete-route terminal structural overhead trustworthy. It does not claim to predict solver runtime or intrinsic instance hardness.
Interface (Input → Output)
Single reduction
- In: an exact registered reduction edge and its source
ProblemSize.
- Out: the exact target
ProblemSize, or an explicit error naming the edge and unavailable/invalid field.
Complete path
- In: a source
ProblemSize and one explicit elementary ReductionPath.
- Out: the final target
ProblemSize, obtained by applying exact transfers step by step. Intermediate sizes are not accumulated into a scalar cost and are not used to discard other prefixes.
Instance-free display
- In: the exact symbolic transfer expressions for a complete path.
- Out: the existing conservative Big-O view, clearly labeled asymptotic. Failure to derive Big-O must not invalidate exact concrete evaluation.
Plan
-
Audit the current contract
- Inventory registered overhead fields and identify declarations that are exact counts, conservative bounds, or currently only asymptotic estimates.
- Record every declaration that depends on an input absent from the source size fields or produces a target field that cannot be validated against the target registry.
-
Replace floating-point concrete evaluation
- Remove
f64 → round() → usize from concrete overhead evaluation in src/rules/registry.rs and the generated evaluator in problemreductions-macros.
- Evaluate exact structural formulas with checked integer arithmetic.
- Fail explicitly on a missing variable, negative/non-integral value, zero division, or overflow.
- Keep floating-point/exponential operations only in the complexity/growth path where they are semantically appropriate.
-
Add a constructed-target oracle
- For every canonical executable rule example, load the source, execute the registered reduction, measure the actual target through its registered size getters, and compare it field-by-field with the declared exact transfer.
- Assert that the number of checked examples equals the number of eligible canonical executable rule examples so silent coverage loss cannot make the audit pass.
-
Migrate cheap structural declarations
- Fix formulas or add cheap source getters when the required statistic is already available or naturally computed by the reduction construction.
- Mark exact propagation unavailable when obtaining the required statistic would be comparable to solving the instance or would require new solver-hard infrastructure.
- If the audit requires changes to more than 20 reduction files, split the formula migrations into follow-up issues/PRs; do not exceed the repository PR scope limit.
-
Propagate exact sizes along explicit paths
- Apply edge transfers sequentially rather than expanding a large composed polynomial for concrete evaluation.
- Compare only final target vectors.
- Preserve the existing rule that exact search performs no intermediate dominance or equal-size coalescing.
-
Clarify user-facing semantics
- Document the difference between exact structural size, asymptotic Big-O, and constructed/measured size.
- Make unavailable exact propagation visible in library, CLI, and MCP results rather than silently falling back to asymptotic evaluation.
Technical recommendations
These are non-binding implementation suggestions:
- Keep
Growth as the conservative instance-free display/comparison domain; do not extend it with special cases to recover information discarded by an ambiguous concrete-size contract.
- Reuse canonical rule examples as the independent target oracle instead of adding snapshot/golden fixtures.
- Prefer direct source getters for cheap construction statistics already present in a reduction. Do not introduce a generic feature registry, solver-cost adapter, or tree-decomposition certificate system.
- Preserve full expressions until Big-O display is explicitly requested. For concrete path evaluation, propagate
ProblemSize edge by edge.
Verification
Add a focused behavioural suite runnable with:
cargo test reduction_overhead_contract --features example-db
It must exercise all of the following in one suite:
- Known-answer exact transfer: the canonical five-vertex, four-edge
MaximumIndependentSet → MaximumClique example predicts num_vertices = 5 and num_edges = 6; executing the reduction and measuring the target produces the same (5, 6) vector.
- Complete-path propagation: a fixed multi-step canonical route propagates source sizes edge by edge and matches the actually constructed terminal target field-by-field.
- Repository-wide oracle: every eligible canonical executable rule example is checked, the checked count equals the eligible example count, and the mismatch count is zero.
- No local-optimum pruning: a synthetic two-route graph contains a locally smaller intermediate graph whose complement is larger at the terminal. Exact search returns the terminal Pareto result determined after the complement step, not the locally smallest prefix.
- Negative controls: exact evaluation rejects an expression with a missing variable, a negative result, a non-integral result, division by zero, and arithmetic overflow. None may become zero, a rounded integer, or
usize::MAX.
The complement case fails if exact expressions are prematurely widened to Big-O. The malformed-expression cases fail if the existing permissive f64/rounding behavior remains. The multi-route case fails if intermediate greedy or dominance pruning is introduced.
After the focused suite passes, run:
make check
cargo test --manifest-path problemreductions-cli/Cargo.toml
Dependencies
Out of scope
- Exact or approximate treewidth, tree decompositions, gadget structure certificates, or other solver-hard instance features.
- Predicting solver runtime, memory, solution quality, or hardware embedding quality.
- Learned cost models, profiling systems, or generic feature registries.
- Greedy edge selection, accumulated intermediate cost, or intermediate Pareto pruning.
- Preserving permissive floating-point concrete-size evaluation for compatibility.
Background
Each registered reduction declares symbolic output-size formulas through
#[reduction(overhead = { ... })]. The Pareto path search introduced by #1093 and PR #1083 correctly compares completed paths rather than greedily choosing the smallest intermediate step, but the size data it compares still has an ambiguous contract: documentation calls it asymptotic scaling, whileReductionOverhead::evaluate_output_sizeand the generatedoverhead_eval_fnevaluate it as a concrete size usingf64,round(), missing-variable defaults, and unchecked casts.That ambiguity loses useful information before terminal comparison. For example,
MaximumIndependentSet → MaximumCliquehas the exact edge-count transfern(n-1)/2 - m; asymptotic widening turns the subtraction into addition and cannot represent that denser inputs produce smaller complement graphs. Conversely, some quantities that affect solver difficulty, such as exact treewidth, are not cheap structural size fields and must not be required by this system.The current graph is small enough for terminal-only exact search: 239 variant nodes, 290 edges, maximum SCC size 5, and representative exact CLI queries expand fewer than 350 states locally. This issue therefore prioritizes trustworthy terminal size data over intermediate pruning.
Objective
Give reduction overhead a testable contract for cheap structural target sizes:
The result should make complete-route terminal structural overhead trustworthy. It does not claim to predict solver runtime or intrinsic instance hardness.
Interface (Input → Output)
Single reduction
ProblemSize.ProblemSize, or an explicit error naming the edge and unavailable/invalid field.Complete path
ProblemSizeand one explicit elementaryReductionPath.ProblemSize, obtained by applying exact transfers step by step. Intermediate sizes are not accumulated into a scalar cost and are not used to discard other prefixes.Instance-free display
Plan
Audit the current contract
Replace floating-point concrete evaluation
f64 → round() → usizefrom concrete overhead evaluation insrc/rules/registry.rsand the generated evaluator inproblemreductions-macros.Add a constructed-target oracle
Migrate cheap structural declarations
Propagate exact sizes along explicit paths
Clarify user-facing semantics
Technical recommendations
These are non-binding implementation suggestions:
Growthas the conservative instance-free display/comparison domain; do not extend it with special cases to recover information discarded by an ambiguous concrete-size contract.ProblemSizeedge by edge.Verification
Add a focused behavioural suite runnable with:
cargo test reduction_overhead_contract --features example-dbIt must exercise all of the following in one suite:
MaximumIndependentSet → MaximumCliqueexample predictsnum_vertices = 5andnum_edges = 6; executing the reduction and measuring the target produces the same(5, 6)vector.usize::MAX.The complement case fails if exact expressions are prematurely widened to Big-O. The malformed-expression cases fail if the existing permissive
f64/rounding behavior remains. The multi-route case fails if intermediate greedy or dominance pruning is introduced.After the focused suite passes, run:
make check cargo test --manifest-path problemreductions-cli/Cargo.tomlDependencies
Out of scope