Tighten sparse, geometric and cached construction overhead formulas

problemreductions-cli/tests/cli_tests.rs

@@ -5534,7 +5534,7 @@ fn test_path_set_has_explicit_parameter_information() {
 }
 
 #[test]
-fn test_path_overall_unavailable_is_reported_per_field_without_internal_modes() {
+fn test_path_reports_numeric_horizon_without_internal_modes() {
     let output = pred()
         .args([
             "path",
@@ -5554,8 +5554,8 @@ fn test_path_overall_unavailable_is_reported_per_field_without_internal_modes()
         .iter()
         .find(|field| field["field"] == "time_horizon")
         .unwrap();
-    assert_eq!(horizon["relation"], "unavailable");
-    assert!(horizon["reason"].is_string());
+    assert_eq!(horizon["relation"], "exact");
+    assert!(horizon["formula"].is_string());
     let task_count = fields
         .iter()
         .find(|field| field["field"] == "num_tasks")
@@ -5613,7 +5613,14 @@ fn test_path_preserves_exact_variables_and_bounded_quadratic_terms() {
 #[test]
 fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
     let output = pred()
-        .args(["path", "Partition", "Knapsack", "--limit", "1", "--json"])
+        .args([
+            "path",
+            "MinimumVertexCover/SimpleGraph/One",
+            "LongestCommonSubsequence",
+            "--limit",
+            "1",
+            "--json",
+        ])
         .output()
         .unwrap();
     assert!(output.status.success());
@@ -5630,8 +5637,8 @@ fn test_path_overall_preserves_unavailable_fields_alongside_exact_fields() {
             )
         })
         .collect::<std::collections::BTreeMap<_, _>>();
-    assert_eq!(relations["num_items"], "exact");
-    assert_eq!(relations["capacity"], "unavailable");
+    assert_eq!(relations["alphabet_size"], "exact");
+    assert_eq!(relations["cross_frequency_product"], "unavailable");
     let unavailable = fields
         .iter()
         .find(|field| field["relation"] == "unavailable")

src/models/algebraic/closest_vector_problem.rs

@@ -48,6 +48,8 @@ pub struct ClosestVectorProblem {
     basis: Vec<Vec<i64>>,
     /// Target vector in the ambient space.
     target: Vec<i64>,
+    #[serde(skip)]
+    coefficient_box_bits: u64,
 }
 
 impl ClosestVectorProblem {
@@ -68,12 +70,53 @@ impl ClosestVectorProblem {
                 basis.len()
             )));
         }
-        if independent_rows(&basis, ambient_dimension).is_none() {
-            return Err(ConstructionError::Conversion(
+        let (_, determinant) = independent_rows(&basis, ambient_dimension).ok_or_else(|| {
+            ConstructionError::Conversion(
                 "closest-vector basis columns must be linearly independent".into(),
-            ));
-        }
-        Ok(Self { basis, target })
+            )
+        })?;
+        let coefficient_box_bits = if basis.is_empty() {
+            0
+        } else {
+            let norms: Vec<BigInt> = basis
+                .iter()
+                .map(|column| column.iter().map(|&entry| BigInt::from(entry).pow(2)).sum())
+                .collect();
+            // Cauchy-Binet and Hadamard bound every adjugate row's squared
+            // norm by the product of the other column norms. The determinant
+            // is already available from the rank check; no source solve is needed.
+            let norm_product = norms.iter().product::<BigInt>();
+            let mut squared_radius: BigInt =
+                target.iter().map(|&entry| BigInt::from(entry).pow(2)).sum();
+            if basis.len() == ambient_dimension {
+                // With full rank, rounding A^-1 t leaves coefficient errors
+                // <=1/2. Cauchy-Schwarz gives ||B error||^2 <=r sum(norms)/4.
+                squared_radius = squared_radius
+                    .min(BigInt::from(basis.len()) * norms.iter().sum::<BigInt>() / 4);
+            }
+            // Every coefficient interval has integer width at most
+            // floor(sqrt(4 P R^2 / det(A)^2)); width's bit length is the
+            // exact-range binary bit count. BigInt keeps large cancellations exact.
+            let scaled_radius = norm_product * squared_radius * 4u32;
+            let squared_determinant = determinant.pow(2);
+            norms
+                .iter()
+                .map(|norm| {
+                    (&scaled_radius / norm / &squared_determinant)
+                        .to_biguint()
+                        .expect("squared width is nonnegative")
+                        .sqrt()
+                        .bits()
+                })
+                .fold(0u64, u64::saturating_add)
+            // Constructible target counts fit u64, so capping an upper bound
+            // at u64::MAX remains sound even if the geometric relaxation exceeds it.
+        };
+        Ok(Self {
+            basis,
+            target,
+            coefficient_box_bits,
+        })
     }
 
     /// Number of basis vectors.
