Make derivable reduction parameters exact

.claude/CLAUDE.md

@@ -351,3 +351,4 @@ Parameter expressions describe how target problem parameters relate to source pr
 3. Watch for common errors: universe elements mismatch (edge indices vs vertex indices), worst-case edge counts in intersection graphs (quadratic, not linear), constant factors in circuit constructions
 4. Test with concrete small instances: construct a source problem, run the reduction, and compare target parameters against the formula
 5. Ensure there is only one primitive reduction registration for each exact source/target variant pair; wrap shared helpers instead of registering duplicate endpoints
+6. Every new rule's `exact` and `upper_bound` fields must be covered by `src/unit_tests/parameter_formula_validation.rs`: evaluate each formula on a valid source instance and compare it with measured target parameters (equal for `exact`, predicted ≥ measured for `upper_bound`). Provide a canonical example or registered generator so the shared test can exercise the rule; add targeted boundary cases when needed.

.claude/skills/add-rule/SKILL.md

@@ -168,6 +168,8 @@ Add to `src/rules/mod.rs`:
 
 Create `src/unit_tests/rules/<source>_<target>.rs`:
 
+Follow the [reduction parameter testing requirement](../../CLAUDE.md#reduction-parameter-relation): the shared test must cover every declared `exact` or `upper_bound` field using a valid source instance.
+
 **Required: closed-loop test** (`test_<source>_to_<target>_closed_loop`):
 ```rust
 // 1. Create source problem instance

src/lib.rs

@@ -135,6 +135,9 @@ pub use problemreductions_macros::{
 // Re-export inventory so `declare_variants!` can use `$crate::inventory::submit!`
 pub use inventory;
 
+#[cfg(all(test, feature = "example-db"))]
+#[path = "unit_tests/parameter_formula_validation.rs"]
+mod parameter_formula_validation;
 #[cfg(all(test, feature = "example-db"))]
 #[path = "unit_tests/symbolic_parameter_contracts.rs"]
 mod symbolic_parameter_contracts;

src/models/algebraic/qubo.rs

@@ -258,6 +258,11 @@ impl<W: Clone> QUBO<W> {
         self.num_vars
     }
 
+    /// Number of nonzero off-diagonal coefficients.
+    pub fn num_quadratic_terms(&self) -> usize {
+        self.entries.iter().filter(|(i, j, _)| i != j).count()
+    }
+
     /// Nonzero upper-triangular coefficients `(i, j, Q[i][j])`, sorted by `(i, j)`.
     pub fn entries(&self) -> &[(usize, usize, W)] {
         &self.entries
@@ -293,7 +298,10 @@ where
     type Solution = Vec<bool>;
     type Value = Min<W::Sum>;
 
-    crate::problem_parameters![("num_vars", num_vars),];
+    crate::problem_parameters![
+        ("num_vars", num_vars),
+        ("num_quadratic_terms", num_quadratic_terms),
+    ];
 
     fn evaluate(
         &self,

src/models/graph/hamiltonian_path.rs

@@ -89,6 +89,11 @@ impl<G: Graph> HamiltonianPath<G> {
         self.graph.num_edges()
     }
 
+    /// Number of consecutive position pairs in a Hamiltonian path.
+    pub fn num_consecutive_positions(&self) -> usize {
+        self.num_vertices().saturating_sub(1)
+    }
+
     /// Check if a configuration is a valid Hamiltonian path.
     pub fn is_valid_solution(&self, config: &[usize]) -> bool {
         is_valid_hamiltonian_path(&self.graph, config)
@@ -103,7 +108,11 @@ where
     type Solution = Vec<usize>;
     type Value = crate::types::Or;
 
-    crate::problem_parameters![("num_edges", num_edges), ("num_vertices", num_vertices),];
+    crate::problem_parameters![
+        ("num_edges", num_edges),
+        ("num_vertices", num_vertices),
+        ("num_consecutive_positions", num_consecutive_positions),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![G]

src/rules/bmf_bicliquecover.rs

@@ -95,12 +95,12 @@ impl ReductionResult for ReductionBMFToBicliqueCover {
 #[reduction(
     transform = exact {
         num_vertices = "rows + cols",
-        num_edges = "rows * cols",
+        left_size = "rows",
+        right_size = "cols",
         rank = "rank",
     },
     unavailable = {
-        left_size = "the exact target parameter is not represented by this reduction's symbolic transform",
-        right_size = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_edges = "the number of true matrix entries is not a registered BMF parameter",
     }
 )]
 impl ReduceTo<BicliqueCover> for BMF {

src/rules/bmf_ilp.rs

@@ -54,9 +54,7 @@ impl ReductionResult for ReductionBMFToILP {
     transform = exact {
         num_vars = "rows * rank + rank * cols + rows * rank * cols + rows * cols",
         num_constraints = "3 * rows * rank * cols + rank * rows * cols + rows * cols + rows * cols",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "10 * rows * rank * cols + 2 * rows * cols",
     }
 )]
 impl ReduceTo<ILP<bool>> for BMF {

src/rules/closeststring_ilp.rs

@@ -82,9 +82,7 @@ impl ReductionResult for ReductionClosestStringToILP {
     transform = exact {
         num_vars = "alphabet_size * string_length + 1",
         num_constraints = "string_length + num_strings",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "alphabet_size * string_length + num_strings * (string_length + 1)",
     }
 )]
 impl ReduceTo<ILP<i64>> for ClosestString {

src/rules/closestvectorproblem_qubo.rs

@@ -233,6 +233,7 @@ fn dot(left: &[i64], right: &[i64], operation: &str) -> Result<i64, crate::rules
 
 #[reduction(transform = unavailable {
     num_vars = "the exact encoding size depends on the concrete basis and target values",
+    num_quadratic_terms = "the number of nonzero products depends on the concrete basis coefficients",
 })]
 impl ReduceTo<QUBO<i64>> for ClosestVectorProblem {
     type Result = ReductionCVPToQUBO;

src/rules/coloring_qubo.rs

@@ -182,6 +182,7 @@ fn reduce_kcoloring_to_qubo<K: KValue>(
 #[reduction(
     transform = exact {
         num_vars = "num_vertices * num_colors",
+        num_quadratic_terms = "num_vertices * num_colors * (num_colors - 1) / 2 + num_edges * num_colors",
     }
 )]
 impl ReduceTo<Decision<QUBO<i64>>> for KColoring<KN, SimpleGraph> {

src/rules/consistencyofdatabasefrequencytables_ilp.rs

@@ -139,9 +139,7 @@ impl crate::rules::AggregateReductionResult for ReductionCDFTToILP {}
     transform = exact {
         num_vars = "num_objects * total_domain_size + num_objects * num_frequency_cells",
         num_constraints = "num_objects * num_attributes + num_known_values + num_frequency_cells + 3 * num_objects * num_frequency_cells",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "num_objects * total_domain_size + num_known_values + 8 * num_objects * num_frequency_cells",
     }
 )]
 impl ReduceTo<ILP<bool>> for ConsistencyOfDatabaseFrequencyTables {

src/rules/exactcoverby3sets_ilp.rs

@@ -43,9 +43,7 @@ impl crate::rules::AggregateReductionResult for ReductionX3CToILP {}
     transform = exact {
         num_vars = "num_subsets",
         num_constraints = "universe_size + 1",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "4 * num_subsets",
     }
 )]
 impl ReduceTo<ILP<bool>> for ExactCoverBy3Sets {

src/rules/expectedretrievalcost_ilp.rs

@@ -80,9 +80,7 @@ impl ReductionResult for ReductionERCToILP {
     transform = exact {
         num_vars = "num_records * num_sectors + num_records^2 * num_sectors^2",
         num_constraints = "num_records + 3 * num_records^2 * num_sectors^2",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "7 * num_records^2 * num_sectors^2",
     }
 )]
 impl ReduceTo<ILP<bool, f64>> for ExpectedRetrievalCost {

src/rules/feasibleregisterassignment_ilp.rs

@@ -51,9 +51,7 @@ impl crate::rules::AggregateReductionResult for ReductionFeasibleRegisterAssignm
     transform = exact {
         num_vars = "2 * num_vertices + num_vertices * (num_vertices - 1) / 2",
         num_constraints = "3 * num_vertices * (num_vertices - 1) / 2 + 3 * num_vertices + 2 * num_arcs + 2 * num_same_register_pairs",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "4 * num_vertices + 4 * num_arcs + 7 * num_vertices * (num_vertices - 1) / 2 + 6 * num_same_register_pairs",
     }
 )]
 impl ReduceTo<ILP<i64>> for FeasibleRegisterAssignment {

src/rules/graphpartitioning_qubo.rs

@@ -36,6 +36,7 @@ impl ReductionResult for ReductionGraphPartitioningToQUBO {
 
 #[reduction(transform = exact {
     num_vars = "num_vertices",
+    num_quadratic_terms = "num_vertices * (num_vertices - 1) / 2",
 })]
 impl ReduceTo<QUBO<i64>> for GraphPartitioning<SimpleGraph> {
     type Result = ReductionGraphPartitioningToQUBO;

src/rules/hamiltoniancircuit_hamiltonianpath.rs

@@ -90,6 +90,7 @@ impl crate::rules::AggregateReductionResult for ReductionHamiltonianCircuitToHam
     transform = upper_bound {
         num_vertices = "num_vertices + 3",
         num_edges = "num_edges + num_vertices + 1",
+        num_consecutive_positions = "num_vertices + 2",
     }
 )]
 impl ReduceTo<HamiltonianPath<SimpleGraph>> for HamiltonianCircuit<SimpleGraph> {

src/rules/hamiltonianpath_ilp.rs

@@ -54,12 +54,10 @@ impl ReductionResult for ReductionHamiltonianPathToILP {
 impl crate::rules::AggregateReductionResult for ReductionHamiltonianPathToILP {}
 
 #[reduction(
-    transform = upper_bound {
-        num_vars = "num_vertices^2 + 2 * num_edges * num_vertices",
-        num_constraints = "2 * num_vertices + 6 * num_edges * num_vertices + num_vertices",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+    transform = exact {
+        num_vars = "num_vertices^2 + 2 * num_edges * num_consecutive_positions",
+        num_constraints = "2 * num_vertices + 6 * num_edges * num_consecutive_positions + num_consecutive_positions",
+        num_nonzeros = "2 * num_vertices^2 + 16 * num_edges * num_consecutive_positions",
     }
 )]
 impl ReduceTo<ILP<bool>> for HamiltonianPath<SimpleGraph> {
@@ -70,7 +68,7 @@ impl ReduceTo<ILP<bool>> for HamiltonianPath<SimpleGraph> {
         let graph = self.graph();
         let edges = graph.edges();
         let m = edges.len();
-        let n_pos = if n == 0 { 0 } else { n - 1 }; // number of consecutive-position pairs
+        let n_pos = self.num_consecutive_positions();
 
         let num_x = n * n;
         let num_z = 2 * m * n_pos;

src/rules/ilp_i64_ilp_bool.rs

@@ -111,9 +111,11 @@ impl ReductionResult for ReductionIntILPToBinaryILP {
 }
 
 #[reduction(
-    transform = unavailable {
+    transform = exact {
+        num_constraints = "num_constraints",
+    },
+    unavailable = {
         num_vars = "the binary width depends on concrete variable bounds, not registered problem parameters",
-        num_constraints = "the exact row count is preserved but the target parameters model is unavailable until all ILP overhead declarations are migrated",
         num_nonzeros = "binary expansion depends on concrete variable bounds and row sparsity",
     },
 )]

src/rules/ilp_qubo.rs

@@ -81,6 +81,7 @@ impl crate::rules::AggregateReductionResult for ReductionILPToQUBO {
 #[reduction(
     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",
     }
 )]
 impl ReduceTo<QUBO<i64>> for ILP<bool> {

src/rules/integerknapsack_ilp.rs

@@ -36,9 +36,7 @@ impl ReductionResult for ReductionIntegerKnapsackToILP {
     transform = exact {
         num_vars = "num_items",
         num_constraints = "num_items + 1",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "2 * num_items",
     }
 )]
 impl ReduceTo<ILP<i64>> for IntegerKnapsack {

src/rules/knapsack_qubo.rs

@@ -46,6 +46,7 @@ impl ReductionResult for ReductionKnapsackToQUBO {
 
 #[reduction(transform = unavailable {
     num_vars = "the exact piecewise slack-bit count is not representable in the parameter-expression language",
+    num_quadratic_terms = "the nonzero products depend on item sizes and values",
 })]
 impl ReduceTo<QUBO<i64>> for Knapsack {
     type Result = ReductionKnapsackToQUBO;

src/rules/ksatisfiability_qubo.rs

@@ -332,6 +332,9 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToQUBO {}
 #[reduction(
     transform = exact {
         num_vars = "num_vars",
+    },
+    unavailable = {
+        num_quadratic_terms = "clause literals can overlap and cancel in the QUBO coefficients",
     }
 )]
 impl ReduceTo<Decision<QUBO<i64>>> for KSatisfiability<K2> {
@@ -365,6 +368,9 @@ impl ReduceTo<Decision<QUBO<i64>>> for KSatisfiability<K2> {
 #[reduction(
     transform = exact {
         num_vars = "num_vars + num_clauses",
+    },
+    unavailable = {
+        num_quadratic_terms = "clause literals can overlap and cancel in the QUBO coefficients",
     }
 )]
 impl ReduceTo<Decision<QUBO<i64>>> for KSatisfiability<K3> {

src/rules/longestcommonsubsequence_ilp.rs

@@ -53,9 +53,7 @@ impl ReductionResult for ReductionLCSToILP {
     transform = exact {
         num_vars = "max_length * (alphabet_size + 1) + max_length * total_length",
         num_constraints = "max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "max_length * (alphabet_size + 1 + num_strings + 3 * total_length) + 2 * num_transitions * (1 + sum_triangular_lengths)",
     }
 )]
 impl ReduceTo<ILP<bool>> for LongestCommonSubsequence {

src/rules/maximumcontactmapoverlap_ilp.rs

@@ -73,9 +73,7 @@ impl ReductionResult for ReductionCMOToILP {
     transform = exact {
         num_vars = "num_vertices_1 * num_vertices_2 + num_contacts_1 * num_contacts_2",
         num_constraints = "num_vertices_1 + num_vertices_2 + num_vertices_1 * (num_vertices_1 - 1) / 2 * num_vertices_2 * (num_vertices_2 + 1) / 2 + 2 * num_contacts_1 * num_contacts_2",
-    },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_nonzeros = "2 * num_vertices_1 * num_vertices_2 + num_vertices_1 * (num_vertices_1 - 1) * num_vertices_2 * (num_vertices_2 + 1) / 2 + 4 * num_contacts_1 * num_contacts_2",
     }
 )]
 impl ReduceTo<ILP<bool>> for MaximumContactMapOverlap {

src/rules/maximumlikelihoodranking_ilp.rs

@@ -76,10 +76,8 @@ impl ReductionResult for ReductionMaximumLikelihoodRankingToILP {
     transform = exact {
         num_vars = "num_items * (num_items - 1) / 2",
         num_constraints = "num_items * (num_items - 1) * (num_items - 2) / 3",
+        num_nonzeros = "num_items * (num_items - 1) * (num_items - 2)",
     },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
 )]
 impl ReduceTo<ILP<bool>> for MaximumLikelihoodRanking {
     type Result = ReductionMaximumLikelihoodRankingToILP;

src/rules/maximumsetpacking_qubo.rs

@@ -43,6 +43,9 @@ impl ReductionResult for ReductionSPToQUBO {
 #[reduction(
     transform = exact {
         num_vars = "num_sets",
+    },
+    unavailable = {
+        num_quadratic_terms = "the number of overlapping set pairs is not a registered source parameter",
     }
 )]
 impl ReduceTo<QUBO<f64>> for MaximumSetPacking<f64> {

src/rules/minimumdiscreteplanarinversekinematics_qubo.rs

@@ -80,6 +80,8 @@ impl ReductionResult for ReductionMinimumDiscretePlanarInverseKinematicsToQUBO {
 
 #[reduction(transform = exact {
     num_vars = "num_orientation_samples",
+}, unavailable = {
+    num_quadratic_terms = "the nonzero products depend on the sampled geometry",
 })]
 impl ReduceTo<QUBO<f64>> for MinimumDiscretePlanarInverseKinematics {
     type Result = ReductionMinimumDiscretePlanarInverseKinematicsToQUBO;

src/rules/minimummatrixcover_ilp.rs

@@ -56,10 +56,8 @@ fn y_index(n: usize, i: usize, j: usize) -> usize {
     transform = exact {
         num_vars = "num_rows + num_rows * (num_rows - 1) / 2",
         num_constraints = "3 * num_rows * (num_rows - 1) / 2",
+        num_nonzeros = "7 * num_rows * (num_rows - 1) / 2",
     },
-    unavailable = {
-        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
-    }
 )]
 impl ReduceTo<ILP<bool>> for MinimumMatrixCover {
     type Result = ReductionMinimumMatrixCoverToILP;

src/rules/minimummultiwaycut_qubo.rs

@@ -86,6 +86,8 @@ impl ReductionResult for ReductionMinimumMultiwayCutToQUBO {
 
 #[reduction(transform = exact {
     num_vars = "num_terminals * num_vertices",
+}, unavailable = {
+    num_quadratic_terms = "the nonzero products depend on edge weights and terminal placement",
 })]
 impl ReduceTo<QUBO<i64>> for MinimumMultiwayCut<SimpleGraph, i64> {
     type Result = ReductionMinimumMultiwayCutToQUBO;

src/rules/minimumvertexcover_longestcommonsubsequence.rs

@@ -44,11 +44,11 @@ impl ReductionResult for ReductionVCToLCS {
         num_strings = "num_edges + 1",
         max_length = "num_vertices",
         total_length = "num_vertices + 2 * num_edges * num_vertices - 2 * num_edges",
+        sum_triangular_lengths = "num_vertices * (num_vertices + 1) / 2 + num_edges * (2 * num_vertices - 2) * (2 * num_vertices - 1) / 2",
     },
     unavailable = {
         cross_frequency_product = "the exact target parameter is not represented by this reduction's symbolic transform",
         num_transitions = "the exact target parameter is not represented by this reduction's symbolic transform",
-        sum_triangular_lengths = "the exact target parameter is not represented by this reduction's symbolic transform",
     }
 )]
 impl ReduceTo<LongestCommonSubsequence> for MinimumVertexCover<SimpleGraph, One> {

src/rules/optimallineararrangement_sequencingtominimizeweightedcompletiontime.rs

@@ -57,9 +57,7 @@ impl ReductionResult for ReductionOLAToSequencingToMinimizeWeightedCompletionTim
 #[reduction(
     transform = exact {
         num_tasks = "num_vertices + num_edges",
-    },
-    unavailable = {
-        num_precedences = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_precedences = "2 * num_edges",
     }
 )]
 impl ReduceTo<SequencingToMinimizeWeightedCompletionTime>

src/rules/paintshop_qubo.rs

@@ -40,6 +40,8 @@ impl ReductionResult for ReductionPaintShopToQUBO {
 
 #[reduction(transform = exact {
     num_vars = "num_cars",
+}, unavailable = {
+    num_quadratic_terms = "adjacency contributions can cancel between repeated car pairs",
 })]
 impl ReduceTo<QUBO<i64>> for PaintShop {
     type Result = ReductionPaintShopToQUBO;

src/rules/partition_multiprocessorscheduling.rs

@@ -56,9 +56,7 @@ impl crate::rules::AggregateReductionResult for ReductionPartitionToMPS {}
 #[reduction(
     transform = exact {
         num_tasks = "num_elements",
-    },
-    unavailable = {
-        num_processors = "the exact target parameter is not represented by this reduction's symbolic transform",
+        num_processors = "2",
     }
 )]
 impl ReduceTo<MultiprocessorScheduling> for Partition {