diff --git a/problemreductions-cli/tests/cli_tests.rs b/problemreductions-cli/tests/cli_tests.rs index ee8ec00c6..8013f5077 100644 --- a/problemreductions-cli/tests/cli_tests.rs +++ b/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::>(); - 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") diff --git a/src/models/algebraic/closest_vector_problem.rs b/src/models/algebraic/closest_vector_problem.rs index 2153e3a3f..0f2658844 100644 --- a/src/models/algebraic/closest_vector_problem.rs +++ b/src/models/algebraic/closest_vector_problem.rs @@ -48,6 +48,8 @@ pub struct ClosestVectorProblem { basis: Vec>, /// Target vector in the ambient space. target: Vec, + #[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 = 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::(); + 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::() / 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] { &self.basis @@ -104,18 +157,20 @@ impl ClosestVectorProblem { } pub(crate) fn independent_rows(&self) -> Result, 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], ambient_dimension: usize) -> Option> { +fn independent_rows(basis: &[Vec], ambient_dimension: usize) -> Option<(Vec, 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], ambient_dimension: usize) -> Option 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, EvaluationError> { diff --git a/src/models/formula/nae_satisfiability.rs b/src/models/formula/nae_satisfiability.rs index f65fdb717..c3edbe42c 100644 --- a/src/models/formula/nae_satisfiability.rs +++ b/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::>() + .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), diff --git a/src/models/graph/integral_flow_homologous_arcs.rs b/src/models/graph/integral_flow_homologous_arcs.rs index 67e8d9e12..e956e1049 100644 --- a/src/models/graph/integral_flow_homologous_arcs.rs +++ b/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), ]; diff --git a/src/models/misc/partition.rs b/src/models/misc/partition.rs index 5e5a36470..7d329b028 100644 --- a/src/models/misc/partition.rs +++ b/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)> { diff --git a/src/models/misc/rectilinear_picture_compression.rs b/src/models/misc/rectilinear_picture_compression.rs index 847bcebf0..b23cadb37 100644 --- a/src/models/misc/rectilinear_picture_compression.rs +++ b/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> { let m = self.num_rows(); let n = self.num_cols(); @@ -248,7 +261,12 @@ impl Problem for RectilinearPictureCompression { type Solution = Vec; 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![] diff --git a/src/models/misc/three_partition.rs b/src/models/misc/three_partition.rs index 2220198c8..4aa3d0490 100644 --- a/src/models/misc/three_partition.rs +++ b/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), diff --git a/src/rules/balancedcompletebipartitesubgraph_ilp.rs b/src/rules/balancedcompletebipartitesubgraph_ilp.rs index bd1ffb04c..d97e2f193 100644 --- a/src/rules/balancedcompletebipartitesubgraph_ilp.rs +++ b/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> for BalancedCompleteBipartiteSubgraph { type Result = ReductionBCBSToILP; diff --git a/src/rules/bottlenecktravelingsalesman_ilp.rs b/src/rules/bottlenecktravelingsalesman_ilp.rs index a1bd5bce0..ebccfb62f 100644 --- a/src/rules/bottlenecktravelingsalesman_ilp.rs +++ b/src/rules/bottlenecktravelingsalesman_ilp.rs @@ -79,6 +79,9 @@ 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", @@ -86,7 +89,7 @@ impl ReductionBTSPToILP { }, 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> for BottleneckTravelingSalesman { diff --git a/src/rules/boundedcomponentspanningforest_ilp.rs b/src/rules/boundedcomponentspanningforest_ilp.rs index 02018bba1..7710cca61 100644 --- a/src/rules/boundedcomponentspanningforest_ilp.rs +++ b/src/rules/boundedcomponentspanningforest_ilp.rs @@ -45,6 +45,9 @@ 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", @@ -52,7 +55,7 @@ impl crate::rules::AggregateReductionResult for ReductionBCSFToILP {} }, 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> for BoundedComponentSpanningForest { diff --git a/src/rules/circuit_ilp.rs b/src/rules/circuit_ilp.rs index 31fcb461f..e00574185 100644 --- a/src/rules/circuit_ilp.rs +++ b/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> for CircuitSAT { type Result = ReductionCircuitToILP; diff --git a/src/rules/closestvectorproblem_qubo.rs b/src/rules/closestvectorproblem_qubo.rs index cfe739304..dbfdf02bc 100644 --- a/src/rules/closestvectorproblem_qubo.rs +++ b/src/rules/closestvectorproblem_qubo.rs @@ -276,11 +276,14 @@ fn dot(left: &[i64], right: &[i64], operation: &str) -> Result> for ClosestVectorProblem { type Result = ReductionCVPToQUBO; diff --git a/src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs b/src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs index 2c98d97d4..c5bd03e23 100644 --- a/src/rules/decisionminimumvertexcover_hamiltoniancircuit.rs +++ b/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> for Decision> { type Result = ReductionDecisionMinimumVertexCoverToHamiltonianCircuit; diff --git a/src/rules/ensemblecomputation_ilp.rs b/src/rules/ensemblecomputation_ilp.rs index 9011e5a72..b94272171 100644 --- a/src/rules/ensemblecomputation_ilp.rs +++ b/src/rules/ensemblecomputation_ilp.rs @@ -84,10 +84,13 @@ impl ReductionResult for ReductionEnsembleComputationToILP { exact { num_vars = "3 * budget * universe_size + budget * (budget - 1) * (universe_size + 1) + num_subsets * budget + budget", num_constraints = "5 * budget - 1 + budget * (budget - 1) * (1 + 3 * universe_size) + 2 * budget * universe_size + num_subsets * budget * (universe_size + 2) + num_subsets", + // Distinct selector/product/result blocks never merge. For b>=1, + // sum activity/prefix/selection/order terms, 7 terms per product, + // both membership rows, and each target's match rows plus final sum. + num_nonzeros = "6 * budget - 2 + 9 * budget * universe_size + (4 + 9 * universe_size) * budget * (budget - 1) + num_subsets * budget * (4 + 2 * universe_size)", }, upper_bound { max_constraint_magnitude_bits = "universe_size + budget + 1", - num_nonzeros = "(3 * budget * universe_size + budget * (budget - 1) * (universe_size + 1) + num_subsets * budget + budget) * (5 * budget - 1 + budget * (budget - 1) * (1 + 3 * universe_size) + 2 * budget * universe_size + num_subsets * budget * (universe_size + 2) + num_subsets)", }, })] impl ReduceTo> for EnsembleComputation { diff --git a/src/rules/integralflowhomologousarcs_ilp.rs b/src/rules/integralflowhomologousarcs_ilp.rs index c6c8cf8b4..7cfb6dbaa 100644 --- a/src/rules/integralflowhomologousarcs_ilp.rs +++ b/src/rules/integralflowhomologousarcs_ilp.rs @@ -40,12 +40,17 @@ impl ReductionResult for ReductionIFHAToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionIFHAToILP {} +// Capacity rows contribute m terms; conservation plus sink balance use at +// most 2m; each declared homologous pair contributes at most two. Duplicate +// pairs retain separate rows, while self-loops and (a,a) pairs cancel terms. +// The clamped requirement has magnitude at most sum(capacities)+1, whose +// bits are at most h+bit_length(m) <= h+ceil(m/2+1); m=0 is also covered. #[reduction( transform = upper_bound { - max_constraint_magnitude_bits = "max_capacity * (num_arcs + 1) + 2", + max_constraint_magnitude_bits = "max_capacity_bits + num_arcs / 2 + 1", num_vars = "num_arcs", - num_constraints = "num_arcs^2 + num_arcs + num_vertices + 1", - num_nonzeros = "num_arcs * (num_arcs^2 + num_arcs + num_vertices + 1)", + num_constraints = "num_arcs + num_vertices + num_homologous_pairs", + num_nonzeros = "3 * num_arcs + 2 * num_homologous_pairs", }, )] impl ReduceTo> for IntegralFlowHomologousArcs { diff --git a/src/rules/isomorphicspanningtree_ilp.rs b/src/rules/isomorphicspanningtree_ilp.rs index 66f7db1fc..6904c4be4 100644 --- a/src/rules/isomorphicspanningtree_ilp.rs +++ b/src/rules/isomorphicspanningtree_ilp.rs @@ -42,11 +42,14 @@ impl ReductionResult for ReductionISTToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionISTToILP {} +// Two assignment families contribute 2n rows and 2n^2 terms. Each of the +// n-1 tree edges emits one two-term row per ordered non-edge, at most n(n-1). +// At n=0 both products vanish, including the otherwise negative n-1 factor. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "2", num_vars = "num_vertices * num_vertices", - num_constraints = "2 * num_vertices + 2 * (num_vertices - 1) * num_vertices * num_vertices", - num_nonzeros = "(num_vertices * num_vertices) * (2 * num_vertices + 2 * (num_vertices - 1) * num_vertices * num_vertices)", + num_constraints = "2 * num_vertices + num_vertices * (num_vertices - 1)^2", + num_nonzeros = "2 * num_vertices^2 + 2 * num_vertices * (num_vertices - 1)^2", })] impl ReduceTo> for IsomorphicSpanningTree { type Result = ReductionISTToILP; diff --git a/src/rules/ksatisfiability_preemptivescheduling.rs b/src/rules/ksatisfiability_preemptivescheduling.rs index 78aa1bc0f..c3d799ced 100644 --- a/src/rules/ksatisfiability_preemptivescheduling.rs +++ b/src/rules/ksatisfiability_preemptivescheduling.rs @@ -368,12 +368,16 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToPreemptiveSchedul } } +// Variable chains/forcing contribute 2n(n+1) precedences; clauses contribute +// 21c, retaining repeated links. Each of n+2 adjacent filler layers has at +// most P^2 links, P<=2n+3+6c. Unit lengths give d_max<=P(n+3); both factors +// are <2^(n+c+3) and <2^(n+2), respectively. Early outputs have one unit task. #[reduction(transform = upper_bound { num_tasks = "(2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3)", num_processors = "2 * num_vars + 3 + 6 * num_clauses", d_max = "(2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3)", - max_schedule_magnitude_bits = "(2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3)", - num_precedences = "((2 * num_vars + 3 + 6 * num_clauses) * (num_vars + 3))^2", + max_schedule_magnitude_bits = "2 * num_vars + num_clauses + 5", + num_precedences = "2 * num_vars * (num_vars + 1) + 21 * num_clauses + (num_vars + 2) * (2 * num_vars + 3 + 6 * num_clauses)^2", })] impl ReduceTo for KSatisfiability { type Result = Reduction3SATToPreemptiveScheduling; diff --git a/src/rules/ksatisfiability_timetabledesign.rs b/src/rules/ksatisfiability_timetabledesign.rs index 295714b52..18f6ef72f 100644 --- a/src/rules/ksatisfiability_timetabledesign.rs +++ b/src/rules/ksatisfiability_timetabledesign.rs @@ -794,14 +794,18 @@ impl ReductionResult for Reduction3SATToTimetableDesign { #[crate::aggregate_reduction(identity)] impl crate::rules::AggregateReductionResult for Reduction3SATToTimetableDesign {} +// Normalization leaves v<=L variables and q<=c+L clauses. Each variable +// has six two-list gadgets: 18 required edges and 36 available assignments. +// Each clause has <=3 edges and <=6 assignments. The two bipartition sides +// have <=1+9v+q craftsmen and <=8v+2q tasks. Periods<=4*max(1,v). #[reduction( transform = upper_bound { num_periods = "4 * num_literals + 4", - period_count_bits = "4 * num_literals + 4", - num_available_assignments = "(24 * num_literals + num_clauses + 1)^2 * (4 * num_literals + 4)", - num_nonzero_requirements = "(24 * num_literals + num_clauses + 1)^2", - num_craftsmen = "24 * num_literals + num_clauses + 1", - num_tasks = "24 * num_literals + num_clauses + 1", + period_count_bits = "num_literals + 3", + num_available_assignments = "42 * num_literals + 6 * num_clauses", + num_nonzero_requirements = "21 * num_literals + 3 * num_clauses", + num_craftsmen = "10 * num_literals + num_clauses + 1", + num_tasks = "10 * num_literals + 2 * num_clauses", } )] impl ReduceTo for KSatisfiability { diff --git a/src/rules/maximumcommonedgesubgraph_ilp.rs b/src/rules/maximumcommonedgesubgraph_ilp.rs index 4ed3f6e90..41918ab2a 100644 --- a/src/rules/maximumcommonedgesubgraph_ilp.rs +++ b/src/rules/maximumcommonedgesubgraph_ilp.rs @@ -66,11 +66,13 @@ impl ReductionResult for ReductionMCESToILP { } } +// Row/column injection inequalities contain 2*n1*n2 terms. Each compatible +// arc pair contributes at most seven McCormick terms; self-loops merge them. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "2", num_vars = "num_vertices_1 * num_vertices_2 + num_arcs_1 * num_arcs_2", num_constraints = "num_vertices_1 + num_vertices_2 + 3 * num_arcs_1 * num_arcs_2", - num_nonzeros = "(num_vertices_1 * num_vertices_2 + num_arcs_1 * num_arcs_2) * (num_vertices_1 + num_vertices_2 + 3 * num_arcs_1 * num_arcs_2)", + num_nonzeros = "2 * num_vertices_1 * num_vertices_2 + 7 * num_arcs_1 * num_arcs_2", })] impl ReduceTo> for MaximumCommonEdgeSubgraph { type Result = ReductionMCESToILP; diff --git a/src/rules/maximumindependentset_gridgraph.rs b/src/rules/maximumindependentset_gridgraph.rs index 1542a67fb..a59ac4880 100644 --- a/src/rules/maximumindependentset_gridgraph.rs +++ b/src/rules/maximumindependentset_gridgraph.rs @@ -37,10 +37,20 @@ impl ReductionResult for ReductionISSimpleOneToGridOne { } } +// At order position i, vertical slot span is <=i and horizontal span +// <=n-1-i. With spacing four, copy lines contain <=4n(n-1)+n cells. +// Only disconnected crossing gadgets increase counts: +2 vertices and +// +10 internal edges, consuming one doubled cell each. There are at most +// n(n-1)/2 doubled cells; all gadget boundary nodes are retained source +// nodes, so no outside edges are added. Other gadgets only decrease counts. +// Copy-line edges total <=4n(n-1)+5(n-1) (five extra corner contacts), +// with at most four extra contacts per pair of crossing lines. Thus final +// V<=5n^2-4n and E<=11n(n-1)+5(n-1)<=11n^2. Positive-coefficient +// relaxations preserve monotonic composition; n=0 is rejected by the mapper. #[reduction( transform = upper_bound { - num_vertices = "16 * num_vertices^2 + 32 * num_vertices + 12", - num_edges = "64 * num_vertices^2 + 128 * num_vertices + 48", + num_vertices = "5 * num_vertices^2", + num_edges = "11 * num_vertices^2", } )] impl ReduceTo> diff --git a/src/rules/minimumexternalmacrodatacompression_ilp.rs b/src/rules/minimumexternalmacrodatacompression_ilp.rs index 09e460598..485ef766e 100644 --- a/src/rules/minimumexternalmacrodatacompression_ilp.rs +++ b/src/rules/minimumexternalmacrodatacompression_ilp.rs @@ -213,11 +213,19 @@ fn encode_pointer(n: usize, start: usize, len: usize) -> usize { idx + len - 1 } -#[reduction(transform = upper_bound { - max_constraint_magnitude_bits = "1", - num_vars = "string_length * alphabet_size + 2 * string_length + string_length ^ 3", - num_constraints = "string_length + string_length * alphabet_size + string_length + string_length + 1 + string_length ^ 3 * string_length", - num_nonzeros = "(string_length * alphabet_size + 2 * string_length + string_length ^ 3) * (string_length + string_length * alphabet_size + string_length + string_length + 1 + string_length ^ 3 * string_length)", +// P=sum_{l=1}^n(n-l+1)^2=n(n+1)(2n+1)/6 pointers; +// M=sum_{l=1}^n l(n-l+1)^2=n(n+1)^2(n+2)/12 matching rows. +// Variables=nk+2n+P; rows=3n+nk+M (also zero at n=0). +// Terms=3nk+4n-2+2P+2M for n>0; dropping -2 covers the empty return. +#[reduction(transform = { + exact { + max_constraint_magnitude_bits = "1", + num_vars = "string_length * alphabet_size + 2 * string_length + string_length * (string_length + 1) * (2 * string_length + 1) / 6", + num_constraints = "3 * string_length + string_length * alphabet_size + string_length * (string_length + 1)^2 * (string_length + 2) / 12", + }, + upper_bound { + num_nonzeros = "3 * string_length * alphabet_size + 4 * string_length + string_length * (string_length + 1) * (2 * string_length + 1) / 3 + string_length * (string_length + 1)^2 * (string_length + 2) / 6", + }, })] impl ReduceTo> for MinimumExternalMacroDataCompression { type Result = ReductionEMDCToILP; diff --git a/src/rules/minimuminternalmacrodatacompression_ilp.rs b/src/rules/minimuminternalmacrodatacompression_ilp.rs index e418a0417..bf821ac5c 100644 --- a/src/rules/minimuminternalmacrodatacompression_ilp.rs +++ b/src/rules/minimuminternalmacrodatacompression_ilp.rs @@ -159,11 +159,17 @@ impl ReductionResult for ReductionIMDCToILP { } } +// Non-overlapping length-l references number at most +// (n-2l+1)(n-2l+2)/2, for 1<=l<=floor(n/2). Their sum is +// (2n^3+3n^2-2n)/24 for even n and 1/8 less for odd n. +// n(n-1)(n+3)/12 bounds it for n>=4; final ceilings cover n=0..3. +// Substring filtering only removes pointers. Every positive-length segment +// appears in exactly two endpoint rows; empty input has zero variables/terms. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "1", - num_vars = "string_len + string_len ^ 3", + num_vars = "string_len + string_len * (string_len - 1) * (string_len + 3) / 12", num_constraints = "string_len + 1", - num_nonzeros = "(string_len + string_len ^ 3) * (string_len + 1)", + num_nonzeros = "2 * string_len + string_len * (string_len - 1) * (string_len + 3) / 6", })] impl ReduceTo> for MinimumInternalMacroDataCompression { type Result = ReductionIMDCToILP; diff --git a/src/rules/minimumvertexcover_longestcommonsubsequence.rs b/src/rules/minimumvertexcover_longestcommonsubsequence.rs index 12b8bc604..cfe1799c0 100644 --- a/src/rules/minimumvertexcover_longestcommonsubsequence.rs +++ b/src/rules/minimumvertexcover_longestcommonsubsequence.rs @@ -52,7 +52,7 @@ impl ReductionResult for ReductionVCToLCS { }, }, unavailable = { - cross_frequency_product = "the exact target parameter is not represented by this reduction's symbolic transform", + cross_frequency_product = "each symbol occurs once in the base string and at most twice in each of num_edges edge strings; the source-only bound num_vertices * 2^num_edges needs a variable exponent, unsupported by the exact evaluator; endpoint incidences determine the exact product", } )] impl ReduceTo for MinimumVertexCover { diff --git a/src/rules/monochromatictriangle_ilp.rs b/src/rules/monochromatictriangle_ilp.rs index ddbc7dacd..576f62c50 100644 --- a/src/rules/monochromatictriangle_ilp.rs +++ b/src/rules/monochromatictriangle_ilp.rs @@ -43,11 +43,16 @@ impl ReductionResult for ReductionMonochromaticTriangleToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionMonochromaticTriangleToILP {} +// For T triangles, K five-cliques, and H triangles in a five-clique: +// rows=2T+15K-H and terms=6T+40K-2H. Incidence counting gives +// 10K<=T(n-3)(n-4)/2; n<3 implies T=0. This is a direct-source bound; +// bounded substitution uses the existing positive polynomial hull, dropping +// negative terms; composed predictions can therefore be looser. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "2", num_vars = "num_edges", - num_constraints = "2 * num_triangles + num_vertices^5 / 8", - num_nonzeros = "num_edges * (2 * num_triangles + num_vertices^5 / 8)", + num_constraints = "2 * num_triangles + 3 * num_triangles * (num_vertices - 3) * (num_vertices - 4) / 4", + num_nonzeros = "6 * num_triangles + 2 * num_triangles * (num_vertices - 3) * (num_vertices - 4)", })] impl ReduceTo> for MonochromaticTriangle { type Result = ReductionMonochromaticTriangleToILP; diff --git a/src/rules/naesatisfiability_ilp.rs b/src/rules/naesatisfiability_ilp.rs index b2218bee2..c748f0e97 100644 --- a/src/rules/naesatisfiability_ilp.rs +++ b/src/rules/naesatisfiability_ilp.rs @@ -44,6 +44,9 @@ impl ReductionResult for ReductionNAESATToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionNAESATToILP {} +// Each clause emits two rows. Repeated variables merge and opposite +// literals cancel, so support is at most twice the summed distinct variables. +// This retains both the dense 2*n*c cap and the occurrence 2*L cap. #[reduction(transform = { exact { num_vars = "num_vars", @@ -51,7 +54,7 @@ impl crate::rules::AggregateReductionResult for ReductionNAESATToILP {} }, upper_bound { max_constraint_magnitude_bits = "num_literals + 1", - num_nonzeros = "num_vars * (2 * num_clauses)", + num_nonzeros = "2 * num_clause_variables", }, })] impl ReduceTo> for NAESatisfiability { diff --git a/src/rules/partition_integralflowwithmultipliers.rs b/src/rules/partition_integralflowwithmultipliers.rs index 2cabe4659..db8a807eb 100644 --- a/src/rules/partition_integralflowwithmultipliers.rs +++ b/src/rules/partition_integralflowwithmultipliers.rs @@ -56,13 +56,12 @@ impl crate::rules::AggregateReductionResult for ReductionPartitionToIntegralFlow #[reduction( transform = upper_bound { + // Odd sums use capacity 1; otherwise max(1,max(sizes),S/2)<=S. + max_capacity = "total_sum", max_capacity_bits = "max_numeric_magnitude_bits + num_elements", num_vertices = "num_elements + 3", num_arcs = "2 * num_elements + 1", }, - unavailable = { - max_capacity = "bounding raw capacities from source magnitude bits requires a variable exponent; downstream ILP predictions use max_capacity_bits", - } )] impl ReduceTo for Partition { type Result = ReductionPartitionToIntegralFlowWithMultipliers; diff --git a/src/rules/partition_knapsack.rs b/src/rules/partition_knapsack.rs index 3d088f0d1..a3c08d673 100644 --- a/src/rules/partition_knapsack.rs +++ b/src/rules/partition_knapsack.rs @@ -51,11 +51,12 @@ impl crate::rules::AggregateReductionResult for ReductionPartitionToKnapsack { #[reduction( transform = { exact { num_items = "num_elements" }, - upper_bound { capacity_bits = "max_numeric_magnitude_bits + num_elements" }, + // The constructor rounds S/2 down; bound evaluation rounds up. + upper_bound { + capacity = "total_sum / 2", + capacity_bits = "max_numeric_magnitude_bits + num_elements", + }, }, - unavailable = { - capacity = "raw capacity requires numeric magnitude values; downstream predictions use capacity_bits", - } )] impl ReduceTo for Partition { type Result = ReductionPartitionToKnapsack; diff --git a/src/rules/partition_openshopscheduling.rs b/src/rules/partition_openshopscheduling.rs index fe467b900..0c5f72bc9 100644 --- a/src/rules/partition_openshopscheduling.rs +++ b/src/rules/partition_openshopscheduling.rs @@ -87,12 +87,11 @@ impl crate::rules::AggregateReductionResult for ReductionPartitionToOpenShopSche num_machines = "3", }, upper_bound { + // Three copies of each size and three floor(S/2) operations. + schedule_horizon = "9 * total_sum / 2", schedule_horizon_bits = "max_numeric_magnitude_bits + num_elements + 3", }, }, - unavailable = { - schedule_horizon = "raw horizon requires numeric magnitude values; downstream predictions use schedule_horizon_bits", - } )] impl ReduceTo> for Partition { type Result = ReductionPartitionToOpenShopScheduling; diff --git a/src/rules/partition_productionplanning.rs b/src/rules/partition_productionplanning.rs index 8ea41f028..d253639fc 100644 --- a/src/rules/partition_productionplanning.rs +++ b/src/rules/partition_productionplanning.rs @@ -41,11 +41,12 @@ impl crate::rules::AggregateReductionResult for ReductionPartitionToProductionPl #[reduction( transform = { exact { num_periods = "num_elements + 1", }, - upper_bound { max_numeric_magnitude_bits = "max_numeric_magnitude_bits + num_elements", }, + upper_bound { + // Capacities are the positive source sizes followed by zero. + max_capacity = "total_sum", + max_numeric_magnitude_bits = "max_numeric_magnitude_bits + num_elements", + }, }, - unavailable = { - max_capacity = "the exact target parameter is not represented by this reduction's symbolic transform", - } )] impl ReduceTo for Partition { type Result = ReductionPartitionToProductionPlanning; diff --git a/src/rules/partitionintocliques_ilp.rs b/src/rules/partitionintocliques_ilp.rs index b530b6fbf..6b504241e 100644 --- a/src/rules/partitionintocliques_ilp.rs +++ b/src/rules/partitionintocliques_ilp.rs @@ -49,11 +49,13 @@ impl ReductionResult for ReductionPartitionIntoCliquesToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionPartitionIntoCliquesToILP {} +// With k<=n and h absent unordered pairs: n+kh rows and nk+2kh +// terms. Use h<=n(n-1)/2; loops and parallel edges do not add rows. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "1", num_vars = "num_vertices^2", - num_constraints = "num_vertices + num_vertices^3", - num_nonzeros = "(num_vertices^2) * (num_vertices + num_vertices^3)", + num_constraints = "num_vertices + num_vertices^2 * (num_vertices - 1) / 2", + num_nonzeros = "num_vertices^3", })] impl ReduceTo> for PartitionIntoCliques { type Result = ReductionPartitionIntoCliquesToILP; diff --git a/src/rules/partitionintopathsoflength2_ilp.rs b/src/rules/partitionintopathsoflength2_ilp.rs index 8dea37fd6..8477633c7 100644 --- a/src/rules/partitionintopathsoflength2_ilp.rs +++ b/src/rules/partitionintopathsoflength2_ilp.rs @@ -67,11 +67,13 @@ impl ReductionResult for ReductionPIPL2ToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionPIPL2ToILP {} +// With q=floor(n/3) and e distinct non-loop edges: q(n+e) variables, +// n+2q+3eq rows, and 2nq+8eq terms. Deduplication gives e<=num_edges. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "2", - num_vars = "num_vertices^2 + num_edges * num_vertices", - num_constraints = "num_vertices^2 + num_edges * num_vertices + num_vertices", - num_nonzeros = "(num_vertices^2 + num_edges * num_vertices) * (num_vertices^2 + num_edges * num_vertices + num_vertices)", + num_vars = "num_vertices * (num_vertices + num_edges) / 3", + num_constraints = "5 * num_vertices / 3 + num_edges * num_vertices", + num_nonzeros = "(2 * num_vertices^2 + 8 * num_edges * num_vertices) / 3", })] impl ReduceTo> for PartitionIntoPathsOfLength2 { type Result = ReductionPIPL2ToILP; diff --git a/src/rules/partitionintotriangles_ilp.rs b/src/rules/partitionintotriangles_ilp.rs index 45dc8be3e..76787e294 100644 --- a/src/rules/partitionintotriangles_ilp.rs +++ b/src/rules/partitionintotriangles_ilp.rs @@ -60,11 +60,16 @@ impl ReductionResult for ReductionPITToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionPITToILP {} -#[reduction(transform = upper_bound { - max_constraint_magnitude_bits = "2", - num_vars = "num_vertices^2", - num_constraints = "num_vertices^2 * num_vertices", - num_nonzeros = "(num_vertices^2) * (num_vertices^2 * num_vertices)", +// Source construction requires n divisible by three, so q=n/3 exactly. +// With h absent unordered pairs: nq variables, n+q+qh rows, and +// 2nq+2qh terms. Use h<=n(n-1)/2; the empty source has q=0. +#[reduction(transform = { + exact { num_vars = "num_vertices^2 / 3", }, + upper_bound { + max_constraint_magnitude_bits = "2", + num_constraints = "4 * num_vertices / 3 + num_vertices^2 * (num_vertices - 1) / 6", + num_nonzeros = "(num_vertices^3 + num_vertices^2) / 3", + }, })] impl ReduceTo> for PartitionIntoTriangles { type Result = ReductionPITToILP; diff --git a/src/rules/rectilinearpicturecompression_ilp.rs b/src/rules/rectilinearpicturecompression_ilp.rs index 632fea4a8..083248890 100644 --- a/src/rules/rectilinearpicturecompression_ilp.rs +++ b/src/rules/rectilinearpicturecompression_ilp.rs @@ -39,12 +39,21 @@ impl ReductionResult for ReductionRPCToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionRPCToILP {} +// The source caches maximal rectangles. Each has a distinct variable and +// contributes one coefficient for each covered cell plus one budget term. +// No coefficients merge or cancel, so these two declarations are exact. +// The clamped RHS has magnitude <=max(1,R). Positive dimensions +// satisfy d(d+1)/2<2^d, hence R<2^(r+c) and its bit count is <=r+c. #[reduction( - transform = upper_bound { - max_constraint_magnitude_bits = "num_rows^2 * num_cols^2 + 1", - num_vars = "num_rows^2 * num_cols^2", - num_constraints = "num_rows * num_cols + 1", - num_nonzeros = "(num_rows^2 * num_cols^2) * (num_rows * num_cols + 1)", + transform = { + exact { + num_vars = "num_rectangles", + num_nonzeros = "total_rectangle_area + num_rectangles", + }, + upper_bound { + max_constraint_magnitude_bits = "num_rows + num_cols", + num_constraints = "num_rows * num_cols + 1", + }, }, )] impl ReduceTo> for RectilinearPictureCompression { diff --git a/src/rules/rootedtreestorageassignment_ilp.rs b/src/rules/rootedtreestorageassignment_ilp.rs index 27386196a..36339e95e 100644 --- a/src/rules/rootedtreestorageassignment_ilp.rs +++ b/src/rules/rootedtreestorageassignment_ilp.rs @@ -90,12 +90,16 @@ impl ReductionResult for ReductionRTSAToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionRTSAToILP {} +// Tree rows contribute <=9n^3+3n^2-n terms. Each nontrivial subset of +// size s contributes 10n^2+4sn^2+4n+12s+8, plus one budget term. +// Use s<=n and r<=num_subsets and drop -n. Magnitudes are bounded by +// n+1 and r(n-1); n+num_subsets+1 bits also cover n=0 and clamped budgets. #[reduction( transform = upper_bound { - max_constraint_magnitude_bits = "universe_size * (num_subsets + 1) + 2", + max_constraint_magnitude_bits = "universe_size + num_subsets + 1", num_vars = "universe_size * universe_size * universe_size + 2 * universe_size * universe_size + universe_size + num_subsets * (universe_size * universe_size + 2 * universe_size + 3)", num_constraints = "4 * universe_size^3 + 6 * universe_size^2 + 5 * universe_size + 2 + num_subsets * (2 * universe_size^3 + 5 * universe_size^2 + 8 * universe_size + 8)", - num_nonzeros = "(universe_size * universe_size * universe_size + 2 * universe_size * universe_size + universe_size + num_subsets * (universe_size * universe_size + 2 * universe_size + 3)) * (4 * universe_size^3 + 6 * universe_size^2 + 5 * universe_size + 2 + num_subsets * (2 * universe_size^3 + 5 * universe_size^2 + 8 * universe_size + 8))", + num_nonzeros = "9 * universe_size^3 + 3 * universe_size^2 + num_subsets * (4 * universe_size^3 + 10 * universe_size^2 + 16 * universe_size + 9)", }, )] impl ReduceTo> for RootedTreeStorageAssignment { diff --git a/src/rules/satisfiability_integralflowhomologousarcs.rs b/src/rules/satisfiability_integralflowhomologousarcs.rs index 042b3bed1..fb15d8236 100644 --- a/src/rules/satisfiability_integralflowhomologousarcs.rs +++ b/src/rules/satisfiability_integralflowhomologousarcs.rs @@ -129,6 +129,9 @@ impl crate::rules::AggregateReductionResult for ReductionSATToIntegralFlowHomolo num_vertices = "2 * num_vars * num_clauses + 3 * num_vars + 2 * num_clauses + 2", num_arcs = "2 * num_vars * num_clauses + 5 * num_vars + num_clauses + num_literals", max_capacity = "num_literals + 1", + // One pair per distinct signed clause literal. Capacity is 1 or at most L-1. + num_homologous_pairs = "num_literals", + max_capacity_bits = "num_literals / 2 + 2", })] impl ReduceTo for Satisfiability { type Result = ReductionSATToIntegralFlowHomologousArcs; diff --git a/src/rules/satisfiability_naesatisfiability.rs b/src/rules/satisfiability_naesatisfiability.rs index a02a28321..a7095e84b 100644 --- a/src/rules/satisfiability_naesatisfiability.rs +++ b/src/rules/satisfiability_naesatisfiability.rs @@ -58,8 +58,12 @@ impl crate::rules::AggregateReductionResult for ReductionSATToNAESAT {} num_clauses = "num_clauses", }, upper_bound { + // Nonempty clauses add one fresh sentinel; empty clauses use (s,s). + num_clause_variables = "num_literals + num_clauses", num_literals = "num_literals + 2 * num_clauses", - num_literal_pairs = "(num_literals + 2 * num_clauses)^2", + // Nonempty length l contributes l(l+1)/2; an empty clause contributes + // one pair. Sum l^2 <= (sum l)^2, including repeated literals. + num_literal_pairs = "num_literals * (num_literals + 1) / 2 + num_clauses", }, })] impl ReduceTo for Satisfiability { diff --git a/src/rules/sequencingwithinintervals_ilp.rs b/src/rules/sequencingwithinintervals_ilp.rs index 1cb662236..1ff775fd4 100644 --- a/src/rules/sequencingwithinintervals_ilp.rs +++ b/src/rules/sequencingwithinintervals_ilp.rs @@ -76,11 +76,13 @@ impl ReductionResult for ReductionSWIToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionSWIToILP {} +// S start slots contribute S assignment terms; at most S(S-1)/2 +// unordered slot pairs emit two-term conflict rows, giving at most S^2 terms. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "1", num_vars = "num_start_slots", - num_constraints = "num_start_slots^2 + num_tasks", - num_nonzeros = "num_start_slots * (num_start_slots^2 + num_tasks)", + num_constraints = "num_tasks + num_start_slots * (num_start_slots - 1) / 2", + num_nonzeros = "num_start_slots^2", })] impl ReduceTo> for SequencingWithinIntervals { type Result = ReductionSWIToILP; diff --git a/src/rules/shortestcommonsupersequence_ilp.rs b/src/rules/shortestcommonsupersequence_ilp.rs index 453e8e634..b59376466 100644 --- a/src/rules/shortestcommonsupersequence_ilp.rs +++ b/src/rules/shortestcommonsupersequence_ilp.rs @@ -45,11 +45,15 @@ impl ReductionResult for ReductionSCSToILP { } } +// With b positions and L source characters: symbol/match/link rows +// contribute b(a+1)+3Lb terms, order rows <=2Lb, padding <=2b. +// Zero positional coefficients disappear. Coefficients <=max(1,b-1) +// require at most ceil(b/2+1) bits, including b=0. #[reduction(transform = upper_bound { - max_constraint_magnitude_bits = "max_length + 1", + max_constraint_magnitude_bits = "max_length / 2 + 1", num_vars = "max_length * (alphabet_size + 1) + total_length * max_length", num_constraints = "max_length + total_length + total_length * max_length + total_length + max_length", - num_nonzeros = "(max_length * (alphabet_size + 1) + total_length * max_length) * (max_length + total_length + total_length * max_length + total_length + max_length)", + num_nonzeros = "max_length * (alphabet_size + 3) + 5 * total_length * max_length", })] impl ReduceTo> for ShortestCommonSupersequence { type Result = ReductionSCSToILP; diff --git a/src/rules/sparsematrixcompression_ilp.rs b/src/rules/sparsematrixcompression_ilp.rs index bb5efda1d..6156f5e2c 100644 --- a/src/rules/sparsematrixcompression_ilp.rs +++ b/src/rules/sparsematrixcompression_ilp.rs @@ -45,11 +45,13 @@ impl ReductionResult for ReductionSMCToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionSMCToILP {} +// Assignments contribute r*k terms. Each unordered row pair and pair +// of columns emits at most k two-term collision rows; empty columns add none. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "1", num_vars = "num_rows * bound_k", - num_constraints = "num_rows + num_rows^2 * num_cols^2 * bound_k", - num_nonzeros = "(num_rows * bound_k) * (num_rows + num_rows^2 * num_cols^2 * bound_k)", + num_constraints = "num_rows + num_rows * (num_rows - 1) * num_cols^2 * bound_k / 2", + num_nonzeros = "num_rows * bound_k + num_rows * (num_rows - 1) * num_cols^2 * bound_k", })] impl ReduceTo> for SparseMatrixCompression { type Result = ReductionSMCToILP; diff --git a/src/rules/stackercrane_ilp.rs b/src/rules/stackercrane_ilp.rs index 1795e54ad..c24517495 100644 --- a/src/rules/stackercrane_ilp.rs +++ b/src/rules/stackercrane_ilp.rs @@ -44,11 +44,14 @@ impl ReductionResult for ReductionSCToILP { } } +// Two assignment families contribute 2m^2 terms. Each of m^3 +// products contributes at most seven terms plus one unreachable-pair pin. +// At m=1 repeated operands merge; at m=0 the target is empty. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "2", num_vars = "num_arcs * num_arcs + num_arcs * num_arcs * num_arcs", num_constraints = "num_arcs + num_arcs + 4 * num_arcs * num_arcs * num_arcs", - num_nonzeros = "(num_arcs * num_arcs + num_arcs * num_arcs * num_arcs) * (num_arcs + num_arcs + 4 * num_arcs * num_arcs * num_arcs)", + num_nonzeros = "2 * num_arcs^2 + 8 * num_arcs^3", })] impl ReduceTo> for StackerCrane { type Result = ReductionSCToILP; diff --git a/src/rules/stringtostringcorrection_ilp.rs b/src/rules/stringtostringcorrection_ilp.rs index f8b674bcf..5acadd719 100644 --- a/src/rules/stringtostringcorrection_ilp.rs +++ b/src/rules/stringtostringcorrection_ilp.rs @@ -115,11 +115,14 @@ impl ReductionResult for ReductionSTSCToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionSTSCToILP {} +// State/initial/final rows contribute <=(2k+4)n^2+(3k+5)n terms; +// operation/legality rows <=8kn+k; updates <=12kn^3+6kn^2. +// The length-rejection target has no terms; n=0 has k one-term no-op rows. #[reduction(transform = upper_bound { max_constraint_magnitude_bits = "1", num_vars = "(bound + 1) * source_length^2 + (bound + 1) * source_length + 2 * bound * source_length + bound", num_constraints = "4 * bound * source_length^3 + 2 * bound * source_length^2 + source_length^2 + 6 * bound * source_length + 5 * source_length + bound + 1", - num_nonzeros = "((bound + 1) * source_length^2 + (bound + 1) * source_length + 2 * bound * source_length + bound) * (4 * bound * source_length^3 + 2 * bound * source_length^2 + source_length^2 + 6 * bound * source_length + 5 * source_length + bound + 1)", + num_nonzeros = "12 * bound * source_length^3 + (8 * bound + 4) * source_length^2 + (11 * bound + 5) * source_length + bound", })] impl ReduceTo> for StringToStringCorrection { type Result = ReductionSTSCToILP; diff --git a/src/rules/subsetsum_closestvectorproblem.rs b/src/rules/subsetsum_closestvectorproblem.rs index 6a0142f0d..1a04d0531 100644 --- a/src/rules/subsetsum_closestvectorproblem.rs +++ b/src/rules/subsetsum_closestvectorproblem.rs @@ -67,6 +67,11 @@ impl ReductionSubsetSumToClosestVectorProblem { } } +// For r=n+k-1 columns, the selected determinant is one. Element column +// squared norms are <=k+2, carry norms are five, and target squared norm +// is <=n+k=r+1. For r>=1, k+4<=2^(k+2) and r+1<=2^r, so width +// <=2^(((r-1)(k+2)+r)/2+1). Its bit length is <=r(k+3)/2+2. +// Sum the per-coordinate bound over r columns. The empty basis has zero bits. #[reduction(transform = { exact { ambient_dimension = "2 * num_elements + max_numeric_magnitude_bits", @@ -74,6 +79,7 @@ impl ReductionSubsetSumToClosestVectorProblem { }, upper_bound { max_numeric_magnitude_bits = "2", + coefficient_box_bits = "(num_elements + max_numeric_magnitude_bits - 1) * ((num_elements + max_numeric_magnitude_bits - 1) * (max_numeric_magnitude_bits + 3) / 2 + 2)", } })] impl ReduceTo> for SubsetSum { diff --git a/src/rules/subsetsum_partition.rs b/src/rules/subsetsum_partition.rs index d59308bc3..a70e9bdf8 100644 --- a/src/rules/subsetsum_partition.rs +++ b/src/rules/subsetsum_partition.rs @@ -73,6 +73,9 @@ impl crate::rules::AggregateReductionResult for ReductionSubsetSumToPartition {} transform = upper_bound { max_numeric_magnitude_bits = "max_numeric_magnitude_bits + num_elements + 1", num_elements = "num_elements + 1", + }, + unavailable = { + total_sum = "target sum is source_sum + abs(source_sum - 2*target); neither raw source_sum nor target is in the source schema, which accepts arbitrary-precision values; a scale-sensitive bound from magnitude bits requires a variable exponent unsupported by the exact evaluator", })] impl ReduceTo for SubsetSum { type Result = ReductionSubsetSumToPartition; diff --git a/src/rules/threedimensionalmatching_threepartition.rs b/src/rules/threedimensionalmatching_threepartition.rs index 6a506ea64..8697414ec 100644 --- a/src/rules/threedimensionalmatching_threepartition.rs +++ b/src/rules/threedimensionalmatching_threepartition.rs @@ -345,6 +345,8 @@ impl crate::rules::AggregateReductionResult for ReductionThreeDimensionalMatchin #[reduction( transform = upper_bound { + // B=64*(16*40*(32q)^4+15)+4; fixed YES/NO bounds are 3/20. + bound = "40960 * (32 * universe_size)^4 + 964", max_numeric_magnitude_bits = "4 * universe_size + 36", num_elements = "24 * num_triples * num_triples - 3 * num_triples + 6", num_groups = "8 * num_triples * num_triples - num_triples + 2", diff --git a/src/rules/threepartition_sequencingwithreleasetimesanddeadlines.rs b/src/rules/threepartition_sequencingwithreleasetimesanddeadlines.rs index 06d5b7a27..d23088f09 100644 --- a/src/rules/threepartition_sequencingwithreleasetimesanddeadlines.rs +++ b/src/rules/threepartition_sequencingwithreleasetimesanddeadlines.rs @@ -96,12 +96,13 @@ impl crate::rules::AggregateReductionResult for ReductionThreePartitionToSRTD {} #[reduction( transform = { - exact { num_tasks = "num_elements + num_groups - 1", }, + // Validated ThreePartition inputs have at least one group. + exact { + num_tasks = "num_elements + num_groups - 1", + time_horizon = "num_groups * (bound + 1) - 1", + }, upper_bound { time_horizon_bits = "max_numeric_magnitude_bits + num_groups + 1", }, }, - unavailable = { - time_horizon = "the exact target parameter is not represented by this reduction's symbolic transform", - } )] impl ReduceTo for ThreePartition { type Result = ReductionThreePartitionToSRTD; diff --git a/src/unit_tests/ilp_overhead.rs b/src/unit_tests/ilp_overhead.rs index 70fc6bed5..21ab2b84a 100644 --- a/src/unit_tests/ilp_overhead.rs +++ b/src/unit_tests/ilp_overhead.rs @@ -8,11 +8,693 @@ use crate::solvers::{BruteForce, BruteForceProblem, ILPSolver}; use crate::topology::{DirectedGraph, SimpleGraph}; use crate::{ types::{Min, One}, - Problem, + Problem, ProblemParameters, }; type BoundedILP = ILP; +// Expected counts below come from enumerated rows/segments, independently of +// the registered expressions. Check predictions as well as the real targets. +fn check_counts, T: Problem>(source: &S, counts: &[(&str, u64, u64)]) { + let (actual, predicted) = check_contract::(source); + for &(field, measured, bound) in counts { + assert_eq!( + actual.get(field), + Some(measured), + "{}: actual {field}", + S::NAME + ); + assert_eq!( + predicted.get(field), + Some(bound), + "{}: predicted {field}", + S::NAME + ); + } +} + +#[test] +fn partition_gadgets_count_sparse_rows_on_the_accepted_domain() { + let entry = crate::rules::registry::reduction_entries() + .into_iter() + .find(|e| e.source_name == "PartitionIntoTriangles" && e.target_name == "ILP") + .unwrap(); + assert_eq!( + entry + .parameter_contract() + .unwrap() + .transform() + .unwrap() + .relation("num_vars"), + Some(ParameterRelation::Exact) + ); + check_counts::<_, ILP>( + &PartitionIntoTriangles::new(SimpleGraph::complete(3)), + &[ + ("num_vars", 3, 3), + ("num_constraints", 4, 7), + ("num_nonzeros", 6, 12), + ], + ); + check_counts::<_, ILP>( + &PartitionIntoTriangles::new(SimpleGraph::empty(6)), + &[ + ("num_vars", 12, 12), + ("num_constraints", 38, 38), + ("num_nonzeros", 84, 84), + ], + ); + check_counts::<_, ILP>( + &PartitionIntoPathsOfLength2::new(SimpleGraph::path(3)), + &[ + ("num_vars", 5, 5), + ("num_constraints", 11, 11), + ("num_nonzeros", 22, 22), + ], + ); + check_counts::<_, ILP>( + &PartitionIntoCliques::new(SimpleGraph::empty(3), 2), + &[("num_constraints", 9, 12), ("num_nonzeros", 18, 27)], + ); + for n in [0, 3] { + check_contract::<_, ILP>(&PartitionIntoTriangles::new(SimpleGraph::empty(n))); + check_contract::<_, ILP>(&PartitionIntoPathsOfLength2::new(SimpleGraph::empty(n))); + } + // Loops never become product variables; parallel orientations merge. + check_contract::<_, ILP>(&PartitionIntoPathsOfLength2::new(SimpleGraph::new( + 3, + vec![(0, 0), (0, 1), (1, 0), (1, 2)], + ))); +} + +#[test] +fn macro_segments_count_endpoint_and_matching_terms() { + // Three literals and three non-overlapping one-character references. + check_counts::<_, ILP>( + &MinimumInternalMacroDataCompression::new(1, vec![0, 0, 0], 1), + &[("num_vars", 6, 6), ("num_nonzeros", 12, 12)], + ); + for (string, vars, terms) in [(vec![], 0, 0), (vec![0, 1], 2, 4), (vec![0, 0], 3, 6)] { + check_counts::<_, ILP>( + &MinimumInternalMacroDataCompression::new(2, string, 2), + &[ + ("num_vars", vars, if vars == 0 { 0 } else { 3 }), + ("num_nonzeros", terms, if vars == 0 { 0 } else { 6 }), + ], + ); + } + // n=2: five pointers, six pointer-character matches, four dictionary bits. + check_counts::<_, ILP>( + &MinimumExternalMacroDataCompression::new(2, vec![0, 1], 2), + &[ + ("num_vars", 13, 13), + ("num_constraints", 16, 16), + ("num_nonzeros", 40, 42), + ], + ); + check_counts::<_, ILP>( + &MinimumExternalMacroDataCompression::new(0, vec![], 2), + &[ + ("num_vars", 0, 0), + ("num_constraints", 0, 0), + ("num_nonzeros", 0, 0), + ], + ); +} + +#[test] +fn triangle_strengthening_counts_cliques_without_dense_rows() { + // K5: ten triangle pairs and five degree rows, no opposite-edge equalities. + check_counts::<_, ILP>( + &MonochromaticTriangle::new(SimpleGraph::complete(5)), + &[ + ("num_vars", 10, 10), + ("num_constraints", 25, 35), + ("num_nonzeros", 80, 100), + ], + ); + // K6: 20 triangles, six K5s, and three opposite edges per base triangle. + check_counts::<_, ILP>( + &MonochromaticTriangle::new(SimpleGraph::complete(6)), + &[("num_constraints", 110, 130), ("num_nonzeros", 320, 360)], + ); + for n in 0..5 { + check_contract::<_, ILP>(&MonochromaticTriangle::new(SimpleGraph::empty(n))); + } +} + +#[test] +fn rectangle_bounds_cover_empty_shapes_and_normalized_budgets() { + for bound in [i64::MIN, 0, 1, i64::MAX] { + // One maximal 2x2 rectangle: four cell rows and one budget row. + check_counts::<_, ILP>( + &RectilinearPictureCompression::new(vec![vec![true; 2]; 2], bound), + &[ + ("num_vars", 1, 1), + ("num_nonzeros", 5, 5), + ("max_constraint_magnitude_bits", 1, 4), + ], + ); + } + for matrix in [vec![vec![false]], vec![vec![false; 2]; 2]] { + check_counts::<_, ILP>( + &RectilinearPictureCompression::new(matrix, i64::MIN), + &[("num_vars", 0, 0), ("num_nonzeros", 0, 0)], + ); + } + // The two maximal dominoes overlap at the top-left cell: four incidences, + // rather than three distinct true cells, and two budget coefficients. + check_counts::<_, ILP>( + &RectilinearPictureCompression::new(vec![vec![true, true], vec![true, false]], 2), + &[("num_vars", 2, 2), ("num_nonzeros", 6, 6)], + ); + check_counts::<_, ILP>( + &RectilinearPictureCompression::new(vec![vec![true, false, true]], 2), + &[("num_vars", 2, 2), ("num_nonzeros", 4, 4)], + ); +} + +#[test] +fn nae_support_ignores_repeated_literals_and_bounds_cancellation() { + use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability}; + for (literals, variables, terms) in [ + (vec![1, 2], 2, 4), + (vec![1, 1, 1, 1], 1, 2), + (vec![1, -1, 2, 2], 2, 2), + (vec![1, -1], 1, 0), + ] { + let source = NAESatisfiability::new(4, vec![CNFClause::new(literals)]); + assert_eq!( + source.parameters().get("num_clause_variables"), + Some(variables) + ); + check_counts::<_, ILP>(&source, &[("num_nonzeros", terms, 2 * variables)]); + } + check_counts::<_, ILP>( + &NAESatisfiability::new(0, vec![]), + &[("num_nonzeros", 0, 0)], + ); + for clauses in [ + vec![CNFClause::new(vec![])], + vec![CNFClause::new(vec![1, 1])], + ] { + check_contract::<_, NAESatisfiability>(&Satisfiability::new(1, clauses)); + } +} + +#[test] +fn timetable_counts_core_edges_and_their_available_colors() { + use crate::models::formula::{CNFClause, KSatisfiability}; + use crate::variant::K3; + let source = KSatisfiability::::new_allow_less( + 1, + vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + ); + // Six two-list variable edges each supply three edges with two colors; + // the two singleton clause edges each supply one available assignment. + check_counts::<_, TimetableDesign>( + &source, + &[ + ("num_nonzero_requirements", 20, 48), + ("num_available_assignments", 38, 96), + ("period_count_bits", 3, 5), + ("num_craftsmen", 10, 23), + ("num_tasks", 10, 24), + ], + ); + check_contract::<_, TimetableDesign>(&KSatisfiability::::new_allow_less(0, vec![])); + check_contract::<_, TimetableDesign>(&KSatisfiability::::new_allow_less( + 0, + vec![CNFClause::new(vec![])], + )); +} + +#[test] +fn lattice_bounds_count_bits_and_off_diagonal_terms() { + use crate::models::algebraic::ClosestVectorProblem; + // Determinant four, largest complementary squared norm five, and rounded + // residual squared at most four: coefficient width <=sqrt(5)<3, or two bits. + check_counts::<_, QUBO>( + &ClosestVectorProblem::new(vec![vec![2, 0], vec![1, 2]], vec![3, 1]).unwrap(), + &[("num_vars", 1, 4), ("num_quadratic_terms", 0, 8)], + ); + check_counts::<_, QUBO>( + &ClosestVectorProblem::new(vec![], vec![]).unwrap(), + &[("num_vars", 0, 0), ("num_quadratic_terms", 0, 0)], + ); +} + +#[test] +fn lattice_geometry_bounds_preserve_ambient_residuals_and_cancellation() { + use crate::models::algebraic::ClosestVectorProblem; + // An unspanned residual of length two permits coefficients -2..=2. + // Three bits encode that range; the two orthogonal blocks each have three + // interactions, and every interaction between the blocks cancels. + let source = + ClosestVectorProblem::new(vec![vec![1, 0, 0], vec![0, 1, 0]], vec![0, 0, 2]).unwrap(); + assert_eq!(source.parameters().get("coefficient_box_bits"), Some(6)); + check_counts::<_, QUBO>( + &source, + &[("num_vars", 6, 6), ("num_quadratic_terms", 6, 18)], + ); + // A one-bit interval exercises the final ceiling of the off-diagonal cap. + check_counts::<_, QUBO>( + &ClosestVectorProblem::new(vec![vec![2]], vec![1]).unwrap(), + &[("num_vars", 1, 1), ("num_quadratic_terms", 0, 1)], + ); + check_counts::<_, QUBO>( + &ClosestVectorProblem::new(vec![vec![2]], vec![0]).unwrap(), + &[("num_vars", 0, 0), ("num_quadratic_terms", 0, 0)], + ); +} + +#[test] +fn lattice_box_bits_sum_distinct_coordinate_widths() { + use crate::models::algebraic::ClosestVectorProblem; + // Selected determinant one, squared complementary norms ten and one, + // and an unspanned residual squared of one: widths six and two use three + // and two bits. All ten off-diagonal pairs have nonzero Gram coefficients. + check_counts::<_, QUBO>( + &ClosestVectorProblem::new(vec![vec![1, 0, 0], vec![3, 1, 0]], vec![0, 0, 1]).unwrap(), + &[("num_vars", 5, 5), ("num_quadratic_terms", 10, 13)], + ); +} + +#[test] +fn kings_mapping_bounds_count_wires_and_gadget_edges() { + use crate::topology::KingsSubgraph; + check_counts::<_, MaximumIndependentSet>( + &MaximumIndependentSet::new(SimpleGraph::empty(1), vec![One]), + &[("num_vertices", 1, 5), ("num_edges", 0, 11)], + ); + // Two adjacent source vertices simplify to a single target edge. + check_counts::<_, MaximumIndependentSet>( + &MaximumIndependentSet::new(SimpleGraph::new(2, vec![(0, 1)]), vec![One; 2]), + &[("num_vertices", 2, 20), ("num_edges", 1, 44)], + ); +} + +#[test] +fn rooted_tree_bounds_count_each_sparse_gadget() { + use crate::models::set::RootedTreeStorageAssignment; + // Two vertices contribute 82 terms; the two-element subset contributes + // 112 gadget terms and one budget term. Dropping -n gives excess two. + check_counts::<_, BoundedILP>( + &RootedTreeStorageAssignment::new(2, vec![vec![0, 1]], 1), + &[ + ("num_nonzeros", 195, 197), + ("max_constraint_magnitude_bits", 2, 4), + ], + ); + check_contract::<_, BoundedILP>(&RootedTreeStorageAssignment::new(0, vec![], i64::MIN)); + check_contract::<_, BoundedILP>(&RootedTreeStorageAssignment::new( + 1, + vec![vec![], vec![0]], + i64::MAX, + )); +} + +#[test] +fn sparse_matrix_and_schedule_rows_count_conflicting_pairs() { + use crate::models::algebraic::SparseMatrixCompression; + check_counts::<_, ILP>( + &SparseMatrixCompression::new(vec![vec![true], vec![true]], 2), + &[ + ("num_vars", 4, 4), + ("num_constraints", 4, 4), + ("num_nonzeros", 8, 8), + ], + ); + check_counts::<_, ILP>( + &SequencingWithinIntervals::new(vec![0, 0], vec![2, 2], vec![1, 1]).unwrap(), + &[ + ("num_vars", 4, 4), + ("num_constraints", 4, 8), + ("num_nonzeros", 8, 16), + ], + ); +} + +#[test] +fn flow_and_tour_bounds_include_sparse_global_rows() { + check_counts::<_, BoundedILP>( + &BoundedComponentSpanningForest::new(SimpleGraph::path(2), vec![1, 1], 1, 2), + &[("num_nonzeros", 52, 52)], + ); + check_contract::<_, BoundedILP>(&BoundedComponentSpanningForest::new( + SimpleGraph::new(1, vec![(0, 0)]), + vec![0], + 1, + 1, + )); + check_counts::<_, ILP>( + &StackerCrane::new(3, vec![(0, 1), (2, 0)], vec![(1, 2)], vec![1, 1], vec![1]), + &[("num_nonzeros", 64, 72)], + ); + check_counts::<_, ILP>( + &BottleneckTravelingSalesman::new(SimpleGraph::path(2), vec![1]), + &[("num_nonzeros", 52, 52)], + ); +} + +#[test] +fn string_state_rows_count_terms_instead_of_dense_entries() { + check_counts::<_, ILP>( + &ShortestCommonSupersequence::new(2, vec![vec![0, 1], vec![1, 0]]), + &[ + ("num_vars", 28, 28), + ("num_nonzeros", 78, 100), + ("max_constraint_magnitude_bits", 2, 3), + ], + ); + check_counts::<_, ILP>( + &StringToStringCorrection::new(1, vec![0], vec![0], 1), + &[("num_nonzeros", 21, 41)], + ); + check_counts::<_, ILP>( + &StringToStringCorrection::new(0, vec![], vec![], 2), + &[("num_nonzeros", 2, 2)], + ); + check_contract::<_, ILP>(&StringToStringCorrection::new(1, vec![], vec![0], 2)); +} + +#[test] +fn ensemble_terms_include_ordering_and_target_matches() { + // Two operands, one operation, one target: 1 activity bound, four selector + // terms + two activity terms, five ordering terms, ten union/disjoint + // terms, and eight match terms. + check_counts::<_, ILP>( + &EnsembleComputation::new(2, vec![vec![0, 1]], 1), + &[("num_nonzeros", 30, 30)], + ); + check_counts::<_, ILP>( + &EnsembleComputation::new(0, vec![], 1), + &[("num_nonzeros", 4, 4)], + ); +} + +#[test] +fn changed_predictions_bound_real_intermediate_targets() { + use crate::models::formula::{CNFClause, KSatisfiability, NAESatisfiability, Satisfiability}; + use crate::variant::K3; + let source = KSatisfiability::::new_allow_less( + 1, + vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + ); + for intermediate in [ + step::(), + step::>(), + ] { + let first = ReductionPath { + steps: vec![step::>(), intermediate], + }; + let mut second = first.clone(); + second.steps.push(step::>()); + let graph = ReductionGraph::new(); + for path in [first, second] { + let chain = graph.reduce_along_path(&path, &source).unwrap().unwrap(); + let predicted = graph + .compose_path_parameter_transform(&path) + .unwrap() + .unwrap() + .evaluate(&source.parameters()) + .unwrap(); + let target = path.steps.last().unwrap(); + let actual = ReductionGraph::compute_problem_parameters( + &target.name, + &target.variant, + chain.target_problem_any(), + ); + for (field, value) in actual.iter() { + assert!( + predicted.get(field).expect(field) >= value, + "{path:?}: {field}" + ); + } + } + } + // Includes empty clauses, repeated literals and a fresh sentinel through + // the new incoming support contract and a real solve/extract workflow. + for literals in [vec![], vec![1, 1], vec![1, -1]] { + check_path( + Satisfiability::new(1, vec![CNFClause::new(literals)]), + ReductionPath { + steps: vec![ + step::(), + step::(), + step::>(), + step::>(), + ], + }, + ); + } +} + +#[test] +fn circuit_support_counts_constant_leaves_and_xor_folds() { + use crate::models::formula::{Assignment, BooleanExpr, Circuit, CircuitSAT}; + let source = CircuitSAT::new(Circuit::new(vec![Assignment::new( + vec!["out".into()], + BooleanExpr::xor(vec![BooleanExpr::constant(false); 32]), + )])); + // 32 one-term constant rows, 31 four-row XORs of three terms, one output link. + check_counts::<_, ILP>( + &source, + &[ + ("num_nonzeros", 406, 419), + ("max_constraint_magnitude_bits", 2, 19), + ], + ); + for expression in [ + BooleanExpr::and(vec![]), + BooleanExpr::or(vec![]), + BooleanExpr::xor(vec![]), + BooleanExpr::xor(vec![BooleanExpr::var("out"), BooleanExpr::var("out")]), + ] { + check_contract::<_, ILP>(&CircuitSAT::new(Circuit::new(vec![Assignment::new( + vec!["out".into()], + expression, + )]))); + } +} + +#[test] +fn graph_mapping_rows_count_non_edges() { + check_counts::<_, ILP>( + &IsomorphicSpanningTree::new(SimpleGraph::path(3), SimpleGraph::path(3)), + &[("num_constraints", 10, 18), ("num_nonzeros", 26, 42)], + ); + use crate::topology::BipartiteGraph; + check_counts::<_, ILP>( + &BalancedCompleteBipartiteSubgraph::new(BipartiteGraph::new(2, 2, vec![]), 2), + &[ + ("num_constraints", 6, 6), + ("num_nonzeros", 12, 12), + ("max_constraint_magnitude_bits", 2, 2), + ], + ); +} + +#[test] +fn homologous_flow_support_counts_repeated_pairs() { + // Accepted duplicate pair declarations each emit their own equality row; + // pair count cannot be bounded by a function of arc/vertex counts alone. + let source = IntegralFlowHomologousArcs::new( + DirectedGraph::new(2, vec![(0, 1), (0, 1)]), + vec![1, 1], + 0, + 1, + 1, + vec![(0, 1); 10], + ); + check_counts::<_, BoundedILP>( + &source, + &[("num_constraints", 13, 14), ("num_nonzeros", 24, 26)], + ); + assert_eq!(source.parameters().get("num_homologous_pairs"), Some(10)); + // All terms in a (self,self) homologous equality cancel. + let source = IntegralFlowHomologousArcs::new( + DirectedGraph::new(1, vec![(0, 0)]), + vec![i64::MAX], + 0, + 0, + i64::MAX, + vec![(0, 0); 10], + ); + assert_eq!(source.parameters().get("max_capacity_bits"), Some(63)); + check_counts::<_, BoundedILP>(&source, &[("max_constraint_magnitude_bits", 63, 65)]); + use crate::models::formula::{CNFClause, Satisfiability}; + let source = Satisfiability::new(1, vec![CNFClause::new(vec![1, 1, -1])]); + check_counts::<_, IntegralFlowHomologousArcs>( + &source, + &[("num_homologous_pairs", 2, 3), ("max_capacity_bits", 1, 4)], + ); + for clauses in [ + vec![], + vec![CNFClause::new(vec![1])], + vec![CNFClause::new(vec![])], + ] { + check_path( + Satisfiability::new(1, clauses), + ReductionPath { + steps: vec![ + step::(), + step::(), + step::(), + step::>(), + step::>(), + ], + }, + ); + } +} + +#[test] +fn labelled_graph_products_count_sparse_support() { + use crate::models::graph::{LabelledArc, LabelledDigraph}; + for (n, arc, terms) in [ + (2, LabelledArc::new(0, 0, 1), 15), + (1, LabelledArc::new(0, 0, 0), 8), + ] { + let graph = LabelledDigraph::new(n, vec![arc]); + check_counts::<_, ILP>( + &MaximumCommonEdgeSubgraph::new(graph.clone(), graph), + &[("num_nonzeros", terms, 2 * n as u64 * n as u64 + 7)], + ); + } + check_contract::<_, ILP>(&MaximumCommonEdgeSubgraph::new( + LabelledDigraph::new(0, vec![]), + LabelledDigraph::new(2, vec![]), + )); +} + +#[test] +fn sentinel_literal_pairs_count_each_clause_once() { + use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability}; + check_counts::<_, NAESatisfiability>( + &Satisfiability::new( + 1, + vec![CNFClause::new(vec![]), CNFClause::new(vec![1, 1, -1])], + ), + &[("num_literal_pairs", 7, 8)], + ); +} + +#[test] +fn unit_schedule_bits_and_precedences_count_layers() { + use crate::models::formula::{CNFClause, KSatisfiability}; + use crate::variant::K3; + // Capacities [1,3,3,6], seven processors, filler sizes [6,4,4,1]. + // 4 variable links + 21 literal links + 24+16+4 filler links. + check_counts::<_, PreemptiveScheduling>( + &KSatisfiability::::new_allow_less(1, vec![CNFClause::new(vec![1])]), + &[ + ("num_precedences", 69, 388), + ("max_schedule_magnitude_bits", 5, 8), + ], + ); + for clauses in [vec![], vec![CNFClause::new(vec![])]] { + check_contract::<_, PreemptiveScheduling>(&KSatisfiability::::new_allow_less( + 0, clauses, + )); + } +} + +#[test] +fn numeric_source_sums_make_raw_target_predictions_available() { + use crate::models::Decision; + for (sizes, sum, capacity, horizon) in [ + (vec![1], 1u64, 0, 3), + (vec![1, 2], 3, 1, 12), + (vec![1, 3], 4, 2, 18), + ] { + let source = Partition::new(sizes).unwrap(); + check_counts::<_, Knapsack>(&source, &[("capacity", capacity, sum.div_ceil(2))]); + check_counts::<_, Decision>( + &source, + &[("schedule_horizon", horizon, (9 * sum).div_ceil(2))], + ); + check_counts::<_, IntegralFlowWithMultipliers>( + &source, + &[("max_capacity", if sum % 2 == 1 { 1 } else { 3 }, sum)], + ); + check_counts::<_, ProductionPlanning>( + &source, + &[( + "max_capacity", + if sum == 1 { + 1 + } else if sum == 3 { + 2 + } else { + 3 + }, + sum, + )], + ); + assert_eq!(source.parameters().get("total_sum"), Some(sum)); + } + let source = ThreePartition::new(vec![1; 3], 3); + check_counts::<_, SequencingWithReleaseTimesAndDeadlines>(&source, &[("time_horizon", 3, 3)]); + assert_eq!(source.parameters().get("bound"), Some(3)); + use crate::models::set::ThreeDimensionalMatching; + for source in [ + ThreeDimensionalMatching::new(0, vec![]), + ThreeDimensionalMatching::new(1, vec![]), + ThreeDimensionalMatching::new(1, vec![(0, 0, 0)]), + ] { + check_contract::<_, ThreePartition>(&source); + let path = ReductionPath { + steps: vec![ + step::(), + step::(), + step::(), + ], + }; + let predicted = ReductionGraph::new() + .compose_path_parameter_transform(&path) + .unwrap() + .unwrap() + .evaluate(&source.parameters()) + .unwrap(); + let intermediate = ReduceTo::::reduce_to(&source).unwrap(); + let target = ReduceTo::::reduce_to( + intermediate.target_problem(), + ) + .unwrap(); + assert!( + predicted.get("time_horizon").unwrap() + >= target + .target_problem() + .parameters() + .get("time_horizon") + .unwrap() + ); + } +} + +#[test] +fn hamiltonian_edge_bound_includes_normalization_and_fixed_outputs() { + use crate::models::Decision; + // Two 14-edge gadgets, one incident chain link, six selector links. + check_counts::<_, HamiltonianCircuit>( + &Decision::new( + MinimumVertexCover::new(SimpleGraph::path(3), vec![One; 3]), + 1, + ), + &[("num_edges", 35, 53)], + ); + for bound in [-1, 0, 3] { + check_contract::<_, HamiltonianCircuit>(&Decision::new( + MinimumVertexCover::new( + SimpleGraph::new(3, vec![(0, 0), (0, 1), (1, 0)]), + vec![One; 3], + ), + bound, + )); + } +} + #[test] fn integer_knapsack_and_open_shop_bit_predictions_reach_qubo() { use crate::models::{set::IntegerKnapsack, Decision}; @@ -97,8 +779,17 @@ fn partition_knapsack_qubo_predictions_and_solution_recovery() { fn subset_sum_lattice_qubo_predictions_and_solution_recovery() { use crate::models::{algebraic::ClosestVectorProblem, Decision}; for (sizes, target) in [(vec![1], 1), (vec![2], 1)] { + let source = SubsetSum::new(sizes.clone(), target); + // The carry lattices have unit selected determinants. Squared column + // norms (3), then (3,5), and squared target norm two bound widths by + // floor(sqrt(8)) and floor(sqrt(40)), respectively. + let (actual_bits, predicted_bits) = if sizes[0] == 1 { (2, 4) } else { (6, 14) }; + check_counts::<_, Decision>( + &source, + &[("coefficient_box_bits", actual_bits, predicted_bits)], + ); check_path( - SubsetSum::new(sizes, target), + source, ReductionPath { steps: vec![ step::(), @@ -131,7 +822,9 @@ fn factoring_circuit_sat_qubo_predictions_and_solution_recovery() { } } -fn check_contract, T: Problem>(source: &S) { +fn check_contract, T: Problem>( + source: &S, +) -> (ProblemParameters, ProblemParameters) { let target = source.reduce_to().unwrap(); let entry = crate::rules::registry::reduction_entries() .into_iter() @@ -151,7 +844,8 @@ fn check_contract, T: Problem>(source: &S) { ); let transform = contract.transform().unwrap(); let predicted = transform.evaluate(&source.parameters()).unwrap(); - for (field, actual) in target.target_problem().parameters().iter() { + let actual = target.target_problem().parameters(); + for (field, actual) in actual.iter() { let prediction = predicted.get(field).expect(field); match transform.relation(field).unwrap() { ParameterRelation::Exact => assert_eq!(prediction, actual, "{}: {field}", S::NAME), @@ -162,6 +856,7 @@ fn check_contract, T: Problem>(source: &S) { ), } } + (actual, predicted) } fn step() -> ReductionStep { diff --git a/src/unit_tests/models/algebraic/closest_vector_problem.rs b/src/unit_tests/models/algebraic/closest_vector_problem.rs index a4928991b..f65f002f3 100644 --- a/src/unit_tests/models/algebraic/closest_vector_problem.rs +++ b/src/unit_tests/models/algebraic/closest_vector_problem.rs @@ -2,6 +2,35 @@ use super::*; use crate::traits::Problem; use crate::types::Min; +#[test] +fn coefficient_bit_bounds_use_basis_geometry_without_solving() { + // Complementary norms are one and the selected determinant is one. + // An ambient residual squared of four allows width four, requiring three bits. + let embedded = ClosestVectorProblem::new(vec![vec![1, 0]], vec![0, 2]).unwrap(); + assert_eq!(embedded.parameters().get("coefficient_box_bits"), Some(3)); + // Full rank permits a rounded coefficient vector with squared error <=1/4; + // the integer error is zero even when the target magnitude is large. + let translated = ClosestVectorProblem::new(vec![vec![1]], vec![i64::MAX]).unwrap(); + assert_eq!(translated.parameters().get("coefficient_box_bits"), Some(0)); + // Nearly parallel columns have determinant one and complementary norms + // five and two. Squared error one bounds widths by four and two: five bits. + let skewed = ClosestVectorProblem::new(vec![vec![1, 1], vec![1, 2]], vec![1, 0]).unwrap(); + assert_eq!(skewed.parameters().get("coefficient_box_bits"), Some(5)); + let decoded: ClosestVectorProblem = + serde_json::from_str(&serde_json::to_string(&skewed).unwrap()).unwrap(); + assert_eq!(decoded.parameters(), skewed.parameters()); + // Row swaps and large cancelling products must preserve the determinant. + let m = i64::MAX; + let cancelled = + ClosestVectorProblem::new(vec![vec![m, m - 1], vec![m - 1, m - 2]], vec![1, 0]).unwrap(); + assert_eq!( + cancelled.parameters().get("coefficient_box_bits"), + Some(130) + ); + let swapped = ClosestVectorProblem::new(vec![vec![0, 2], vec![3, 0]], vec![0, 1]).unwrap(); + assert_eq!(swapped.parameters().get("coefficient_box_bits"), Some(1)); +} + #[test] fn test_cvp_constructs_integer_targets() { let integer = diff --git a/src/unit_tests/models/misc/rectilinear_picture_compression.rs b/src/unit_tests/models/misc/rectilinear_picture_compression.rs index a951f51d2..4093d8d85 100644 --- a/src/unit_tests/models/misc/rectilinear_picture_compression.rs +++ b/src/unit_tests/models/misc/rectilinear_picture_compression.rs @@ -3,6 +3,20 @@ use crate::solvers::BruteForce; use crate::solvers::BruteForceProblem as _; use crate::traits::Problem; +#[test] +fn rectangle_parameters_count_cached_incidence_including_overlaps() { + for (matrix, rectangles, area) in [ + (vec![vec![false; 2]; 2], 0, 0), + (vec![vec![true; 2]; 2], 1, 4), + (vec![vec![true, true], vec![true, false]], 2, 4), + (vec![vec![true, false, true]], 2, 2), + ] { + let source = RectilinearPictureCompression::new(matrix, 1); + assert_eq!(source.parameters().get("num_rectangles"), Some(rectangles)); + assert_eq!(source.parameters().get("total_rectangle_area"), Some(area)); + } +} + #[test] fn test_rectilinear_picture_compression_rejects_invalid_json_without_panicking() { for matrix in [ diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs index 5a65141ad..1e212c22f 100644 --- a/src/unit_tests/reduction_graph.rs +++ b/src/unit_tests/reduction_graph.rs @@ -1375,12 +1375,29 @@ fn numeric_magnitude_bits_cover_padding_and_empty_targets() { }) .unwrap(); let contract = entry.parameter_contract().unwrap(); + let expected_unavailable = if S::NAME == SubsetSum::NAME && T::NAME == Partition::NAME { + vec!["total_sum"] + } else { + vec![] + }; + assert_eq!( + contract + .unavailable() + .iter() + .map(|f| f.field) + .collect::>(), + expected_unavailable + ); let predicted = contract .transform() .unwrap() .evaluate(&source.parameters()) .unwrap(); for (field, actual) in reduction.target_problem().parameters().iter() { + if expected_unavailable.contains(&field) { + assert!(predicted.get(field).is_none()); + continue; + } assert!( predicted.get(field).unwrap() >= actual, "{} -> {}: {field}",