@@ -93,6 +136,16 @@ impl ClosestVectorProblem {
         )
     }
 
+    /// Cached upper bound on total bits in a constructible closest-vector box.
+    ///
+    /// Uses the selected coordinate determinant, Hadamard bounds on inverse
+    /// row norms, and the zero or full-rank rounded candidate's distance bound.
+    /// Computing it adds norm sums and integer arithmetic to the existing rank
+    /// check, without computing coefficient centers or solving CVP.
+    pub fn coefficient_box_bits(&self) -> u64 {
+        self.coefficient_box_bits
+    }
+
     /// Integer basis columns.
     pub fn basis(&self) -> &[Vec<i64>] {
         &self.basis
@@ -104,18 +157,20 @@ impl ClosestVectorProblem {
     }
 
     pub(crate) fn independent_rows(&self) -> Result<Vec<usize>, ConstructionError> {
-        independent_rows(&self.basis, self.ambient_dimension()).ok_or_else(|| {
-            ConstructionError::Conversion(
-                "closest-vector basis columns must be linearly independent".into(),
-            )
-        })
+        independent_rows(&self.basis, self.ambient_dimension())
+            .map(|(rows, _)| rows)
+            .ok_or_else(|| {
+                ConstructionError::Conversion(
+                    "closest-vector basis columns must be linearly independent".into(),
+                )
+            })
     }
 }
 
