Derive reduction parameter contracts and bound ILP encodings

[isPANN]

Reduction metadata could claim exact target sizes when construction skips rows, merges coefficients, or returns an empty target. Integer-to-binary paths also advertised general ILP even though encoding requires explicit finite variable bounds. This PR derives parameter contracts from the concrete constructions and makes that encoding precondition explicit in the reduction graph.

• Support exact and upper-bound relations per target parameter, preserving independent fields when another composed prediction is unavailable.
• Add ILP<V, C, B = General> and the bounded integer variant. Supply finite intervals in incoming reductions, target binary ILP directly where applicable, and restrict integer-to-binary encoding to bounded ILP. Update solver dispatch, CLI references, and documentation.
• Add intrinsic numeric-magnitude parameters and derive encoding overhead from them. With magnitude bits h, bounded integer ILP uses at most n(h+1) binary variables; binary ILP with n variables and m constraints produces at most U = n + m(n+h) QUBO variables and U² quadratic terms.
• Propagate numeric bounds through flow, augmentation, scheduling, knapsack, circuit, and lattice reductions. Normalize irrelevant thresholds and multipliers, compress resource-scheduling horizons, and replace the exponential highly-connected-deletion encoding with a polynomial pair-variable construction.
• Correct construction-dependent counts for Coloring → QUBO, TSP, RuralPostman, matching, flow, and fault detection. Enforce the relevant capacity/lower-bound domains and preserve tiny nonzero QUBO-to-SpinGlass couplings.
• Document the parameter-schema and per-field API changes, mathematical derivations, and remaining unavailable fields.

For example, BinPacking with sizes [1,1] and capacity 1 predicts at most 34 QUBO variables along its ILP route; the actual construction has 8, and solving and recovering gives source optimum Min(2).

Validation: the complete stack passed make check and make paper before consolidation. The squash commit has exactly the same Git tree as the reviewed stack tip 1f16a331; git diff --cached --check passed. Consolidation changes commit history and PR organization only. Existing behavior tests and temporary diagnostics supplement the construction-based derivations; no additional instance fixtures were introduced for the review.

The loop/duplicate-edge parameter declarations in Coloring → ILP, MinimumCoveringByCliques → ILP, and MaximumEdgeWeightedKClique → ILP have been corrected. The previously reported SpinGlass → QUBO reversed-endpoint bug and scheduling input-domain gaps are outside these fixes. Fixed-width arithmetic and solver numerical limits still apply; not every symbolic field or composed path is predictable.

This is now the single PR for the work previously split across #1180, #1182, #1183, #1184, and #1185. Their combined changes were squash-merged into this branch as 8bdddd45; the separate PRs are superseded.

Related: #1175, #1176.

Review follow-up through 8377fe5a fixes two solver preprocessing regressions and their broader cases. Quadratic congruences and Diophantine solving always search a small positive-witness prefix before factoring. Factorization, prime-residue scans and CRT combination allocation share a work budget; exhaustion resumes complete witness enumeration instead of reporting infeasibility. EnsembleComputation rejects impossible union budgets before generating subsets, constructs an optimal chain for one distinct required set (including feasible 64-element sets), and bounds subset/partition enumeration before falling back to the existing compact ILP encoding for larger multi-set cases. Output allocation failures remain typed errors.

Regression tests cover both sides of the former quadratic cutoff, feasible and infeasible fallback searches, zero/nonunit residues, large ensemble chains, duplicate requirements, compact ILP fallback and allocation errors. Independent review found no blocking correctness issues. The follow-up also removes a needless borrow flagged by CI's Rust 1.99 Clippy.

make check, make paper, and all seven CI workflow jobs pass on 8377fe5a. The no-mistakes runner could not start its review because its configured Claude Code account is restricted; independent review and repository checks were run directly instead.

[codecov]

Codecov Report

❌ Patch coverage is 97.15272% with 132 lines in your changes missing coverage. Please review.
✅ Project coverage is 96.88%. Comparing base (9a726f1) to head (8377fe5).

Files with missing lines	Patch %	Lines
src/unit_tests/parameter_formula_validation.rs	84.47%	34 Missing ⚠️
src/solvers/customized/ensemble_computation.rs	93.87%	9 Missing ⚠️
src/rules/mixedchinesepostman_ilp.rs	61.90%	8 Missing ⚠️
src/rules/acyclicpartition_ilp.rs	97.08%	6 Missing ⚠️
src/solvers/customized/quadratic_congruences.rs	97.19%	6 Missing ⚠️
src/rules/minimumtardinesssequencing_ilp.rs	54.54%	5 Missing ⚠️
src/models/misc/resource_constrained_scheduling.rs	80.95%	4 Missing ⚠️
src/rules/flowshopscheduling_ilp.rs	60.00%	4 Missing ⚠️
src/rules/registersufficiency_ilp.rs	92.85%	4 Missing ⚠️
src/rules/bmf_ilp.rs	96.55%	3 Missing ⚠️
... and 31 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1174      +/-   ##
==========================================
+ Coverage   96.73%   96.88%   +0.15%     
==========================================
  Files        1069     1095      +26     
  Lines      138549   144504    +5955     
