Tighten reduction overhead predictions from construction-derived counts and source statistics

[isPANN]

Problem

The overhead calibration following #1174 found no formula violations on the tested inputs, but many valid bounds remain too loose to describe the targets the package actually constructs. Track systematic tightening here, deriving each declaration from the concrete reduction algorithm rather than fitting constants to corpus results.

Audited baseline

• Package/catalog inspected at de787aa7; corpus b9ae9e39.
• 309 executable, non-Turing rules; 967 target-parameter declarations: 443 exact, 518 upper bounds, 6 unavailable.
• 96,100 measured formula comparisons, 0 violations. Six unavailable fields contribute another 600 observations without predictions.
• 394 / 518 upper bounds have observed slack; 372 have median prediction/actual greater than 1. The 124 bounds equal on all tested inputs are not thereby proved exact.
• 87 declarations use dense-product bounds. Of 113 nonzero-count bounds, 106 show slack.
• 177 fields across 103 rules have identical complete source-parameter vectors but different measured target values. No expression of those existing parameters alone can be exact on both inputs.

Measurement provenance is deliberately mixed: original constructions at bf09cce890bf519e5a48f3ebd47f44cc1e769c2a, the MaxCut/MaximumMatching calibration rerun at 2ba9a0368070ff6553078a85bc8b46d785c8cfb2, and the catalog cleanup at de787aa70230c0a02159bc7aa5c3d1d3436d9b9c. Do not interpret the table as a fresh rerun of every constructor at the catalog commit.

First implementation candidates

These 16 candidate upper bounds were derived from construction blocks and checked against 100 retained measurements each (1,600 comparisons). They are proposals, not implemented fixes or corpus-based proofs. Symbols and construction arguments are defined below.

Source rule	Target field	Candidate bound	Median ratio: current → candidate
BiconnectivityAugmentation → ILP	num_nonzeros	p + n(n+1)(4m+8p)	1104.60× → 1.47×
StrongConnectivityAugmentation → ILP	num_nonzeros	2p + n(4m+8p)	94.28× → 1.12×
Factoring → ILP	num_nonzeros	8ab + 5a + 5b + 4t	101.78× → 1.05×
EulerianPath → ILP	num_nonzeros	7m + 6m(m−1)	134.40× → 3.40×
PartitionIntoTriangles → ILP	num_nonzeros	(n³+n²)/3	169.36× → 1.31×
PartitionIntoTriangles → ILP	num_vars	n²/3	3.00× → 1.00×
PartitionIntoCliques → ILP	num_nonzeros	n³	90.67× → 3.84×
PartitionIntoPathsOfLength2 → ILP	num_nonzeros	(2n²+8mn)/3	109.42× → 1.00×
PartitionIntoPathsOfLength2 → ILP	num_vars	n(n+m)/3	3.00× → 1.00×
MinimumInternalMacroDataCompression → ILP	num_vars	n + (n³−n)/6	38.84× → 6.79×
MinimumInternalMacroDataCompression → ILP	num_nonzeros	2n + (n³−n)/3	194.21× → 6.79×
NAESatisfiability → ILP	num_nonzeros	2L	2.00× → 1.00×
MonochromaticTriangle → ILP	num_nonzeros	6T + 2T(n−3)(n−4)	453.25× → 5.00×
MonochromaticTriangle → ILP	num_constraints	2T + 3T(n−3)(n−4)/4	132.31× → 5.50×
RectilinearPictureCompression → ILP	max_constraint_magnitude_bits	rows + cols + 1	85.67× → 3.00×
DecisionMinimumVertexCover → HamiltonianCircuit	num_edges	16m + 2n² + 3	56.21× → 1.40×

Construction arguments and pinned source locations