-fn independent_rows(basis: &[Vec<i64>], ambient_dimension: usize) -> Option<Vec<usize>> {
+fn independent_rows(basis: &[Vec<i64>], ambient_dimension: usize) -> Option<(Vec<usize>, BigInt)> {
     let num_columns = basis.len();
     if num_columns == 0 {
-        return Some(Vec::new());
+        return Some((Vec::new(), BigInt::from(1)));
     }
 
     let mut matrix = (0..ambient_dimension)
@@ -147,7 +202,7 @@ fn independent_rows(basis: &[Vec<i64>], ambient_dimension: usize) -> Option<Vec<
         previous_pivot = pivot;
     }
     row_indices.truncate(num_columns);
-    Some(row_indices)
+    Some((row_indices, previous_pivot))
 }
 
 impl<'de> Deserialize<'de> for ClosestVectorProblem {
@@ -175,6 +230,7 @@ impl Problem for ClosestVectorProblem {
         ("ambient_dimension", ambient_dimension),
         ("num_basis_vectors", num_basis_vectors),
         ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
+        ("coefficient_box_bits", coefficient_box_bits),
     ];
 
     fn evaluate(&self, solution: &Self::Solution) -> Result<Min<i64>, EvaluationError> {

src/models/formula/nae_satisfiability.rs

@@ -74,6 +74,24 @@ impl NAESatisfiability {
         self.clauses.iter().map(|c| c.len()).sum()
     }
 
+    /// Sum of the distinct Boolean variables appearing in each clause.
+    ///
+    /// Signs and repeated occurrences do not change membership. Computing this
+    /// statistic takes expected linear time in the number of literal occurrences.
+    pub fn num_clause_variables(&self) -> usize {
+        self.clauses
+            .iter()
+            .map(|clause| {
+                clause
+                    .literals
+                    .iter()
+                    .map(|lit| lit.unsigned_abs())
+                    .collect::<std::collections::HashSet<_>>()
+                    .len()
+            })
+            .sum()
+    }
+
     /// Get the total number of literal pairs across all clauses.
     ///
     /// For each clause with k literals, this contributes C(k,2) = k*(k-1)/2 pairs.
@@ -168,6 +186,7 @@ impl Problem for NAESatisfiability {
 
     crate::problem_parameters![
         ("num_clauses", num_clauses),
+        ("num_clause_variables", num_clause_variables),
         ("num_literal_pairs", num_literal_pairs),
         ("num_literals", num_literals),
         ("num_vars", num_vars),

src/models/graph/integral_flow_homologous_arcs.rs

@@ -226,6 +226,14 @@ impl IntegralFlowHomologousArcs {
         self.capacities.iter().copied().max().unwrap_or(0)
     }
 
+    pub fn max_capacity_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits([self.max_capacity()])
+    }
+
+    pub fn num_homologous_pairs(&self) -> usize {
+        self.homologous_pairs.len()
+    }
+
     pub fn is_valid_solution(
         &self,
         config: &[usize],
@@ -299,7 +307,9 @@ impl Problem for IntegralFlowHomologousArcs {
 
     crate::problem_parameters![
         ("max_capacity", max_capacity),
+        ("max_capacity_bits", max_capacity_bits),
         ("num_arcs", num_arcs),
+        ("num_homologous_pairs", num_homologous_pairs),
         ("num_vertices", num_vertices),
     ];
 

src/models/misc/partition.rs

@@ -115,6 +115,7 @@ impl Problem for Partition {
     crate::problem_parameters![
         ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
         ("num_elements", num_elements),
+        ("total_sum", total_sum),
     ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {

src/models/misc/rectilinear_picture_compression.rs

@@ -143,6 +143,19 @@ impl RectilinearPictureCompression {
         &self.maximal_rects
     }
 
+    /// Number of cached maximal all-1 rectangles.
+    pub fn num_rectangles(&self) -> usize {
+        self.maximal_rects.len()
+    }
+
+    /// Sum of maximal rectangle areas, counting overlapping cells separately.
+    pub fn total_rectangle_area(&self) -> usize {
+        self.maximal_rects
+            .iter()
+            .map(|&(r1, c1, r2, c2)| (r2 - r1 + 1) * (c2 - c1 + 1))
+            .sum()
+    }
+
     fn build_prefix_sum(&self) -> Vec<Vec<usize>> {
         let m = self.num_rows();
         let n = self.num_cols();
@@ -248,7 +261,12 @@ impl Problem for RectilinearPictureCompression {
     type Solution = Vec<bool>;
     type Value = crate::types::Or;
 
-    crate::problem_parameters![("num_cols", num_cols), ("num_rows", num_rows),];
+    crate::problem_parameters![
+        ("num_cols", num_cols),
+        ("num_rows", num_rows),
+        ("num_rectangles", num_rectangles),
+        ("total_rectangle_area", total_rectangle_area),
+    ];
 
     fn variant() -> Vec<(&'static str, &'static str)> {
         crate::variant_params![]

src/models/misc/three_partition.rs

@@ -194,6 +194,7 @@ impl Problem for ThreePartition {
     type Value = Or;
 
     crate::problem_parameters![
+        ("bound", bound),
         ("max_numeric_magnitude_bits", max_numeric_magnitude_bits),
         ("num_elements", num_elements),
         ("num_groups", num_groups),

src/rules/balancedcompletebipartitesubgraph_ilp.rs

@@ -45,11 +45,14 @@ impl ReductionResult for ReductionBCBSToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionBCBSToILP {}
 
+// The two partition sums contain n terms total; each missing cross-pair
+// contributes one two-term row. Edge lookup deduplicates raw edges.
+// Coefficients/endpoints are 0/1 and the only other magnitude is k.
 #[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "k + 1",
+    max_constraint_magnitude_bits = "k / 2 + 1",
     num_vars = "num_vertices",
-    num_constraints = "num_vertices^2 + 2",
-    num_nonzeros = "num_vertices * (num_vertices^2 + 2)",
+    num_constraints = "left_size * right_size + 2",
+    num_nonzeros = "num_vertices + 2 * left_size * right_size",
 })]
 impl ReduceTo<ILP<bool>> for BalancedCompleteBipartiteSubgraph {
     type Result = ReductionBCBSToILP;

src/rules/bottlenecktravelingsalesman_ilp.rs

@@ -79,14 +79,17 @@ impl ReductionBTSPToILP {
     }
 }
 
+// Binary/assignment/implication/selection rows contribute 3n^2+18mn+3m
+// terms. Weight-threshold selectors add at most m^2 terms, including ties.
+// Loop orientations and parallel edges remain separate variables.
 #[reduction(transform = {
     exact {
         num_vars = "num_vertices^2 + 2 * num_edges * num_vertices + num_edges",
         num_constraints = "num_vertices^2 + 6 * num_edges * num_vertices + 4 * num_edges + 3 * num_vertices + 1",
     },
     upper_bound {
         max_constraint_magnitude_bits = "2",
-        num_nonzeros = "(num_vertices^2 + 2 * num_edges * num_vertices + num_edges) * (num_vertices^2 + 6 * num_edges * num_vertices + 4 * num_edges + 3 * num_vertices + 1)",
+        num_nonzeros = "3 * num_vertices^2 + 18 * num_edges * num_vertices + num_edges^2 + 3 * num_edges",
     },
 })]
 impl ReduceTo<ILP<bool>> for BottleneckTravelingSalesman {

src/rules/boundedcomponentspanningforest_ilp.rs

@@ -45,14 +45,17 @@ impl ReductionResult for ReductionBCSFToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionBCSFToILP {}
 
+// Assignment/weight/size/root/product/conservation rows contribute
+// <=16nk+6k terms; arc capacities and conservation add <=14mk.
+// Zero weights, n=0/1 capacity coefficients, and self-loop flows only cancel.
 #[reduction(transform = {
     exact {
         num_vars = "3 * num_vertices * max_components + 2 * max_components + 2 * num_edges * max_components",
         num_constraints = "num_vertices + 5 * max_components + 6 * num_vertices * max_components + 6 * num_edges * max_components",
     },
     upper_bound {
         max_constraint_magnitude_bits = "max_weight_bits + num_vertices",
-        num_nonzeros = "(3 * num_vertices * max_components + 2 * max_components + 2 * num_edges * max_components) * (num_vertices + 5 * max_components + 6 * num_vertices * max_components + 6 * num_edges * max_components)",
+        num_nonzeros = "16 * num_vertices * max_components + 6 * max_components + 14 * num_edges * max_components",
     },
 })]
 impl ReduceTo<ILP<i64, i64, Bounded>> for BoundedComponentSpanningForest<SimpleGraph, i64> {

src/rules/circuit_ilp.rs

@@ -194,11 +194,15 @@ impl ILPBuilder {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionCircuitToILP {}
 
+// With N expression nodes and A roots there are N-A child edges. Each
+// gate contributes at most 12 terms per child plus one per node (including
+// constants and empty gates); each output link contributes at most two.
+// Repeated operands merge/cancel. All normalized magnitudes are at most N+2.
 #[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "num_expression_nodes + num_assignment_outputs + 2",
+    max_constraint_magnitude_bits = "num_expression_nodes / 2 + 2",
     num_vars = "num_variables + 2 * num_expression_nodes",
     num_constraints = "5 * num_expression_nodes + num_assignment_outputs",
-    num_nonzeros = "(num_variables + 2 * num_expression_nodes) * (5 * num_expression_nodes + num_assignment_outputs)",
+    num_nonzeros = "13 * num_expression_nodes - 12 * num_assignments + 2 * num_assignment_outputs",
 })]
 impl ReduceTo<ILP<bool>> for CircuitSAT {
     type Result = ReductionCircuitToILP;

src/rules/closestvectorproblem_qubo.rs

@@ -276,11 +276,14 @@ fn dot(left: &[i64], right: &[i64], operation: &str) -> Result<i64, crate::rules
         })
 }
 
-// Cofactor bounds give at most r^2 + d + r*h + 3 bits per coefficient,
-// where r is the rank, d the ambient dimension, and h the input magnitude bits.
+// The source's cached geometric bound sums the bits of individual coefficient intervals,
+// including the zero-distance and empty-basis cases. It uses the same
+// selected determinant and a Hadamard bound, without computing the intervals.
+// QUBO counts only off-diagonal terms: at most N(N-1)/2<=N^2/2;
+// the latter bound also composes monotonically through bounded dimensions.
 #[reduction(transform = upper_bound {
-    num_vars = "num_basis_vectors * (num_basis_vectors^2 + ambient_dimension + num_basis_vectors * max_numeric_magnitude_bits + 3)",
-    num_quadratic_terms = "(num_basis_vectors * (num_basis_vectors^2 + ambient_dimension + num_basis_vectors * max_numeric_magnitude_bits + 3))^2",
+    num_vars = "coefficient_box_bits",
+    num_quadratic_terms = "coefficient_box_bits^2 / 2",
 })]
 impl ReduceTo<QUBO<i64>> for ClosestVectorProblem {
     type Result = ReductionCVPToQUBO;

src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs

@@ -300,9 +300,12 @@ impl crate::rules::AggregateReductionResult
 {
 }
 
+// Normalized surviving edges m'<=m contribute 14m' gadget edges;
+// incident chains add <=2m', selectors <=2n^2. Set deduplication only
+// decreases these counts; fixed YES/NO targets have at most three edges.
 #[reduction(transform = upper_bound {
     num_vertices = "num_vertices + 12 * num_edges + 3",
-    num_edges = "(num_vertices + 12 * num_edges + 3)^2",
+    num_edges = "16 * num_edges + 2 * num_vertices^2 + 3",
 })]
 impl ReduceTo<HamiltonianCircuit<SimpleGraph>> for Decision<MinimumVertexCover<SimpleGraph, One>> {
     type Result = ReductionDecisionMinimumVertexCoverToHamiltonianCircuit;