Make reduction size formulas available end-to-end (ILP → QUBO first)

[isPANN]

Summary

Path ranking and symbolic pruning both need end-to-end size predictions. Most multi-step paths don't have one: a single unavailable field in a rule's parameter contract makes every downstream formula that depends on it unavailable too.

A sweep of pred path <variant> <target> --json --limit 20 for all 256 variants to ILP, QUBO, SAT, MIS and SpinGlass (1,240 paths total) gave:

Composed end-to-end contract	Paths
every field unavailable	718 (58%)
mix of unavailable and upper bound	279
mix of unavailable and exact	164
fully upper bound	40
fully exact	39 (3%)

Where the unavailable fields come from

144 rule implementations declare 158 unavailable target fields:

Target field	Rules
ILP.num_nonzeros	111
QUBO.num_quadratic_terms	10
QUBO.num_vars	3
other	34

121 of the 158 use the same generic reason: "the exact target parameter is not represented by this reduction's symbolic transform". That reads like a placeholder rather than a real limitation. For most X → ILP rules the constraint matrix is written explicitly in the code, so num_nonzeros is countable.

8 rules are entirely transform = unavailable: circuit_sat, closestvectorproblem_qubo, decisionminimumvertexcover_hamiltoniancircuit, ilp_qubo, knapsack_qubo, ksatisfiability_simultaneousincongruences, setsplitting_betweenness, subsetsum_closestvectorproblem.

Priority: ILP → QUBO

src/rules/ilp_qubo.rs is the biggest blind spot. Nearly every path to QUBO/SpinGlass goes through it, and it is where concrete executions blow up (see #1152). Current declaration:

transform = unavailable {
    num_vars = "the slack-bit count depends on coefficient magnitudes and right-hand sides absent from the registered source parameters vector",
    num_quadratic_terms = "the nonzero products depend on generated penalty coefficients",
}

The source parameter schema (num_vars, num_constraints, num_nonzeros) has no quantity that bounds the slack bits. Options to evaluate:

1. Add an ILP parameter that captures the slack encoding (for example the total slack bit count, or the maximum bit length of constraint ranges) so num_vars becomes exact.
2. Give a sound upper_bound in terms of a new magnitude parameter.
3. For num_quadratic_terms, check whether ≤ num_vars_qubo^2 (or a tighter bound from constraint supports) is sound despite coefficient cancellation.

Tasks

• Investigate ILP → QUBO first: decide on a parameter or bound that makes num_vars and num_quadratic_terms available.
• Audit the 121 generic-reason fields, starting with ILP.num_nonzeros. For each one, provide an exact or upper_bound formula or record a specific mathematical reason why none exists.
• Review the other 8 fully unavailable rules the same way.
• Every new formula must be covered by src/unit_tests/parameter_formula_validation.rs.
• Re-run the sweep and report the new availability breakdown.

Why this comes first

This is the foundation for path selection: the size budget, symbolic pruning and Pareto ranking all rely on these predictions.