Restore reduction size predictions with source-based upper bounds

[isPANN]

Superseded by #1174. This PR’s changes were included in the combined squash commit 8bdddd45 on fix/exact-reduction-parameters. Continue review and fixes in #1174. The original description below is retained for reference.

---

Motivation and changes

This PR completes the prediction contracts of 17 reduction rules and supplies another missing field on MinimumVertexCover → LongestCommonSubsequence. It replaces unavailable declarations with exact formulas or conservative upper bounds derived from source parameters.

An unavailable intermediate parameter can prevent a whole reduction path from predicting its final size. Several declarations required an exact count even though a simple upper bound was sufficient; others had become stale as source parameters were added. For example, SubsetSum → CVP still declared its dimensions unavailable even though SubsetSum already exposed the required input bit length. Repairing these local contracts restores size predictions through circuit and lattice paths to QUBO.

Stacked on #1184 (fix/remaining-ilp-overhead). Related to #1175.

What changes for callers

Before values below are established from the comparison base's registered contracts; the new bounds are checked against constructed target instances.

Reduction	Before	After
BMF → BicliqueCover	Edge count unavailable without a nonzero-entry parameter	num_edges ≤ rows * cols; a 2×2 diagonal Boolean matrix has 2 edges and a bound of 4
CircuitSAT → Satisfiability	All target counts unavailable because exact Tseitin counts were absent	Bounds use existing named-variable, expression-node, and assignment-output counts
SubsetSum → DecisionCVP	Both dimensions unavailable	Exact dimensions 2n + h and n + h - 1, using existing source magnitude bits h
CVP → QUBO	Both target counts unavailable	With rank r, ambient dimension d, and magnitude bits h, at most V = r * (r² + d + r*h + 3) variables and V² quadratic terms
DecisionMinimumVertexCover → HamiltonianCircuit	Counts unavailable because of the decision threshold	Existing threshold normalization permits bounds n + 12m + 3 vertices and its square for edges
Knapsack → QUBO	Counts unavailable because exact slack width is piecewise	At most num_items + capacity + 1 variables and its square for quadratic terms

Additional formulas cover SAT/NAE literal counts, SAT and factoring circuit statistics, flow capacities, scheduling precedences, set normalization, bipartite graph counts, and prime-generated incongruence counts. The SAT → NAE literal formula also corrects an existing error: an empty clause produces two sentinel occurrences, so the previous claimed equality did not hold.

The only new source parameter is CVP's max_numeric_magnitude_bits: the maximum binary digit count of the absolute basis and target entries, at least one. It uses the existing magnitude helper and is computed directly from the source instance. Numerical magnitudes are necessary because dimensions alone cannot bound the encoding width. The incoming SubsetSum rule explicitly supplies a bound of two for this parameter, since its constructed coordinates have magnitude at most two.

Each rule declares its formulas locally, with only registered source parameters on the right-hand side. The paper includes derivations for the less immediate bounds.

Coverage and remaining work

Audit of all 333 registered edges:

Prediction contract	Base	This PR
Every target parameter predictable	309	326
Some target parameters predictable	17	7
No target parameters predictable	7	0

These are direct-edge counts. Some composed paths still lose all predictions, including Partition → Knapsack → QUBO.

The remaining seven missing fields are:

• MinimumVertexCover → LongestCommonSubsequence: cross_frequency_product.
• Partition → DecisionOpenShopScheduling: schedule_horizon.
• Partition → IntegralFlowWithMultipliers: max_capacity.
• Partition → Knapsack: capacity.
• Partition → ProductionPlanning: max_capacity.
• SubsetSum → IntegerKnapsack: capacity.
• ThreePartition → SequencingWithReleaseTimesAndDeadlines: time_horizon.

They need expressions with variable exponents, such as 2^h for numeric magnitudes or 2^m for cross-frequency products. Extending exact expression evaluation and safe upper-bound composition requires a separate approved change to the formula contract. This PR leaves that work pending. Concrete prediction evaluation also retains its existing numeric range checks.

Verification

• cargo test --workspace --features example-db -- --include-ignored passed.
• End-to-end tests cover feasible and infeasible inputs through SubsetSum → DecisionCVP → CVP → QUBO and Factoring → CircuitSAT → SAT → NAE-SAT → ILP<bool> → QUBO, comparing predicted sizes with actual targets and recovered results with brute force.
• Boundary tests cover empty clauses and inputs, repeated literals, sparse matrices, normalization, threshold extremes, and magnitude boundaries.
• CLI tests preserve reporting of partial and wholly unavailable composed predictions.
• Formatting, Clippy with warnings denied, graph/schema/example exports, and Typst paper compilation passed.
• Workspace coverage run passed; all 5 added executable production lines were covered. Formula correctness is checked against constructed targets separately.
• After /simplify, all 20 parameter-contract tests passed again.

Stack refresh

Merged the updated parent #1184, carrying the construction-derived bounds and validation fixes from #1174 through the stack. Preserved this PR's bounded ILP types, numeric-magnitude fields, and algorithms; no instance fixtures were added. The PR remains based on its immediate parent.

Validation of the updated head: make check passed (formatting, all-target/all-feature Clippy, and workspace tests including ignored tests). GitHub CI is restricted to PRs targeting main or develop, so these stack branches were checked locally.

The complete stack also passes make paper, including graph/schema/example exports and Typst compilation.

[codecov]

Codecov Report

❌ Patch coverage is 99.78308% with 1 line in your changes missing coverage. Please review.
⚠️ Please upload report for BASE (fix/remaining-ilp-overhead@e36915e). Learn more about missing BASE report.

Files with missing lines	Patch %	Lines
src/unit_tests/ilp_overhead.rs	98.96%	1 Missing ⚠️

Additional details and impacted files

@@                      Coverage Diff                      @@
##             fix/remaining-ilp-overhead    #1185   +/-   ##
=============================================================
  Coverage                              ?   96.80%           
=============================================================
  Files                                 ?     1073           
  Lines                                 ?   141905           
  Branches                              ?        0           
=============================================================
  Hits                                  ?   137365           
  Misses                                ?     4540           
  Partials                              ?        0           

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

[isPANN]

Merged to #1174.