• BiconnectivityAugmentation / num_nonzeros: n vertices, m existing edges, p candidates. Budget ≤p terms. Each of n(n+1) commodities contributes ≤4m+8p: removed-edge pins and surviving-edge conservation are disjoint; candidate activation contributes two terms per direction. Trivial commodities use fewer terms. Normalization cannot increase support. Constructor.
• StrongConnectivityAugmentation / num_nonzeros: n vertices, m arcs, p candidate arcs. Candidate bounds plus budget ≤2p. For each commodity, forward/backward conservation contributes ≤4(m+p), and activation ≤4p. Dummy commodity pins ≤2(m+p). Loops can cancel terms, preserving the upper bound. Constructor.
• Factoring / num_nonzeros: a,b factor bit widths; t target bits; L=max(a+b,t). McCormick rows contribute 7ab, bit equations ab+2L−1, final carry 1, factor bounds a+b, carry bounds 2L. Total 8ab+a+b+4L; use L≤a+b+t. Constructor.
• EulerianPath / num_nonzeros: m arcs and P compatible ordered pairs of distinct arcs. Predecessor/successor rows: 2m+2P; start/end/order bounds: 3m; pair bounds and MTZ: 4P; two global sums: 2m. Total 7m+6P, with P≤m(m−1). The empty case has zero terms. Constructor.
• PartitionIntoTriangles / num_nonzeros: q=floor(n/3). Assignment and group-size rows have 2nq terms; every absent unordered vertex pair adds 2q. At most n(n−1)/2 such pairs; use q≤n/3. Existing source parameters expose n only, not the absent-pair count. Constructor.
• PartitionIntoTriangles / num_vars: Constructor allocates n floor(n/3) variables. The declared upper bound can be ceil(n²/3); exactness requires representing floor or a group-count source parameter. Constructor.
• PartitionIntoCliques / num_nonzeros: k≤n by construction validation. nk assignment terms and 2k per absent unordered pair give ≤nk+n(n−1)k=n²k≤n³. Exact count needs k and the distinct non-loop absent-pair count. Constructor.
• PartitionIntoPathsOfLength2 / num_nonzeros: q=floor(n/3), e distinct non-loop source edges, e≤m. Assignment plus group-size rows: 2nq; McCormick rows: 7eq; per-group edge sums: eq. Total 2nq+8eq. Use q≤n/3 and e≤m. Constructor.
• PartitionIntoPathsOfLength2 / num_vars: Constructor uses q(n+e) variables with q=floor(n/3) and e≤m. Upper-bound rounding is applied only to the final rational expression. Constructor.
• MinimumInternalMacroDataCompression / num_vars: At position i, there are at most i(n−i) candidate (length,reference) pairs before rejecting overlapping or unequal substrings. Sum over i is (n³−n)/6. Add n literal variables. Empty string has zero variables. Constructor.
• MinimumInternalMacroDataCompression / num_nonzeros: Each literal or valid pointer is a positive-length DAG segment and appears at its two endpoint conservation rows. Thus actual support is exactly twice actual variables. Apply the preceding source-only bound; empty string has zero support. Constructor.
• NAESatisfiability / num_nonzeros: L total literal occurrences. Each clause emits two rows, one term per literal before normalization. Duplicate literals merge and opposite signs cancel; both can only reduce support. This proposal may be looser than the current dense cap on inputs dominated by repeated literals; retain the caveat and compare both bounds. Constructor.
• MonochromaticTriangle / num_nonzeros: T triangles, K five-cliques, H triangles contained in at least one five-clique. Two rows per triangle give 6T terms. Opposite-edge equalities give 2(10K−H); degree equalities give 20K. Total 6T+40K−2H. Since 10K≤T(n−3)(n−4)/2, drop −2H. For n<3, T=0; for n=3 or 4 the product vanishes. Negative coefficients may weaken composed bounds. Constructor.
• MonochromaticTriangle / num_constraints: Exact row count is 2T+(10K−H)+5K = 2T+15K−H. Use the five-clique incidence bound and discard −H. Counts refer to the actual strengthening rows, not merely the basic triangle-coloring formulation. Constructor.
• RectilinearPictureCompression / max_constraint_magnitude_bits: All row coefficients are 1; binary endpoints are 0/1; budget RHS is clamped into [−1,R], with R maximal rectangles. R≤[r(r+1)/2][c(c+1)/2]≤2^(r+c) for positive dimensions; hence bits≤r+c+1. Empty dimensions have R=0 and magnitude bits 1. This improves magnitude-to-bit overestimation without adding log support. Constructor.
• DecisionMinimumVertexCover / num_edges: n source vertices, m raw edges. After normalization and forced-cover removal, m′≤m. Each edge gadget inserts 14 edges; incident-edge chains contribute at most 2m′; selector links at most 2n². Fixed YES/NO outputs have at most three edges. A set deduplicates edges, which can only reduce the bound. Constructor.

Review caveats: repeated literals can make the NAE 2L bound looser than the existing dense cap outside this corpus; compare both derivations before replacing it. Subtractive terms in the MonochromaticTriangle candidates need domain and composition checks. Rational counts need the real evaluator's rounding semantics. None of these caveats should be hidden by testing only the observed input shapes.

Work plan and acceptance criteria

• Derive tighter counts for the 16 candidates, covering every accepted source input, early returns, duplicate/zero terms, merged coefficients and target normalization. Use exact only when equality is proved; otherwise retain a sound upper_bound.
• Implement the justified candidates and continue the remaining loose-bound queue, prioritizing ILP nonzeros, variables and encoding bit lengths. Report absolute excess alongside ratios.
• For demonstrated information gaps, identify the smallest useful source statistics. Start with cheap/cached properties; account for the cost of computing any new statistic and update incoming parameter contracts. Do not run a solver just to predict an overhead.
• Trace all six unavailable fields to their algorithms and source schemas; supply a representable count/bound or a precise reason for remaining unavailable. Coordinate availability work with Make reduction size formulas available end-to-end (ILP → QUBO first) #1175.
• Write meaningful failing behavior checks before each implementation change; independently derive expected counts. Reuse existing test inputs and keep the corpus at its current size.
• Rerun affected corpus measurements, preserving unaffected records; record before/after median, P95, maximum, zero cases, equality rate and absolute excess. Require zero underestimates and exact-declaration violations, with universal derivations in the implementation review.
• Check concrete intermediate targets against composed predictions for affected chains. Run repository checks and refresh the dashboard.

Scope

This issue concerns the size of the implemented target construction, not an abstract best-known algorithm or empirical curve fitting. Source changes should improve declarations without silently changing reduction semantics. Keep symbolic-engine and parameter-comparison changes in their separate worktree/issues; path ranking is not an acceptance criterion here. The inspected path search uses hop count, so tighter formulas do not by themselves demonstrate faster solving or different selected paths.

The full local evidence bundle is the 2026-09-29-bf09cce8 run: accuracy-report/inventory.{json,csv}, proposals.json, proposal-cases.json, source-information-gaps.json, and provenance.json. These generated files are not committed to the package; the findings and candidate derivations needed to start work are included above.

Related: #1174 (current contracts), #1175 (formula availability), #1179 and #1187 (separate path-selection work).

Reduction-correctness timeouts are tracked separately in #1189.

[isPANN]

Fixed in #1190.