==========================================
+ Hits       134023   140006    +5983     
+ Misses       4526     4498      -28     

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

[GiggleLiu]

Agentic Review Report

Reviewed head f7434918 against merge-base 309ac65e. Generic PR (no linked issue): 172 files, per-field parameter relations, a registry-wide formula test, and finite variable bounds on ILP<i64> rules.

Verdict: changes requested. The infrastructure is sound, but six formulas declared exact (and one upper_bound) are false on valid instances, and the new registry-wide test cannot catch them because it checks one instance per rule.

Structural

Check	Result
Generated exports in diff	none
Merge state	conflicts with main: .claude/CLAUDE.md (content) and .claude/skills/add-rule/SKILL.md (deleted on main by #1173)
make clippy (-D warnings, all features)	pass
Targeted tests (parameter_formula_validation, symbolic_parameter_contracts, parameters::)	41 passed
New registry-wide tests runtime	2.0 s and 1.2 s (under the 5 s limit)
CI / codecov patch	green / 98.1%
Macro: mixed transform = { exact {..}, upper_bound {..}, unavailable {..} }	parses, rejects unknown relation and duplicate unavailable; tested
ParameterTransform::compose per-field relation and unavailability	correct; an unavailable or non-polynomial dependency now affects only the dependent field; tested
Scope	wider than the PR description: it also changes composition semantics, removes PathParameterError::Unavailable behaviour, changes the CLI JSON shape, and adds variable bounds to ~40 ILP<i64> rules

Quality

• every_parameter_formula_matches_a_constructed_target evaluates each rule on the first usable canonical example (or one random instance). Every finding below passes that test. Canonical examples are connected, duplicate-free, and non-degenerate, which are exactly the cases where the formulas hold.
• target_parameters() in src/unit_tests/parameter_formula_validation.rs:70-113 hardcodes rule-name branches (MinimumVertexCover → MinimumMaximalMatching, SubsetSum → IntegerKnapsack) that re-implement the target construction in the test. These check the test's own construction, not the rule.
• source_for() hardcodes random inputs by name (num_vertices, seed, k, bound) and errors on anything else, so a new generator with a different input name fails the shared test for an unrelated reason.

Feature test (pred built from the PR head)

Command	Result
pred show QUBO	lists num_quadratic_terms; per-field = / <= / unavailable rendered correctly
pred path HamiltonianPath ILP	three exact formulas using num_consecutive_positions
pred path KSatisfiability/K2 QUBO	overall num_vars =, num_quadratic_terms <= (mixed relation composes)
pred path QUBO ILP inst.json on the canonical example	measured 5 / 6 / 14, matches n + m, 3m, 7m
Counterexamples below	all reproduced

Findings

All reproduced with pred inspect + pred path <S> <T> instance.json on the PR head.

Critical — formulas declared exact that are false on valid instances

#	Location	Instance	Declared	Measured
1	src/rules/coloring_qubo.rs:185 num_quadratic_terms (new in this PR)	KColoring, 2 vertices, edges [(0,1),(0,1)], 3 colors	12	9
2	src/rules/travelingsalesman_ilp.rs:69-72 num_constraints	TSP, 2 vertices, edges [(0,1),(0,1)]	24	28
3	src/rules/ruralpostman_ilp.rs:44-47 num_vars, num_constraints	2 vertices, 1 edge, required_edges = []	6, 16	0, 0
4	src/rules/minimummaximalmatching_ilp.rs:52-55 num_constraints	3 vertices, edges [(0,1)] (isolated vertex)	4	3
5	src/rules/minimumedgecostflow_ilp.rs:57-60 num_constraints	3 vertices, arcs [(0,1)], source 0, sink 1	4	3
6	src/rules/minimumfaultdetectiontestset_ilp.rs:46-54 num_constraints and the new num_nonzeros bound	2 vertices, arcs [(0,1),(1,0)], inputs [0], outputs [0]	0, ≤ 0	1, 1

Notes:

• Implement remaining reduction rules #2 undercounts, so relabelling it upper_bound is not enough. The non-edge block uses has_edge (distinct pairs) while the McCormick block iterates all edges. Either dedupe edges in the rule or reject parallel edges in the model.
• Expand ILP solver support to more problem types #6 with inputs [0,0], outputs [1] evaluates to -1, so evaluate() returns NegativeResult. Root cause: the model does not require inputs and outputs to be distinct and disjoint.
• Roadmap #1 is introduced here. Implement remaining reduction rules #2–Expand ILP solver support to more problem types #6 predate the PR but are re-declared in its exact blocks, and the PR's claim is that every declared formula is verified.
• Suggested fixes: Roadmap #1, feat: Feature parity with ProblemReductions.jl #4, Add HiGHS ILP solver support #5 move to upper_bound; Coding Rules - For AI agents to follow #3 move to upper_bound or drop the early return at :61-67; Expand ILP solver support to more problem types #6 validate the model or bound by num_vertices.
• maximummatching_ilp.rs got exactly this treatment in this PR (isolated vertices, test parameter_predictions_account_for_isolated_vertices_and_loops); feat: Feature parity with ProblemReductions.jl #4 is the same construction.

Important

7. New variable bounds turn infeasible instances into reduction errors. src/rules/pathconstrainednetworkflow_ilp.rs:74-79 and src/rules/undirectedflowlowerbounds_ilp.rs:176-183 build IntegerVariable::new(Some(0), Some(capacity)). Neither model rejects negative capacities, so a capacity of -1 now fails with integer variable lower bound exceeds its upper bound; before the PR it produced an infeasible ILP. Under the chain contract a failed reduction is an error, not proof of infeasibility. Fix at the root: reject negative capacities in both constructors.
8. Weak verification. Add adversarial instances to the shared test for every exact field: isolated vertices, parallel edges and self-loops (SimpleGraph::new accepts both), empty required/terminal sets, and size 0/1. Findings 1–6 are the ones found by hand; the test design will miss the next one.
9. Undocumented breaking changes. CLI contract JSON moves relation from the contract level into each fields[] entry (problemreductions-cli/src/commands/graph.rs:667-677). ParameterContractError::{EmptyTransform, MissingRelation} and ParameterTransform::relation() (no argument) are removed from the public API. path_parameter_transforms no longer returns PathParameterError::Unavailable. None is in the PR description.
10. QUBO<f64> → SpinGlass behaviour change. src/rules/spinglass_qubo.rs:63-77 drops the 1e-10 threshold so that num_interactions = num_quadratic_terms is exact. Couplings that were filtered are now kept. Reasonable, but it is a semantic change and should be stated.
11. Merge conflicts with main must be resolved. The add-rule skill edit should move to how-to-code / how-to-verify, and the .claude/CLAUDE.md edits need rebasing onto the Replace board-driven pipelines with agent-invoked how-to guides #1173 rewrite.

Minor

12. SpinGlass → QUBO bound num_spins * (num_spins - 1) / 2 discards sparsity; num_quadratic_terms <= num_interactions always holds and composes better into QUBO → ILP.
13. Most new num_nonzeros bounds are the generic num_vars * num_constraints product. Valid (rows are normalized), but tight linear forms are available, e.g. maximummatching_ilp is exactly 2 * num_edges, maximalis_ilp 4 * num_edges + num_vertices, minimumdominatingset_ilp 2 * num_edges + num_vertices.
14. Fields declared upper_bound that are exact: minimumcapacitatedspanningtree_ilp (num_vars, num_constraints), lengthboundeddisjointpaths_ilp and maximumsetpacking_ilp (num_vars), hamiltoniancircuit_hamiltonianpath (num_vertices, num_consecutive_positions), paintshop_ilp (num_vars).
15. knapsack_ilp.rs:43 reads "num_items * 1".
16. Stray blank lines left where relation: was removed: src/models/decision.rs:82,127, problemreductions-cli/src/test_support.rs:402,433, subsetsum_integerknapsack.rs:35.
17. Bounded ILP<i64> rules keep their explicit x <= bound rows alongside the new variable bounds. Correct, and the exact num_constraints formulas match the code as written; removing the rows later needs the formulas updated in the same change.

Pre-existing, not introduced here

18. SpinGlass → QUBO (src/rules/spinglass_qubo.rs:145-151, :186-201) writes matrix[i][j] without ordering the endpoints, and QUBO::from_matrix reads only the upper triangle. A SpinGlass with edge (1,0), coupling 1 reduces to QUBO entries [(0,0,-2),(1,1,-2)] with no quadratic term, so the coupling is lost. Worth a separate issue.

Verified correct

Hand-counted and confirmed exact, including size-0/1 cases: hamiltonianpath_ilp (all three), quadraticassignment_ilp, qubo_ilp, qubo_casts, bmf_ilp, closeststring_ilp, consistencyofdatabasefrequencytables_ilp, exactcoverby3sets_ilp, expectedretrievalcost_ilp, feasibleregisterassignment_ilp, graphpartitioning_qubo, integerknapsack_ilp, longestcommonsubsequence_ilp, maximumcontactmapoverlap_ilp, maximumlikelihoodranking_ilp, minimummatrixcover_ilp, registersufficiency_ilp, sumofsquarespartition_ilp, threedimensionalmatching_ilp, and the four non-ILP rules. Apart from finding 7, the new with_variables bounds are implied by existing rows, cut no feasible or optimal point, add no panics or unchecked casts, and leave extract_solution unchanged.

[GiggleLiu]

Reviewed the parameter contracts, bounded ILP encodings and solver changes, including independent review of the follow-up fixes. Two preprocessing regressions were found and fixed: unbounded work before small quadratic witnesses, and exponential subset generation for ensemble instances. The fixes also cover the broader cutoff and feasible-large-set cases, with complete fallback searches and compact ILP fallback. The current-CI Clippy warning is fixed. No blocking findings remain; policy audit PASS.

Validation on 8377fe5: make check and make paper pass; all seven CI workflow jobs pass, including tests, coverage and platform builds. The no-mistakes runner was unavailable because its configured Claude account is restricted; independent review and repository checks were performed directly.