From 8523caabdbd8040f497b8a8e020cb3bd2fdc2e98 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Tue, 27 Oct 2026 12:12:22 -0700 Subject: [PATCH 01/12] Reject negative ConsecutiveOnesSubmatrix bounds at construction The bound K counts selected columns, but try_new accepted any negative value. Such an instance panicked in parameters(), whose bound must fit u64, and its ILP reduction cast the bound with `as usize`. Co-Authored-By: Claude Opus 5.5 --- src/models/algebraic/consecutive_ones_submatrix.rs | 6 +++--- .../models/algebraic/consecutive_ones_submatrix.rs | 9 +++++++++ 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/models/algebraic/consecutive_ones_submatrix.rs b/src/models/algebraic/consecutive_ones_submatrix.rs index bad2a8a4c..a1096a369 100644 --- a/src/models/algebraic/consecutive_ones_submatrix.rs +++ b/src/models/algebraic/consecutive_ones_submatrix.rs @@ -84,7 +84,7 @@ impl ConsecutiveOnesSubmatrix { /// /// # Panics /// - /// Panics if `bound > n`, or if rows have inconsistent lengths. + /// Panics if `bound` is negative or exceeds `n`, or if rows have inconsistent lengths. pub fn new(matrix: Vec>, bound: i64) -> Self { Self::try_new(matrix, bound).unwrap_or_else(|error| panic!("{error}")) } @@ -97,8 +97,8 @@ impl ConsecutiveOnesSubmatrix { if matrix.iter().any(|row| row.len() != n) { return Err("all matrix rows must have the same length".into()); } - if !(bound < 0 || usize::try_from(bound).is_ok_and(|bound| bound <= n)) { - return Err(format!("bound ({bound}) must be <= number of columns ({n})").into()); + if !usize::try_from(bound).is_ok_and(|bound| bound <= n) { + return Err(format!("bound ({bound}) must be in 0..={n}, the number of columns").into()); } Ok(Self { matrix, bound }) } diff --git a/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs b/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs index a0a0bf5d1..1f6d60fe7 100644 --- a/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs +++ b/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs @@ -241,3 +241,12 @@ fn json_rejects_invalid_instance() { ) .is_err()); } + +#[test] +fn json_rejects_negative_bound() { + // A column count is nonnegative; a negative bound would break the u64 parameter. + assert!(serde_json::from_value::( + serde_json::json!({"matrix":[[true]],"bound":-1}) + ) + .is_err()); +} From 3de4a67b531fdf2e663d10e5df1edb9928d5d8a2 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Tue, 27 Oct 2026 12:25:14 -0700 Subject: [PATCH 02/12] Declare exact parameter counts the constructions always produce The corpus measured 81 non-trivial upper-bound fields at exactly their prediction on every instance. Of those, 46 fields in 30 rules are exact by construction: every row family and variable block is emitted unconditionally, the source invariants (simple graphs, exactly-K clauses, n divisible by 3, 1 <= k <= n) rule out merged or dropped terms, and no early return builds a different target. The rest stay upper bounds: degenerate-input shortcuts, data-dependent zero coefficients or cancelled literals, and QUBO entries where penalty and objective terms can cancel. Co-Authored-By: Claude Opus 5.5 --- src/models/algebraic/consecutive_ones_submatrix.rs | 4 +++- src/rules/biconnectivityaugmentation_ilp.rs | 2 +- src/rules/clustering_ilp.rs | 8 ++++++-- src/rules/consecutiveblockminimization_ilp.rs | 8 ++++++-- src/rules/consecutiveonessubmatrix_ilp.rs | 8 ++++++-- src/rules/directedhamiltonianpath_ilp.rs | 8 ++++++-- src/rules/directedtwocommodityintegralflow_ilp.rs | 8 ++++++-- src/rules/flowshopscheduling_ilp.rs | 8 ++++++-- src/rules/hamiltoniancircuit_ilp.rs | 10 +++++++--- src/rules/isomorphicspanningtree_ilp.rs | 8 ++++++-- .../kclique_balancedcompletebipartitesubgraph.rs | 2 +- src/rules/kernel_ilp.rs | 2 +- .../ksatisfiability_decisionminimumvertexcover.rs | 5 +++-- src/rules/ksatisfiability_kclique.rs | 8 ++++++-- .../ksatisfiability_oneinthreesatisfiability.rs | 10 +++++++--- src/rules/ksatisfiability_subsetsum.rs | 8 ++++++-- src/rules/maximalis_ilp.rs | 4 ++-- src/rules/maximum2satisfiability_maxcut.rs | 8 ++++++-- src/rules/maximummatching_ilp.rs | 2 +- src/rules/minimumdominatingset_ilp.rs | 2 +- src/rules/minimumsummulticenter_ilp.rs | 8 ++++++-- src/rules/minimumvertexcover_ensemblecomputation.rs | 8 ++++++-- src/rules/numericalmatchingwithtargetsums_ilp.rs | 8 ++++++-- .../partitionintocliques_minimumcoveringbycliques.rs | 2 +- src/rules/partitionintopathsoflength2_ilp.rs | 12 ++++++++---- src/rules/partitionintoperfectmatchings_ilp.rs | 10 +++++++--- src/rules/shortestcommonsupersequence_ilp.rs | 8 ++++++-- src/rules/sparsematrixcompression_ilp.rs | 8 ++++++-- src/rules/strongconnectivityaugmentation_ilp.rs | 2 +- src/rules/subgraphisomorphism_ilp.rs | 8 ++++++-- src/rules/undirectedflowlowerbounds_ilp.rs | 8 ++++++-- src/unit_tests/symbolic_parameter_contracts.rs | 3 ++- 32 files changed, 148 insertions(+), 60 deletions(-) diff --git a/src/models/algebraic/consecutive_ones_submatrix.rs b/src/models/algebraic/consecutive_ones_submatrix.rs index a1096a369..2b9d2eb95 100644 --- a/src/models/algebraic/consecutive_ones_submatrix.rs +++ b/src/models/algebraic/consecutive_ones_submatrix.rs @@ -98,7 +98,9 @@ impl ConsecutiveOnesSubmatrix { return Err("all matrix rows must have the same length".into()); } if !usize::try_from(bound).is_ok_and(|bound| bound <= n) { - return Err(format!("bound ({bound}) must be in 0..={n}, the number of columns").into()); + return Err( + format!("bound ({bound}) must be in 0..={n}, the number of columns").into(), + ); } Ok(Self { matrix, bound }) } diff --git a/src/rules/biconnectivityaugmentation_ilp.rs b/src/rules/biconnectivityaugmentation_ilp.rs index f8bc8e07f..f15484f23 100644 --- a/src/rules/biconnectivityaugmentation_ilp.rs +++ b/src/rules/biconnectivityaugmentation_ilp.rs @@ -81,9 +81,9 @@ impl crate::rules::AggregateReductionResult for ReductionBiconnAugToILP {} #[reduction(transform = { exact { max_constraint_magnitude_bits = "max_numeric_magnitude_bits", + num_vars = "num_potential_edges + 2 * num_vertices * (num_vertices + 1) * (num_edges + num_potential_edges)", }, upper_bound { - num_vars = "num_potential_edges + 2 * num_vertices * (num_vertices + 1) * (num_edges + num_potential_edges)", num_constraints = "1 + num_vertices * (num_vertices + 1) * (2 * num_edges + 4 * num_potential_edges + num_vertices)", num_nonzeros = "num_potential_edges + num_vertices * (num_vertices + 1) * (4 * num_edges + 8 * num_potential_edges)", }, diff --git a/src/rules/clustering_ilp.rs b/src/rules/clustering_ilp.rs index ca6434296..d4eb7517a 100644 --- a/src/rules/clustering_ilp.rs +++ b/src/rules/clustering_ilp.rs @@ -49,11 +49,15 @@ impl ReductionResult for ReductionClusteringToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionClusteringToILP {} -#[reduction(transform = upper_bound { +#[reduction(transform = { + exact { + num_vars = "num_elements * num_clusters", + }, + upper_bound { max_constraint_magnitude_bits = "1", - num_vars = "num_elements * num_clusters", num_constraints = "num_elements + num_elements * (num_elements - 1) / 2 * num_clusters", num_nonzeros = "num_elements * num_clusters + num_elements * (num_elements - 1) * num_clusters", +}, })] impl ReduceTo> for Clustering { type Result = ReductionClusteringToILP; diff --git a/src/rules/consecutiveblockminimization_ilp.rs b/src/rules/consecutiveblockminimization_ilp.rs index 7ff7395b6..de13be9e8 100644 --- a/src/rules/consecutiveblockminimization_ilp.rs +++ b/src/rules/consecutiveblockminimization_ilp.rs @@ -43,12 +43,16 @@ impl ReductionResult for ReductionCBMToILP { impl crate::rules::AggregateReductionResult for ReductionCBMToILP {} #[reduction( - transform = upper_bound { - max_constraint_magnitude_bits = "num_rows * num_cols + 1", + transform = { + exact { num_vars = "num_cols * num_cols + num_rows * num_cols + num_rows * num_cols", + }, + upper_bound { + max_constraint_magnitude_bits = "num_rows * num_cols + 1", num_constraints = "num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1", num_nonzeros = "2 * num_cols^2 + num_rows * num_cols^2 + 5 * num_rows * num_cols", }, +}, )] impl ReduceTo> for ConsecutiveBlockMinimization { type Result = ReductionCBMToILP; diff --git a/src/rules/consecutiveonessubmatrix_ilp.rs b/src/rules/consecutiveonessubmatrix_ilp.rs index c3db9451a..e830eb04b 100644 --- a/src/rules/consecutiveonessubmatrix_ilp.rs +++ b/src/rules/consecutiveonessubmatrix_ilp.rs @@ -46,11 +46,15 @@ impl ReductionResult for ReductionCOSToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionCOSToILP {} -#[reduction(transform = upper_bound { +#[reduction(transform = { + exact { + num_vars = "num_cols + num_cols * bound + 5 * num_rows * bound", + }, + upper_bound { max_constraint_magnitude_bits = "bound + num_cols + 1", - num_vars = "num_cols + num_cols * bound + 5 * num_rows * bound", num_constraints = "2 + num_cols + bound + 3 * num_rows + 8 * num_rows * bound", num_nonzeros = "2 * num_cols + 2 * num_cols * bound + num_rows * num_cols * bound + 2 * num_rows * bound^2 + 21 * num_rows * bound", +}, })] impl ReduceTo> for ConsecutiveOnesSubmatrix { type Result = ReductionCOSToILP; diff --git a/src/rules/directedhamiltonianpath_ilp.rs b/src/rules/directedhamiltonianpath_ilp.rs index c5c821c84..e317af756 100644 --- a/src/rules/directedhamiltonianpath_ilp.rs +++ b/src/rules/directedhamiltonianpath_ilp.rs @@ -53,11 +53,15 @@ impl ReductionResult for ReductionDirectedHamiltonianPathToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionDirectedHamiltonianPathToILP {} -#[reduction(transform = upper_bound { +#[reduction(transform = { + exact { + num_vars = "num_vertices^2", + }, + upper_bound { max_constraint_magnitude_bits = "1", - num_vars = "num_vertices^2", num_constraints = "3 * num_vertices + num_vertices^3", num_nonzeros = "num_vertices^2 + 2 * num_vertices^3", +}, })] impl ReduceTo> for DirectedHamiltonianPath { type Result = ReductionDirectedHamiltonianPathToILP; diff --git a/src/rules/directedtwocommodityintegralflow_ilp.rs b/src/rules/directedtwocommodityintegralflow_ilp.rs index f08d07b2f..4e14d01ea 100644 --- a/src/rules/directedtwocommodityintegralflow_ilp.rs +++ b/src/rules/directedtwocommodityintegralflow_ilp.rs @@ -56,12 +56,16 @@ impl ReductionResult for ReductionD2CIFToILP { impl crate::rules::AggregateReductionResult for ReductionD2CIFToILP {} #[reduction( - transform = upper_bound { - max_constraint_magnitude_bits = "max_capacity * (num_arcs + 1) + 2", + transform = { + exact { num_vars = "2 * num_arcs", + }, + upper_bound { + max_constraint_magnitude_bits = "max_capacity * (num_arcs + 1) + 2", num_constraints = "num_arcs + 2 * num_vertices + 2", num_nonzeros = "(2 * num_arcs) * (num_arcs + 2 * num_vertices + 2)", }, +}, )] impl ReduceTo> for DirectedTwoCommodityIntegralFlow { type Result = ReductionD2CIFToILP; diff --git a/src/rules/flowshopscheduling_ilp.rs b/src/rules/flowshopscheduling_ilp.rs index 6845717cd..8d3cf124f 100644 --- a/src/rules/flowshopscheduling_ilp.rs +++ b/src/rules/flowshopscheduling_ilp.rs @@ -72,12 +72,16 @@ impl ReductionResult for ReductionFSSToILP { impl crate::rules::AggregateReductionResult for ReductionFSSToILP {} #[reduction( - transform = upper_bound { - max_constraint_magnitude_bits = "max_time_bits + 1", + transform = { + exact { num_vars = "num_jobs * (num_jobs - 1) / 2 + num_jobs * num_processors", + }, + upper_bound { + max_constraint_magnitude_bits = "max_time_bits + 1", num_constraints = "num_jobs * (num_jobs - 1) + num_jobs + num_jobs * (num_processors - 1) + num_jobs * (num_jobs - 1) * num_processors + num_jobs", num_nonzeros = "num_jobs * (num_jobs - 1) * (1 + 3 * num_processors) + 2 * num_jobs * num_processors", }, +}, )] impl ReduceTo> for FlowShopScheduling { type Result = ReductionFSSToILP; diff --git a/src/rules/hamiltoniancircuit_ilp.rs b/src/rules/hamiltoniancircuit_ilp.rs index c7b46ff5c..217a66313 100644 --- a/src/rules/hamiltoniancircuit_ilp.rs +++ b/src/rules/hamiltoniancircuit_ilp.rs @@ -39,11 +39,15 @@ impl ReductionResult for ReductionHamiltonianCircuitToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionHamiltonianCircuitToILP {} -#[crate::reduction(transform = upper_bound { - num_vars = "3 * num_edges", +#[crate::reduction(transform = { + exact { + num_vars = "3 * num_edges", + num_nonzeros = "10 * num_edges", + }, + upper_bound { num_constraints = "2 * num_vertices + 2 * num_edges + 1", - num_nonzeros = "10 * num_edges", max_constraint_magnitude_bits = "num_vertices + 2", +}, })] impl ReduceTo> for HamiltonianCircuit { type Result = ReductionHamiltonianCircuitToILP; diff --git a/src/rules/isomorphicspanningtree_ilp.rs b/src/rules/isomorphicspanningtree_ilp.rs index 6904c4be4..f78c0fb8d 100644 --- a/src/rules/isomorphicspanningtree_ilp.rs +++ b/src/rules/isomorphicspanningtree_ilp.rs @@ -45,11 +45,15 @@ 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 { +#[reduction(transform = { + exact { + num_vars = "num_vertices * num_vertices", + }, + upper_bound { max_constraint_magnitude_bits = "2", - num_vars = "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/kclique_balancedcompletebipartitesubgraph.rs b/src/rules/kclique_balancedcompletebipartitesubgraph.rs index b3cb09b81..d2b2d330e 100644 --- a/src/rules/kclique_balancedcompletebipartitesubgraph.rs +++ b/src/rules/kclique_balancedcompletebipartitesubgraph.rs @@ -56,7 +56,7 @@ impl ReductionResult for ReductionKCliqueToBCBS { #[crate::aggregate_reduction(identity)] impl crate::rules::AggregateReductionResult for ReductionKCliqueToBCBS {} -#[reduction(transform = upper_bound { +#[reduction(transform = exact { left_size = "num_vertices + k * (k - 1) / 2", right_size = "num_edges + num_vertices - k", k = "num_vertices + k * (k - 1) / 2 - k", diff --git a/src/rules/kernel_ilp.rs b/src/rules/kernel_ilp.rs index 95c986253..8363af39a 100644 --- a/src/rules/kernel_ilp.rs +++ b/src/rules/kernel_ilp.rs @@ -36,9 +36,9 @@ impl crate::rules::AggregateReductionResult for ReductionKernelToILP {} exact { num_vars = "num_vertices", num_constraints = "num_arcs + num_vertices", + num_nonzeros = "3 * num_arcs + num_vertices", }, upper_bound { - num_nonzeros = "3 * num_arcs + num_vertices", max_constraint_magnitude_bits = "2", }, })] diff --git a/src/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/rules/ksatisfiability_decisionminimumvertexcover.rs index 7d2019231..ceb43021d 100644 --- a/src/rules/ksatisfiability_decisionminimumvertexcover.rs +++ b/src/rules/ksatisfiability_decisionminimumvertexcover.rs @@ -69,8 +69,9 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToDecisionMVC {} #[reduction( transform = { - exact { num_vertices = "2 * num_vars + 3 * num_clauses" }, - upper_bound { num_edges = "num_vars + 6 * num_clauses" }, + exact { num_vertices = "2 * num_vars + 3 * num_clauses", + num_edges = "num_vars + 6 * num_clauses", + }, } )] impl ReduceTo>> for KSatisfiability { diff --git a/src/rules/ksatisfiability_kclique.rs b/src/rules/ksatisfiability_kclique.rs index 79dc24313..6e79a4c17 100644 --- a/src/rules/ksatisfiability_kclique.rs +++ b/src/rules/ksatisfiability_kclique.rs @@ -57,11 +57,15 @@ impl ReductionResult for Reduction3SATToKClique { impl crate::rules::AggregateReductionResult for Reduction3SATToKClique {} #[reduction( - transform = upper_bound { + transform = { + exact { num_vertices = "3 * num_clauses + 1", k = "num_clauses + 1", + }, + upper_bound { num_edges = "9 * num_clauses^2 + 3 * num_clauses", - } + }, +} )] impl ReduceTo> for KSatisfiability { type Result = Reduction3SATToKClique; diff --git a/src/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/rules/ksatisfiability_oneinthreesatisfiability.rs index 711f2f42c..e424fa988 100644 --- a/src/rules/ksatisfiability_oneinthreesatisfiability.rs +++ b/src/rules/ksatisfiability_oneinthreesatisfiability.rs @@ -49,10 +49,14 @@ impl ReductionResult for Reduction3SATToOneInThreeSAT { impl crate::rules::AggregateReductionResult for Reduction3SATToOneInThreeSAT {} #[reduction( - transform = upper_bound { - num_vars = "num_vars + 2 + 6 * num_clauses", + transform = { + exact { num_clauses = "1 + 5 * num_clauses", - })] + }, + upper_bound { + num_vars = "num_vars + 2 + 6 * num_clauses", + }, +})] impl ReduceTo for KSatisfiability { type Result = Reduction3SATToOneInThreeSAT; diff --git a/src/rules/ksatisfiability_subsetsum.rs b/src/rules/ksatisfiability_subsetsum.rs index 3efa0a862..0fd2cbaf7 100644 --- a/src/rules/ksatisfiability_subsetsum.rs +++ b/src/rules/ksatisfiability_subsetsum.rs @@ -74,9 +74,13 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToSubsetSum {} // Every integer has at most n+m decimal digits, and 10 < 2^4. The extra 1 // also covers the empty formula's zero target (whose magnitude parameter is 1). -#[reduction(transform = upper_bound { - num_elements = "2 * num_vars + 2 * num_clauses", +#[reduction(transform = { + exact { + num_elements = "2 * num_vars + 2 * num_clauses", + }, + upper_bound { max_numeric_magnitude_bits = "4 * (num_vars + num_clauses) + 1", +}, })] impl ReduceTo for KSatisfiability { type Result = Reduction3SATToSubsetSum; diff --git a/src/rules/maximalis_ilp.rs b/src/rules/maximalis_ilp.rs index 1f8ebb2fb..2e3bbb9b3 100644 --- a/src/rules/maximalis_ilp.rs +++ b/src/rules/maximalis_ilp.rs @@ -37,11 +37,11 @@ impl ReductionResult for ReductionMxISToILP { #[reduction(transform = { exact { num_vars = "num_vertices", + num_constraints = "num_edges + num_vertices", + num_nonzeros = "4 * num_edges + num_vertices", }, upper_bound { max_constraint_magnitude_bits = "2 * num_edges + 2", - num_constraints = "num_edges + num_vertices", - num_nonzeros = "4 * num_edges + num_vertices", }, })] impl ReduceTo> for MaximalIS { diff --git a/src/rules/maximum2satisfiability_maxcut.rs b/src/rules/maximum2satisfiability_maxcut.rs index e153b5d4f..1e1c24890 100644 --- a/src/rules/maximum2satisfiability_maxcut.rs +++ b/src/rules/maximum2satisfiability_maxcut.rs @@ -62,10 +62,14 @@ fn literal_polarity(lit: i64) -> i64 { } #[reduction( - transform = upper_bound { + transform = { + exact { num_vertices = "num_vars + 1", + }, + upper_bound { num_edges = "(num_vars + 1)^2", - } + }, +} )] impl ReduceTo> for Maximum2Satisfiability { type Result = ReductionMaximum2SatisfiabilityToMaxCut; diff --git a/src/rules/maximummatching_ilp.rs b/src/rules/maximummatching_ilp.rs index 42f1a3799..ab0f0a9f8 100644 --- a/src/rules/maximummatching_ilp.rs +++ b/src/rules/maximummatching_ilp.rs @@ -48,11 +48,11 @@ impl ReductionResult for ReductionMatchingToILP { #[reduction(transform = { exact { num_vars = "num_edges", + num_nonzeros = "2 * num_edges", }, upper_bound { max_constraint_magnitude_bits = "2", num_constraints = "num_vertices", - num_nonzeros = "2 * num_edges", }, })] impl ReduceTo> for MaximumMatching { diff --git a/src/rules/minimumdominatingset_ilp.rs b/src/rules/minimumdominatingset_ilp.rs index 7f3007d82..db2ea9980 100644 --- a/src/rules/minimumdominatingset_ilp.rs +++ b/src/rules/minimumdominatingset_ilp.rs @@ -52,10 +52,10 @@ impl ReductionResult for ReductionDSToILP { exact { num_vars = "num_vertices", num_constraints = "num_vertices", + num_nonzeros = "2 * num_edges + num_vertices", }, upper_bound { max_constraint_magnitude_bits = "2 * num_edges + 2", - num_nonzeros = "2 * num_edges + num_vertices", }, })] impl ReduceTo> for MinimumDominatingSet { diff --git a/src/rules/minimumsummulticenter_ilp.rs b/src/rules/minimumsummulticenter_ilp.rs index a714ec003..181b4805b 100644 --- a/src/rules/minimumsummulticenter_ilp.rs +++ b/src/rules/minimumsummulticenter_ilp.rs @@ -117,11 +117,15 @@ fn weighted_distances_msmc( dist } -#[reduction(transform = upper_bound { +#[reduction(transform = { + exact { + num_vars = "num_vertices + num_vertices^2", + }, + upper_bound { max_constraint_magnitude_bits = "num_vertices + 1", - num_vars = "num_vertices + num_vertices^2", num_constraints = "num_vertices^2 + 2 * num_vertices + 1", num_nonzeros = "3 * num_vertices^2 + num_vertices", +}, })] impl ReduceTo> for MinimumSumMulticenter { type Result = ReductionMSMCToILP; diff --git a/src/rules/minimumvertexcover_ensemblecomputation.rs b/src/rules/minimumvertexcover_ensemblecomputation.rs index 710badf1f..2d6b1df72 100644 --- a/src/rules/minimumvertexcover_ensemblecomputation.rs +++ b/src/rules/minimumvertexcover_ensemblecomputation.rs @@ -76,11 +76,15 @@ impl ReductionResult for ReductionVCToEC { } #[reduction( - transform = upper_bound { + transform = { + exact { universe_size = "num_vertices + 1", + }, + upper_bound { num_subsets = "num_edges", budget = "num_vertices + num_edges + 1", - } + }, +} )] impl ReduceTo for MinimumVertexCover { type Result = ReductionVCToEC; diff --git a/src/rules/numericalmatchingwithtargetsums_ilp.rs b/src/rules/numericalmatchingwithtargetsums_ilp.rs index 83a8b9df8..2b543ccad 100644 --- a/src/rules/numericalmatchingwithtargetsums_ilp.rs +++ b/src/rules/numericalmatchingwithtargetsums_ilp.rs @@ -70,11 +70,15 @@ impl ReductionResult for ReductionNMTSToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionNMTSToILP {} -#[reduction(transform = upper_bound { +#[reduction(transform = { + exact { + num_constraints = "3 * num_pairs", + }, + upper_bound { max_constraint_magnitude_bits = "1", num_vars = "num_pairs * num_pairs * num_pairs", - num_constraints = "3 * num_pairs", num_nonzeros = "3 * num_pairs * num_pairs * num_pairs", +}, })] impl ReduceTo> for NumericalMatchingWithTargetSums { type Result = ReductionNMTSToILP; diff --git a/src/rules/partitionintocliques_minimumcoveringbycliques.rs b/src/rules/partitionintocliques_minimumcoveringbycliques.rs index 1c4639752..d090e7173 100644 --- a/src/rules/partitionintocliques_minimumcoveringbycliques.rs +++ b/src/rules/partitionintocliques_minimumcoveringbycliques.rs @@ -208,7 +208,7 @@ impl crate::rules::AggregateReductionResult } #[reduction( - transform = upper_bound { + transform = exact { num_vertices = "2 * num_vertices + 4 * num_edges + 4", num_edges = "(num_vertices + 2 * num_edges)^2 + 4 * num_vertices + 14 * num_edges + 2", } diff --git a/src/rules/partitionintopathsoflength2_ilp.rs b/src/rules/partitionintopathsoflength2_ilp.rs index 8477633c7..fabf2770a 100644 --- a/src/rules/partitionintopathsoflength2_ilp.rs +++ b/src/rules/partitionintopathsoflength2_ilp.rs @@ -69,11 +69,15 @@ 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 { +#[reduction(transform = { + exact { + 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", + }, + upper_bound { max_constraint_magnitude_bits = "2", - 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/partitionintoperfectmatchings_ilp.rs b/src/rules/partitionintoperfectmatchings_ilp.rs index 95add09a6..5e8468173 100644 --- a/src/rules/partitionintoperfectmatchings_ilp.rs +++ b/src/rules/partitionintoperfectmatchings_ilp.rs @@ -27,11 +27,15 @@ impl ReductionResult for ReductionPartitionIntoPerfectMatchingsToILP { } #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionPartitionIntoPerfectMatchingsToILP {} -#[crate::reduction(transform = upper_bound { - num_vars = "num_vertices + 2 * num_edges", - num_constraints = "num_vertices + 4 * num_edges", +#[crate::reduction(transform = { + exact { + num_vars = "num_vertices + 2 * num_edges", + num_constraints = "num_vertices + 4 * num_edges", + }, + upper_bound { num_nonzeros = "16 * num_edges", max_constraint_magnitude_bits = "num_matchings", +}, })] impl ReduceTo> for PartitionIntoPerfectMatchings { type Result = ReductionPartitionIntoPerfectMatchingsToILP; diff --git a/src/rules/shortestcommonsupersequence_ilp.rs b/src/rules/shortestcommonsupersequence_ilp.rs index 636d06962..ab57c23af 100644 --- a/src/rules/shortestcommonsupersequence_ilp.rs +++ b/src/rules/shortestcommonsupersequence_ilp.rs @@ -49,11 +49,15 @@ impl ReductionResult for ReductionSCSToILP { // 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 { +#[reduction(transform = { + exact { + num_vars = "max_length * (alphabet_size + 1) + total_length * max_length", + }, + upper_bound { 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 + 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 6156f5e2c..f4f368713 100644 --- a/src/rules/sparsematrixcompression_ilp.rs +++ b/src/rules/sparsematrixcompression_ilp.rs @@ -47,11 +47,15 @@ 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 { +#[reduction(transform = { + exact { + num_vars = "num_rows * bound_k", + }, + upper_bound { max_constraint_magnitude_bits = "1", - num_vars = "num_rows * 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/strongconnectivityaugmentation_ilp.rs b/src/rules/strongconnectivityaugmentation_ilp.rs index 233a99613..af2ecb5d8 100644 --- a/src/rules/strongconnectivityaugmentation_ilp.rs +++ b/src/rules/strongconnectivityaugmentation_ilp.rs @@ -50,9 +50,9 @@ impl crate::rules::AggregateReductionResult for ReductionSCAToILP {} #[reduction(transform = { exact { max_constraint_magnitude_bits = "max_numeric_magnitude_bits", + num_vars = "num_potential_arcs + 2 * num_vertices * (num_arcs + num_potential_arcs)", }, upper_bound { - num_vars = "num_potential_arcs + 2 * num_vertices * (num_arcs + num_potential_arcs)", num_constraints = "1 + num_potential_arcs + 2 * num_arcs + 2 * num_vertices * num_potential_arcs + 2 * num_vertices * num_vertices", num_nonzeros = "2 * num_potential_arcs + num_vertices * (4 * num_arcs + 8 * num_potential_arcs)", }, diff --git a/src/rules/subgraphisomorphism_ilp.rs b/src/rules/subgraphisomorphism_ilp.rs index dccbb54c4..e664e7bf9 100644 --- a/src/rules/subgraphisomorphism_ilp.rs +++ b/src/rules/subgraphisomorphism_ilp.rs @@ -57,11 +57,15 @@ impl ReductionResult for ReductionSubIsoToILP { #[crate::aggregate_reduction(ilp_feasibility)] impl crate::rules::AggregateReductionResult for ReductionSubIsoToILP {} -#[reduction(transform = upper_bound { +#[reduction(transform = { + exact { + num_vars = "num_pattern_vertices * num_host_vertices", + }, + upper_bound { max_constraint_magnitude_bits = "2", - num_vars = "num_pattern_vertices * num_host_vertices", num_constraints = "num_pattern_vertices + num_host_vertices + num_pattern_edges * num_host_vertices^2", num_nonzeros = "2 * num_pattern_vertices * num_host_vertices + 2 * num_pattern_edges * num_host_vertices^2", +}, })] impl ReduceTo> for SubgraphIsomorphism { type Result = ReductionSubIsoToILP; diff --git a/src/rules/undirectedflowlowerbounds_ilp.rs b/src/rules/undirectedflowlowerbounds_ilp.rs index 19ad6e55a..a70af3bcd 100644 --- a/src/rules/undirectedflowlowerbounds_ilp.rs +++ b/src/rules/undirectedflowlowerbounds_ilp.rs @@ -80,12 +80,16 @@ impl ReductionResult for ReductionUFLBToILP { impl crate::rules::AggregateReductionResult for ReductionUFLBToILP {} #[reduction( - transform = upper_bound { - max_constraint_magnitude_bits = "max_capacity_bits + num_edges + 1", + transform = { + exact { num_vars = "3 * num_edges", + }, + upper_bound { + max_constraint_magnitude_bits = "max_capacity_bits + num_edges + 1", num_constraints = "5 * num_edges + num_vertices + 1", num_nonzeros = "13 * num_edges", }, +}, )] impl ReduceTo> for UndirectedFlowLowerBounds { type Result = ReductionUFLBToILP; diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs index a7e6bfb34..8ae246250 100644 --- a/src/unit_tests/symbolic_parameter_contracts.rs +++ b/src/unit_tests/symbolic_parameter_contracts.rs @@ -587,10 +587,11 @@ fn missing_structural_bounds_cover_sparse_and_normalized_instances() { SimpleGraph::path(3), SimpleGraph::complete(3), ] { + // SimpleGraph rejects repeated edges, so the bipartite side sizes are exact. check_reduced_parameters::<_, BalancedCompleteBipartiteSubgraph>( KClique::new(graph, 2), &["num_vertices"], - upper, + ParameterRelation::Exact, ); } } From b8867cfb63c843f641162ac31c787822f583bc9e Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Tue, 27 Oct 2026 12:34:55 -0700 Subject: [PATCH 03/12] Keep 3-SAT literal-dependent counts as upper bounds KSatisfiability::new_allow_less admits clauses with fewer than three literals, so 3SAT -> KClique num_vertices and 3SAT -> DecisionMVC num_edges shrink below their formulas. Return both to upper_bound, pin the relations with short-clause instances, and lay out the transform declarations by nesting depth. Co-Authored-By: Claude Opus 5.5 --- src/rules/clustering_ilp.rs | 8 ++-- src/rules/consecutiveblockminimization_ilp.rs | 14 +++---- src/rules/consecutiveonessubmatrix_ilp.rs | 8 ++-- src/rules/directedhamiltonianpath_ilp.rs | 8 ++-- .../directedtwocommodityintegralflow_ilp.rs | 14 +++---- src/rules/flowshopscheduling_ilp.rs | 14 +++---- src/rules/hamiltoniancircuit_ilp.rs | 6 +-- src/rules/isomorphicspanningtree_ilp.rs | 8 ++-- ...tisfiability_decisionminimumvertexcover.rs | 6 +-- src/rules/ksatisfiability_kclique.rs | 15 ++++---- ...satisfiability_oneinthreesatisfiability.rs | 10 ++--- src/rules/ksatisfiability_subsetsum.rs | 4 +- src/rules/maximum2satisfiability_maxcut.rs | 12 +++--- src/rules/minimumsummulticenter_ilp.rs | 8 ++-- .../minimumvertexcover_ensemblecomputation.rs | 14 +++---- .../numericalmatchingwithtargetsums_ilp.rs | 8 ++-- src/rules/partitionintopathsoflength2_ilp.rs | 4 +- .../partitionintoperfectmatchings_ilp.rs | 6 +-- src/rules/shortestcommonsupersequence_ilp.rs | 8 ++-- src/rules/sparsematrixcompression_ilp.rs | 8 ++-- src/rules/subgraphisomorphism_ilp.rs | 8 ++-- src/rules/undirectedflowlowerbounds_ilp.rs | 14 +++---- .../symbolic_parameter_contracts.rs | 38 +++++++++++++++++++ 23 files changed, 140 insertions(+), 103 deletions(-) diff --git a/src/rules/clustering_ilp.rs b/src/rules/clustering_ilp.rs index d4eb7517a..69bbb04af 100644 --- a/src/rules/clustering_ilp.rs +++ b/src/rules/clustering_ilp.rs @@ -54,10 +54,10 @@ impl crate::rules::AggregateReductionResult for ReductionClusteringToILP {} num_vars = "num_elements * num_clusters", }, upper_bound { - max_constraint_magnitude_bits = "1", - num_constraints = "num_elements + num_elements * (num_elements - 1) / 2 * num_clusters", - num_nonzeros = "num_elements * num_clusters + num_elements * (num_elements - 1) * num_clusters", -}, + max_constraint_magnitude_bits = "1", + num_constraints = "num_elements + num_elements * (num_elements - 1) / 2 * num_clusters", + num_nonzeros = "num_elements * num_clusters + num_elements * (num_elements - 1) * num_clusters", + }, })] impl ReduceTo> for Clustering { type Result = ReductionClusteringToILP; diff --git a/src/rules/consecutiveblockminimization_ilp.rs b/src/rules/consecutiveblockminimization_ilp.rs index de13be9e8..8ed091c3d 100644 --- a/src/rules/consecutiveblockminimization_ilp.rs +++ b/src/rules/consecutiveblockminimization_ilp.rs @@ -45,14 +45,14 @@ impl crate::rules::AggregateReductionResult for ReductionCBMToILP {} #[reduction( transform = { exact { - num_vars = "num_cols * num_cols + num_rows * num_cols + num_rows * num_cols", - }, - upper_bound { - max_constraint_magnitude_bits = "num_rows * num_cols + 1", - num_constraints = "num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1", - num_nonzeros = "2 * num_cols^2 + num_rows * num_cols^2 + 5 * num_rows * num_cols", + num_vars = "num_cols * num_cols + num_rows * num_cols + num_rows * num_cols", + }, + upper_bound { + max_constraint_magnitude_bits = "num_rows * num_cols + 1", + num_constraints = "num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1", + num_nonzeros = "2 * num_cols^2 + num_rows * num_cols^2 + 5 * num_rows * num_cols", + }, }, -}, )] impl ReduceTo> for ConsecutiveBlockMinimization { type Result = ReductionCBMToILP; diff --git a/src/rules/consecutiveonessubmatrix_ilp.rs b/src/rules/consecutiveonessubmatrix_ilp.rs index e830eb04b..41ba6339a 100644 --- a/src/rules/consecutiveonessubmatrix_ilp.rs +++ b/src/rules/consecutiveonessubmatrix_ilp.rs @@ -51,10 +51,10 @@ impl crate::rules::AggregateReductionResult for ReductionCOSToILP {} num_vars = "num_cols + num_cols * bound + 5 * num_rows * bound", }, upper_bound { - max_constraint_magnitude_bits = "bound + num_cols + 1", - num_constraints = "2 + num_cols + bound + 3 * num_rows + 8 * num_rows * bound", - num_nonzeros = "2 * num_cols + 2 * num_cols * bound + num_rows * num_cols * bound + 2 * num_rows * bound^2 + 21 * num_rows * bound", -}, + max_constraint_magnitude_bits = "bound + num_cols + 1", + num_constraints = "2 + num_cols + bound + 3 * num_rows + 8 * num_rows * bound", + num_nonzeros = "2 * num_cols + 2 * num_cols * bound + num_rows * num_cols * bound + 2 * num_rows * bound^2 + 21 * num_rows * bound", + }, })] impl ReduceTo> for ConsecutiveOnesSubmatrix { type Result = ReductionCOSToILP; diff --git a/src/rules/directedhamiltonianpath_ilp.rs b/src/rules/directedhamiltonianpath_ilp.rs index e317af756..133efcf35 100644 --- a/src/rules/directedhamiltonianpath_ilp.rs +++ b/src/rules/directedhamiltonianpath_ilp.rs @@ -58,10 +58,10 @@ impl crate::rules::AggregateReductionResult for ReductionDirectedHamiltonianPath num_vars = "num_vertices^2", }, upper_bound { - max_constraint_magnitude_bits = "1", - num_constraints = "3 * num_vertices + num_vertices^3", - num_nonzeros = "num_vertices^2 + 2 * num_vertices^3", -}, + max_constraint_magnitude_bits = "1", + num_constraints = "3 * num_vertices + num_vertices^3", + num_nonzeros = "num_vertices^2 + 2 * num_vertices^3", + }, })] impl ReduceTo> for DirectedHamiltonianPath { type Result = ReductionDirectedHamiltonianPathToILP; diff --git a/src/rules/directedtwocommodityintegralflow_ilp.rs b/src/rules/directedtwocommodityintegralflow_ilp.rs index 4e14d01ea..edf1a5c29 100644 --- a/src/rules/directedtwocommodityintegralflow_ilp.rs +++ b/src/rules/directedtwocommodityintegralflow_ilp.rs @@ -58,14 +58,14 @@ impl crate::rules::AggregateReductionResult for ReductionD2CIFToILP {} #[reduction( transform = { exact { - num_vars = "2 * num_arcs", - }, - upper_bound { - max_constraint_magnitude_bits = "max_capacity * (num_arcs + 1) + 2", - num_constraints = "num_arcs + 2 * num_vertices + 2", - num_nonzeros = "(2 * num_arcs) * (num_arcs + 2 * num_vertices + 2)", + num_vars = "2 * num_arcs", + }, + upper_bound { + max_constraint_magnitude_bits = "max_capacity * (num_arcs + 1) + 2", + num_constraints = "num_arcs + 2 * num_vertices + 2", + num_nonzeros = "(2 * num_arcs) * (num_arcs + 2 * num_vertices + 2)", + }, }, -}, )] impl ReduceTo> for DirectedTwoCommodityIntegralFlow { type Result = ReductionD2CIFToILP; diff --git a/src/rules/flowshopscheduling_ilp.rs b/src/rules/flowshopscheduling_ilp.rs index 8d3cf124f..2a85d956a 100644 --- a/src/rules/flowshopscheduling_ilp.rs +++ b/src/rules/flowshopscheduling_ilp.rs @@ -74,14 +74,14 @@ impl crate::rules::AggregateReductionResult for ReductionFSSToILP {} #[reduction( transform = { exact { - num_vars = "num_jobs * (num_jobs - 1) / 2 + num_jobs * num_processors", - }, - upper_bound { - max_constraint_magnitude_bits = "max_time_bits + 1", - num_constraints = "num_jobs * (num_jobs - 1) + num_jobs + num_jobs * (num_processors - 1) + num_jobs * (num_jobs - 1) * num_processors + num_jobs", - num_nonzeros = "num_jobs * (num_jobs - 1) * (1 + 3 * num_processors) + 2 * num_jobs * num_processors", + num_vars = "num_jobs * (num_jobs - 1) / 2 + num_jobs * num_processors", + }, + upper_bound { + max_constraint_magnitude_bits = "max_time_bits + 1", + num_constraints = "num_jobs * (num_jobs - 1) + num_jobs + num_jobs * (num_processors - 1) + num_jobs * (num_jobs - 1) * num_processors + num_jobs", + num_nonzeros = "num_jobs * (num_jobs - 1) * (1 + 3 * num_processors) + 2 * num_jobs * num_processors", + }, }, -}, )] impl ReduceTo> for FlowShopScheduling { type Result = ReductionFSSToILP; diff --git a/src/rules/hamiltoniancircuit_ilp.rs b/src/rules/hamiltoniancircuit_ilp.rs index 217a66313..013e42d60 100644 --- a/src/rules/hamiltoniancircuit_ilp.rs +++ b/src/rules/hamiltoniancircuit_ilp.rs @@ -45,9 +45,9 @@ impl crate::rules::AggregateReductionResult for ReductionHamiltonianCircuitToILP num_nonzeros = "10 * num_edges", }, upper_bound { - num_constraints = "2 * num_vertices + 2 * num_edges + 1", - max_constraint_magnitude_bits = "num_vertices + 2", -}, + num_constraints = "2 * num_vertices + 2 * num_edges + 1", + max_constraint_magnitude_bits = "num_vertices + 2", + }, })] impl ReduceTo> for HamiltonianCircuit { type Result = ReductionHamiltonianCircuitToILP; diff --git a/src/rules/isomorphicspanningtree_ilp.rs b/src/rules/isomorphicspanningtree_ilp.rs index f78c0fb8d..74e22a5c0 100644 --- a/src/rules/isomorphicspanningtree_ilp.rs +++ b/src/rules/isomorphicspanningtree_ilp.rs @@ -50,10 +50,10 @@ impl crate::rules::AggregateReductionResult for ReductionISTToILP {} num_vars = "num_vertices * num_vertices", }, upper_bound { - max_constraint_magnitude_bits = "2", - num_constraints = "2 * num_vertices + num_vertices * (num_vertices - 1)^2", - num_nonzeros = "2 * num_vertices^2 + 2 * num_vertices * (num_vertices - 1)^2", -}, + max_constraint_magnitude_bits = "2", + 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_decisionminimumvertexcover.rs b/src/rules/ksatisfiability_decisionminimumvertexcover.rs index ceb43021d..6221cde56 100644 --- a/src/rules/ksatisfiability_decisionminimumvertexcover.rs +++ b/src/rules/ksatisfiability_decisionminimumvertexcover.rs @@ -69,9 +69,9 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToDecisionMVC {} #[reduction( transform = { - exact { num_vertices = "2 * num_vars + 3 * num_clauses", - num_edges = "num_vars + 6 * num_clauses", - }, + exact { num_vertices = "2 * num_vars + 3 * num_clauses", }, + // A clause with fewer than three literals links fewer triangle corners. + upper_bound { num_edges = "num_vars + 6 * num_clauses", }, } )] impl ReduceTo>> for KSatisfiability { diff --git a/src/rules/ksatisfiability_kclique.rs b/src/rules/ksatisfiability_kclique.rs index 6e79a4c17..ac3f830c1 100644 --- a/src/rules/ksatisfiability_kclique.rs +++ b/src/rules/ksatisfiability_kclique.rs @@ -58,14 +58,13 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToKClique {} #[reduction( transform = { - exact { - num_vertices = "3 * num_clauses + 1", - k = "num_clauses + 1", - }, - upper_bound { - num_edges = "9 * num_clauses^2 + 3 * num_clauses", - }, -} + exact { k = "num_clauses + 1", }, + // Clauses built with `new_allow_less` may have fewer than three literals. + upper_bound { + num_vertices = "3 * num_clauses + 1", + num_edges = "9 * num_clauses^2 + 3 * num_clauses", + }, + } )] impl ReduceTo> for KSatisfiability { type Result = Reduction3SATToKClique; diff --git a/src/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/rules/ksatisfiability_oneinthreesatisfiability.rs index e424fa988..f86ad1ac8 100644 --- a/src/rules/ksatisfiability_oneinthreesatisfiability.rs +++ b/src/rules/ksatisfiability_oneinthreesatisfiability.rs @@ -51,11 +51,11 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToOneInThreeSAT {} #[reduction( transform = { exact { - num_clauses = "1 + 5 * num_clauses", - }, - upper_bound { - num_vars = "num_vars + 2 + 6 * num_clauses", - }, + num_clauses = "1 + 5 * num_clauses", + }, + upper_bound { + num_vars = "num_vars + 2 + 6 * num_clauses", + }, })] impl ReduceTo for KSatisfiability { type Result = Reduction3SATToOneInThreeSAT; diff --git a/src/rules/ksatisfiability_subsetsum.rs b/src/rules/ksatisfiability_subsetsum.rs index 0fd2cbaf7..78f420ef9 100644 --- a/src/rules/ksatisfiability_subsetsum.rs +++ b/src/rules/ksatisfiability_subsetsum.rs @@ -79,8 +79,8 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToSubsetSum {} num_elements = "2 * num_vars + 2 * num_clauses", }, upper_bound { - max_numeric_magnitude_bits = "4 * (num_vars + num_clauses) + 1", -}, + max_numeric_magnitude_bits = "4 * (num_vars + num_clauses) + 1", + }, })] impl ReduceTo for KSatisfiability { type Result = Reduction3SATToSubsetSum; diff --git a/src/rules/maximum2satisfiability_maxcut.rs b/src/rules/maximum2satisfiability_maxcut.rs index 1e1c24890..f2340a3d4 100644 --- a/src/rules/maximum2satisfiability_maxcut.rs +++ b/src/rules/maximum2satisfiability_maxcut.rs @@ -64,12 +64,12 @@ fn literal_polarity(lit: i64) -> i64 { #[reduction( transform = { exact { - num_vertices = "num_vars + 1", - }, - upper_bound { - num_edges = "(num_vars + 1)^2", - }, -} + num_vertices = "num_vars + 1", + }, + upper_bound { + num_edges = "(num_vars + 1)^2", + }, + } )] impl ReduceTo> for Maximum2Satisfiability { type Result = ReductionMaximum2SatisfiabilityToMaxCut; diff --git a/src/rules/minimumsummulticenter_ilp.rs b/src/rules/minimumsummulticenter_ilp.rs index 181b4805b..2b131677d 100644 --- a/src/rules/minimumsummulticenter_ilp.rs +++ b/src/rules/minimumsummulticenter_ilp.rs @@ -122,10 +122,10 @@ fn weighted_distances_msmc( num_vars = "num_vertices + num_vertices^2", }, upper_bound { - max_constraint_magnitude_bits = "num_vertices + 1", - num_constraints = "num_vertices^2 + 2 * num_vertices + 1", - num_nonzeros = "3 * num_vertices^2 + num_vertices", -}, + max_constraint_magnitude_bits = "num_vertices + 1", + num_constraints = "num_vertices^2 + 2 * num_vertices + 1", + num_nonzeros = "3 * num_vertices^2 + num_vertices", + }, })] impl ReduceTo> for MinimumSumMulticenter { type Result = ReductionMSMCToILP; diff --git a/src/rules/minimumvertexcover_ensemblecomputation.rs b/src/rules/minimumvertexcover_ensemblecomputation.rs index 2d6b1df72..a6702de2b 100644 --- a/src/rules/minimumvertexcover_ensemblecomputation.rs +++ b/src/rules/minimumvertexcover_ensemblecomputation.rs @@ -78,13 +78,13 @@ impl ReductionResult for ReductionVCToEC { #[reduction( transform = { exact { - universe_size = "num_vertices + 1", - }, - upper_bound { - num_subsets = "num_edges", - budget = "num_vertices + num_edges + 1", - }, -} + universe_size = "num_vertices + 1", + }, + upper_bound { + num_subsets = "num_edges", + budget = "num_vertices + num_edges + 1", + }, + } )] impl ReduceTo for MinimumVertexCover { type Result = ReductionVCToEC; diff --git a/src/rules/numericalmatchingwithtargetsums_ilp.rs b/src/rules/numericalmatchingwithtargetsums_ilp.rs index 2b543ccad..45cff4eb0 100644 --- a/src/rules/numericalmatchingwithtargetsums_ilp.rs +++ b/src/rules/numericalmatchingwithtargetsums_ilp.rs @@ -75,10 +75,10 @@ impl crate::rules::AggregateReductionResult for ReductionNMTSToILP {} num_constraints = "3 * num_pairs", }, upper_bound { - max_constraint_magnitude_bits = "1", - num_vars = "num_pairs * num_pairs * num_pairs", - num_nonzeros = "3 * num_pairs * num_pairs * num_pairs", -}, + max_constraint_magnitude_bits = "1", + num_vars = "num_pairs * num_pairs * num_pairs", + num_nonzeros = "3 * num_pairs * num_pairs * num_pairs", + }, })] impl ReduceTo> for NumericalMatchingWithTargetSums { type Result = ReductionNMTSToILP; diff --git a/src/rules/partitionintopathsoflength2_ilp.rs b/src/rules/partitionintopathsoflength2_ilp.rs index fabf2770a..041374742 100644 --- a/src/rules/partitionintopathsoflength2_ilp.rs +++ b/src/rules/partitionintopathsoflength2_ilp.rs @@ -76,8 +76,8 @@ impl crate::rules::AggregateReductionResult for ReductionPIPL2ToILP {} num_nonzeros = "(2 * num_vertices^2 + 8 * num_edges * num_vertices) / 3", }, upper_bound { - max_constraint_magnitude_bits = "2", -}, + max_constraint_magnitude_bits = "2", + }, })] impl ReduceTo> for PartitionIntoPathsOfLength2 { type Result = ReductionPIPL2ToILP; diff --git a/src/rules/partitionintoperfectmatchings_ilp.rs b/src/rules/partitionintoperfectmatchings_ilp.rs index 5e8468173..80e09cb58 100644 --- a/src/rules/partitionintoperfectmatchings_ilp.rs +++ b/src/rules/partitionintoperfectmatchings_ilp.rs @@ -33,9 +33,9 @@ impl crate::rules::AggregateReductionResult for ReductionPartitionIntoPerfectMat num_constraints = "num_vertices + 4 * num_edges", }, upper_bound { - num_nonzeros = "16 * num_edges", - max_constraint_magnitude_bits = "num_matchings", -}, + num_nonzeros = "16 * num_edges", + max_constraint_magnitude_bits = "num_matchings", + }, })] impl ReduceTo> for PartitionIntoPerfectMatchings { type Result = ReductionPartitionIntoPerfectMatchingsToILP; diff --git a/src/rules/shortestcommonsupersequence_ilp.rs b/src/rules/shortestcommonsupersequence_ilp.rs index ab57c23af..9dbe64439 100644 --- a/src/rules/shortestcommonsupersequence_ilp.rs +++ b/src/rules/shortestcommonsupersequence_ilp.rs @@ -54,10 +54,10 @@ impl ReductionResult for ReductionSCSToILP { num_vars = "max_length * (alphabet_size + 1) + total_length * max_length", }, upper_bound { - max_constraint_magnitude_bits = "max_length / 2 + 1", - num_constraints = "max_length + total_length + total_length * max_length + total_length + max_length", - num_nonzeros = "max_length * (alphabet_size + 3) + 5 * total_length * max_length", -}, + max_constraint_magnitude_bits = "max_length / 2 + 1", + num_constraints = "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 f4f368713..fcdc44d46 100644 --- a/src/rules/sparsematrixcompression_ilp.rs +++ b/src/rules/sparsematrixcompression_ilp.rs @@ -52,10 +52,10 @@ impl crate::rules::AggregateReductionResult for ReductionSMCToILP {} num_vars = "num_rows * bound_k", }, upper_bound { - max_constraint_magnitude_bits = "1", - 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", -}, + max_constraint_magnitude_bits = "1", + 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/subgraphisomorphism_ilp.rs b/src/rules/subgraphisomorphism_ilp.rs index e664e7bf9..e7252e364 100644 --- a/src/rules/subgraphisomorphism_ilp.rs +++ b/src/rules/subgraphisomorphism_ilp.rs @@ -62,10 +62,10 @@ impl crate::rules::AggregateReductionResult for ReductionSubIsoToILP {} num_vars = "num_pattern_vertices * num_host_vertices", }, upper_bound { - max_constraint_magnitude_bits = "2", - num_constraints = "num_pattern_vertices + num_host_vertices + num_pattern_edges * num_host_vertices^2", - num_nonzeros = "2 * num_pattern_vertices * num_host_vertices + 2 * num_pattern_edges * num_host_vertices^2", -}, + max_constraint_magnitude_bits = "2", + num_constraints = "num_pattern_vertices + num_host_vertices + num_pattern_edges * num_host_vertices^2", + num_nonzeros = "2 * num_pattern_vertices * num_host_vertices + 2 * num_pattern_edges * num_host_vertices^2", + }, })] impl ReduceTo> for SubgraphIsomorphism { type Result = ReductionSubIsoToILP; diff --git a/src/rules/undirectedflowlowerbounds_ilp.rs b/src/rules/undirectedflowlowerbounds_ilp.rs index a70af3bcd..69bcede2a 100644 --- a/src/rules/undirectedflowlowerbounds_ilp.rs +++ b/src/rules/undirectedflowlowerbounds_ilp.rs @@ -82,14 +82,14 @@ impl crate::rules::AggregateReductionResult for ReductionUFLBToILP {} #[reduction( transform = { exact { - num_vars = "3 * num_edges", - }, - upper_bound { - max_constraint_magnitude_bits = "max_capacity_bits + num_edges + 1", - num_constraints = "5 * num_edges + num_vertices + 1", - num_nonzeros = "13 * num_edges", + num_vars = "3 * num_edges", + }, + upper_bound { + max_constraint_magnitude_bits = "max_capacity_bits + num_edges + 1", + num_constraints = "5 * num_edges + num_vertices + 1", + num_nonzeros = "13 * num_edges", + }, }, -}, )] impl ReduceTo> for UndirectedFlowLowerBounds { type Result = ReductionUFLBToILP; diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs index 8ae246250..6e864147f 100644 --- a/src/unit_tests/symbolic_parameter_contracts.rs +++ b/src/unit_tests/symbolic_parameter_contracts.rs @@ -933,3 +933,41 @@ fn vertex_cover_lcs_transition_bounds_cover_empty_strings() { ); } } + +#[test] +fn three_sat_contracts_cover_short_clauses() { + use crate::models::decision::Decision; + use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability}; + use crate::models::graph::{KClique, MinimumVertexCover}; + use crate::models::misc::SubsetSum; + use crate::types::One; + use crate::variant::K3; + // `new_allow_less` admits clauses with fewer than three literals, so + // counts that grow with each literal are only upper bounds. + let upper = ParameterRelation::UpperBound; + let exact = ParameterRelation::Exact; + for clauses in [ + vec![CNFClause::new(vec![1])], + vec![CNFClause::new(vec![])], + vec![CNFClause::new(vec![1, -2]), CNFClause::new(vec![2])], + ] { + let source = KSatisfiability::::new_allow_less(2, clauses); + check_reduced_parameters::<_, KClique>( + source.clone(), + &["num_vertices"], + upper, + ); + check_reduced_parameters::<_, KClique>(source.clone(), &["k"], exact); + check_reduced_parameters::<_, Decision>>( + source.clone(), + &["num_edges"], + upper, + ); + check_reduced_parameters::<_, OneInThreeSatisfiability>( + source.clone(), + &["num_clauses"], + exact, + ); + check_reduced_parameters::<_, SubsetSum>(source, &["num_elements"], exact); + } +} From 0318bfdf9e6059290a5b3572f3ee6d6c20168030 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 28 Oct 2026 08:21:32 -0700 Subject: [PATCH 04/12] Test exact construction counts on degenerate graphs The exact claims for HamiltonianCircuit, MaximalIS, MinimumDominatingSet, MaximumMatching, Kernel, PartitionIntoPathsOfLength2, PartitionIntoPerfectMatchings and PartitionIntoCliques were checked only on canonical examples. Pin them on empty, path and complete graphs with up to three vertices, k = 1 and k = n, and antiparallel arcs. Also promote MinimumVertexCover -> EnsembleComputation num_subsets, one subset per edge, and convert the ConsecutiveOnesSubmatrix bound with try_from now that construction keeps it nonnegative. Co-Authored-By: Claude Opus 5.5 --- src/rules/consecutiveonessubmatrix_ilp.rs | 2 +- .../minimumvertexcover_ensemblecomputation.rs | 2 +- .../symbolic_parameter_contracts.rs | 85 +++++++++++++++++++ 3 files changed, 87 insertions(+), 2 deletions(-) diff --git a/src/rules/consecutiveonessubmatrix_ilp.rs b/src/rules/consecutiveonessubmatrix_ilp.rs index 41ba6339a..3c7eb412e 100644 --- a/src/rules/consecutiveonessubmatrix_ilp.rs +++ b/src/rules/consecutiveonessubmatrix_ilp.rs @@ -62,7 +62,7 @@ impl ReduceTo> for ConsecutiveOnesSubmatrix { fn reduce_to(&self) -> Result { let m = self.num_rows(); let n = self.num_cols(); - let k = self.bound() as usize; + let k = usize::try_from(self.bound()).expect("construction keeps 0 <= bound <= num_cols"); // Variable layout (all binary): // s_c: n vars at [0, n) — column selection diff --git a/src/rules/minimumvertexcover_ensemblecomputation.rs b/src/rules/minimumvertexcover_ensemblecomputation.rs index a6702de2b..a625c5c08 100644 --- a/src/rules/minimumvertexcover_ensemblecomputation.rs +++ b/src/rules/minimumvertexcover_ensemblecomputation.rs @@ -79,9 +79,9 @@ impl ReductionResult for ReductionVCToEC { transform = { exact { universe_size = "num_vertices + 1", + num_subsets = "num_edges", }, upper_bound { - num_subsets = "num_edges", budget = "num_vertices + num_edges + 1", }, } diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs index 6e864147f..fee6ad490 100644 --- a/src/unit_tests/symbolic_parameter_contracts.rs +++ b/src/unit_tests/symbolic_parameter_contracts.rs @@ -971,3 +971,88 @@ fn three_sat_contracts_cover_short_clauses() { check_reduced_parameters::<_, SubsetSum>(source, &["num_elements"], exact); } } + +#[test] +fn exact_construction_counts_hold_on_degenerate_graphs() { + use crate::models::algebraic::ILP; + use crate::models::decision::Decision; + use crate::models::graph::{ + HamiltonianCircuit, Kernel, MaximalIS, MaximumMatching, MinimumCoveringByCliques, + MinimumDominatingSet, MinimumVertexCover, PartitionIntoCliques, + PartitionIntoPathsOfLength2, PartitionIntoPerfectMatchings, + }; + use crate::models::misc::EnsembleComputation; + use crate::topology::{Graph, SimpleDigraph}; + use crate::types::One; + // Canonical examples are mid-sized; check the boundaries exact claims rely on: + // no vertices, no edges, k = 1, and k = n. + let exact = ParameterRelation::Exact; + let graphs = |n: usize| { + [ + SimpleGraph::empty(n), + SimpleGraph::path(n), + SimpleGraph::complete(n), + ] + }; + for n in 0..=3 { + for graph in graphs(n) { + let m = graph.num_edges(); + check_reduced_parameters::<_, ILP>( + HamiltonianCircuit::new(graph.clone()), + &["num_vars", "num_nonzeros"], + exact, + ); + check_reduced_parameters::<_, ILP>( + MaximalIS::new(graph.clone(), vec![1_i64; n]), + &["num_constraints", "num_nonzeros"], + exact, + ); + check_reduced_parameters::<_, ILP>( + MinimumDominatingSet::new(graph.clone(), vec![1_i64; n]), + &["num_nonzeros"], + exact, + ); + check_reduced_parameters::<_, ILP>( + MaximumMatching::new(graph.clone(), vec![1_i64; m]), + &["num_nonzeros"], + exact, + ); + check_reduced_parameters::<_, EnsembleComputation>( + MinimumVertexCover::new(graph.clone(), vec![One; n]), + &["universe_size", "num_subsets"], + exact, + ); + for k in [1, n].into_iter().filter(|&k| (1..=n).contains(&k)) { + check_reduced_parameters::<_, ILP>( + PartitionIntoPerfectMatchings::new(graph.clone(), k), + &["num_vars", "num_constraints"], + exact, + ); + check_reduced_parameters::<_, Decision>>( + PartitionIntoCliques::new(graph.clone(), k), + &["num_vertices", "num_edges"], + exact, + ); + } + if n % 3 == 0 { + check_reduced_parameters::<_, ILP>( + PartitionIntoPathsOfLength2::new(graph.clone()), + &["num_vars", "num_constraints", "num_nonzeros"], + exact, + ); + } + } + } + for arcs in [ + vec![], + vec![(0, 1)], + vec![(0, 1), (1, 0)], + vec![(0, 1), (1, 2), (2, 0)], + ] { + check_reduced_parameters::<_, ILP>( + Kernel::new(SimpleDigraph::new(3, arcs)), + &["num_nonzeros"], + exact, + ); + } +} From f7be5380adca51947cd42b32c57fb0254f028732 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 28 Oct 2026 08:30:34 -0700 Subject: [PATCH 05/12] Reduce negative-weight MaxCut to MinimumMatrixCover with an edge gadget MaxCut accepts negative weights, but the rule rejected them, so every planned path through it (for example Max2SAT -> MaxCut -> MinimumMatrixCover) failed on ordinary inputs. Replace each negative edge {u, v} by an auxiliary vertex joined to v with |w| + 1 and to u with |w|: every maximum cut separates the auxiliary vertex from v, so the gadget shifts the cut by the constant 2|w| + 1 and preserves maximum cuts. Extraction drops the auxiliary bits; num_rows becomes an upper bound. Co-Authored-By: Claude Opus 5.5 --- docs/paper/reductions.typ | 8 +-- src/rules/maxcut_minimummatrixcover.rs | 56 ++++++++++++------- .../rules/maxcut_minimummatrixcover.rs | 46 +++++++++++++-- 3 files changed, 82 insertions(+), 28 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 9fcc31655..0e2fd33c4 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -19988,13 +19988,13 @@ The following table shows concrete target-variable counts for example instances, *Multiplicity:* The fixture stores one canonical witness. The form is invariant under $f arrow.r -f$, so the complementary assignment $(-1, +1, -1, +1)$ (config $(0, 1, 0, 1)$) is equally optimal. ], )[ - @garey1979 (MS13) The construction takes $A$ to be the weighted adjacency matrix of $G$. The identity $sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 dot "cut"(S)$ — where $S = {i : f(i) = +1\}$ and $W = sum_(e in E) w(e)$ — converts MaxCut maximization into MinimumMatrixCover minimization with $O(n^2)$ overhead. + @garey1979 (MS13) The construction takes $A$ to be the weighted adjacency matrix of $G$. The identity $sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 dot "cut"(S)$ — where $S = {i : f(i) = +1\}$ and $W = sum_(e in E) w(e)$ — converts MaxCut maximization into MinimumMatrixCover minimization with $O(n^2)$ overhead for nonnegative weights. Each negative edge first becomes a two-edge gadget through one auxiliary vertex, giving $O((n + |E|)^2)$ overhead. ][ - _Construction._ Given a MaxCut instance $(G, w)$ with $G = (V, E)$, $|V| = n$, and nonnegative integer edge weights $w$, build the $n times n$ matrix $A$ with $a_(i j) = w(\{i, j\})$ for $\{i, j\} in E$, $a_(i j) = 0$ otherwise, and $a_(i i) = 0$. $A$ is symmetric, zero-diagonal, and nonnegative, hence a valid MinimumMatrixCover instance. + _Construction._ Given a MaxCut instance $(G, w)$ with $G = (V, E)$ and $|V| = n$, first remove negative weights. Replace each edge $\{u, v\}$ with $w(\{u, v\}) < 0$ by a fresh vertex $t$ and edges $\{t, v\}$ of weight $|w| + 1$ and $\{t, u\}$ of weight $|w|$. The resulting graph $G'$ has $n' <= n + |E|$ vertices and nonnegative weights $w'$. Build the $n' times n'$ matrix $A$ with $a_(i j) = w'(\{i, j\})$ for edges of $G'$, $a_(i j) = 0$ otherwise, and $a_(i i) = 0$. $A$ is symmetric, zero-diagonal, and nonnegative, hence a valid MinimumMatrixCover instance. - _Correctness._ For any $f in \{-1, +1\}^n$ with $S = \{i : f(i) = +1\}$, each edge $\{i, j\} in E$ appears twice in $sum_(i, j) a_(i j) f(i) f(j)$. A non-cut edge contributes $+2 w(\{i, j\})$ (same signs, $f(i) f(j) = +1$); a cut edge contributes $-2 w(\{i, j\})$. Summing yields $sum_(i, j) a_(i j) f(i) f(j) = 2 (W - "cut"(S)) - 2 "cut"(S) = 2 W - 4 "cut"(S)$. Since $2 W$ is a constant, $min_f sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 max_S "cut"(S)$, so the two problems share the same optimal partitions. ($arrow.r.double$) A maximum cut $S^*$ defines $f^*$ minimizing the quadratic form. ($arrow.l.double$) A minimizing $f^*$ defines $S^* = \{i : f^*(i) = +1\}$ achieving the maximum cut. + _Correctness._ For any $f in \{-1, +1\}^n$ with $S = \{i : f(i) = +1\}$, each edge $\{i, j\} in E$ appears twice in $sum_(i, j) a_(i j) f(i) f(j)$. A non-cut edge contributes $+2 w(\{i, j\})$ (same signs, $f(i) f(j) = +1$); a cut edge contributes $-2 w(\{i, j\})$. Summing yields $sum_(i, j) a_(i j) f(i) f(j) = 2 (W - "cut"(S)) - 2 "cut"(S) = 2 W - 4 "cut"(S)$. Since $2 W$ is a constant, $min_f sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 max_S "cut"(S)$ on $G'$. Each gadget preserves maximum cuts: moving $t$ to the side opposite $v$ gains $|w| + 1$ and loses at most $|w|$, so every maximum cut of $G'$ separates $t$ from $v$. Then $\{t, u\}$ is cut exactly when $u$ and $v$ share a side, and $|w| dot [u, v "together"] = w dot [u, v "cut"] + |w|$. Each gadget therefore adds the constant $2|w| + 1$, and maximum cuts of $G'$ restrict to maximum cuts of $G$; every maximum cut of $G$ extends to one of $G'$. Hence the two problems share the same optimal partitions on $V$. ($arrow.r.double$) A maximum cut $S^*$ defines $f^*$ minimizing the quadratic form. ($arrow.l.double$) A minimizing $f^*$ defines $S^* = \{i : f^*(i) = +1\}$ achieving the maximum cut. - _Precondition._ Nonnegative edge weights. Negative-weight MaxCut instances are out of scope; a separate weight-shifting reduction would be required. + _Solution extraction._ Keep the signs of the original vertices and drop auxiliary vertices. _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction is the identity. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip. ] diff --git a/src/rules/maxcut_minimummatrixcover.rs b/src/rules/maxcut_minimummatrixcover.rs index a1e8f50c7..520f2d7cd 100644 --- a/src/rules/maxcut_minimummatrixcover.rs +++ b/src/rules/maxcut_minimummatrixcover.rs @@ -12,10 +12,14 @@ //! partition encoding (`config[i] = 1 ⇔ i ∈ S`) and MinimumMatrixCover's //! sign encoding (`config[i] = 1 ⇔ f(i) = +1 ⇔ i ∈ S`). //! -//! **Precondition:** all edge weights must be nonnegative. The reduction -//! panics on any negative weight, since `MinimumMatrixCover` requires a -//! nonnegative integer matrix. Negative-weight `MaxCut` instances are out -//! of scope and must use a different (preprocessing) reduction. +//! `MinimumMatrixCover` requires a nonnegative matrix, so each negative edge +//! `{u, v}` with weight `w < 0` becomes an auxiliary vertex `t` joined to `v` +//! by weight `|w| + 1` and to `u` by weight `|w|`. Moving `t` to the side +//! opposite `v` gains `|w| + 1` and loses at most `|w|`, so every maximum cut +//! separates `t` from `v`. Then `t` is cut from `u` exactly when `u` and `v` +//! share a side, and `|w| · [u, v same side] = w · [u, v cut] + |w|`: each +//! gadget shifts the cut by the constant `2|w| + 1`. Maximum cuts, and so +//! optimal sign assignments, correspond after dropping auxiliary vertices. //! //! Reference: Garey & Johnson, *Computers and Intractability* (1979), //! Appendix A1.2, MS13 ("Transformation from MAXIMUM CUT"). @@ -30,6 +34,7 @@ use crate::topology::{Graph, SimpleGraph}; #[derive(Debug, Clone)] pub struct ReductionMaxCutToMMC { target: MinimumMatrixCover, + num_source_vertices: usize, } impl ReductionResult for ReductionMaxCutToMMC { @@ -40,7 +45,7 @@ impl ReductionResult for ReductionMaxCutToMMC { &self.target } - /// Solution extraction is the identity. + /// Solution extraction keeps the source vertices' bits. /// /// Both encodings agree that bit `i = 1` means vertex `i` is in `S`: /// MaxCut treats `config[i] = 1` as one side of the partition, and @@ -54,13 +59,14 @@ impl ReductionResult for ReductionMaxCutToMMC { ) -> crate::rules::ExtractionResult<::Solution> { crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?; - Ok(target_solution.to_vec()) + Ok(target_solution[..self.num_source_vertices].to_vec()) } } #[reduction( - transform = exact { - num_rows = "num_vertices", + transform = upper_bound { + // One auxiliary row per negative-weight edge. + num_rows = "num_vertices + num_edges", } )] impl ReduceTo for MaxCut { @@ -68,24 +74,36 @@ impl ReduceTo for MaxCut { fn reduce_to(&self) -> Result { let n = self.graph().num_vertices(); - let mut matrix: Vec> = vec![vec![0i64; n]; n]; + let edges = self.edges(); + let size = n + edges.iter().filter(|&&(_, _, w)| w < 0).count(); + let mut matrix: Vec> = vec![vec![0i64; size]; size]; + let mut link = |a: usize, b: usize, weight: i64| { + matrix[a][b] = weight; + matrix[b][a] = weight; + }; - for (u, v, w) in self.edges() { - if w < 0 { - return Err(crate::rules::ReductionError::invalid_target::< + let mut auxiliary = n; + for (u, v, w) in edges { + if w >= 0 { + link(u, v, w); + continue; + } + let magnitude = w.checked_neg(); + let anchor = magnitude.and_then(|m| m.checked_add(1)); + let (Some(magnitude), Some(anchor)) = (magnitude, anchor) else { + return Err(crate::rules::ReductionError::integer_overflow::< MaxCut, MinimumMatrixCover, - >(format!( - "edge ({u}, {v}) has negative weight {w}" - ))); - } - let w64 = w; - matrix[u][v] = w64; - matrix[v][u] = w64; + >("negating a negative edge weight")); + }; + link(auxiliary, v, anchor); + link(auxiliary, u, magnitude); + auxiliary += 1; } Ok(ReductionMaxCutToMMC { target: MinimumMatrixCover::new(matrix), + num_source_vertices: n, }) } } diff --git a/src/unit_tests/rules/maxcut_minimummatrixcover.rs b/src/unit_tests/rules/maxcut_minimummatrixcover.rs index 7e6ef4a1b..6ad377025 100644 --- a/src/unit_tests/rules/maxcut_minimummatrixcover.rs +++ b/src/unit_tests/rules/maxcut_minimummatrixcover.rs @@ -229,7 +229,7 @@ fn test_empty_graph() { #[test] fn test_overhead_num_rows_equals_num_vertices() { - // Spot-check the exact parameter relation: target.num_rows == source.num_vertices. + // Nonnegative weights add no auxiliary rows. for n in [1usize, 2, 5, 8] { let edges: Vec<(usize, usize)> = (0..n.saturating_sub(1)).map(|i| (i, i + 1)).collect(); let weights: Vec = vec![1; edges.len()]; @@ -241,12 +241,48 @@ fn test_overhead_num_rows_equals_num_vertices() { } #[test] -fn test_negative_weight_is_rejected() { - // The reduction only handles nonnegative weights. - let source = MaxCut::::new(SimpleGraph::new(2, vec![(0, 1)]), vec![-1]); +fn test_maxcut_to_minimummatrixcover_closed_loop_negative_weights() { + // Mixed signs: a negative edge rewards keeping its endpoints together. + for (n, edges, weights) in [ + (2, vec![(0, 1)], vec![-1_i64]), + (3, vec![(0, 1), (1, 2), (0, 2)], vec![-2, 3, 1]), + (4, vec![(0, 1), (1, 2), (2, 3), (0, 3)], vec![-1, -1, 2, 2]), + (3, vec![(0, 1), (1, 2), (0, 2)], vec![-1, -1, -1]), + ] { + let source = MaxCut::::new(SimpleGraph::new(n, edges), weights); + let reduction = + ReduceTo::::reduce_to(&source).expect("reduction should succeed"); + assert_optimization_round_trip_from_optimization_target( + &source, + &reduction, + "MaxCut with negative weights -> MinimumMatrixCover", + ); + } +} + +#[test] +fn test_negative_edge_gadget_layout() { + // Edge {0, 1} with w = -2 adds vertex 2: weight 3 to v = 1 and 2 to u = 0. + let source = MaxCut::::new(SimpleGraph::new(2, vec![(0, 1)]), vec![-2]); + let reduction = + ReduceTo::::reduce_to(&source).expect("reduction should succeed"); + let expected: Vec> = vec![vec![0, 0, 2], vec![0, 0, 3], vec![2, 3, 0]]; + assert_eq!(reduction.target_problem().matrix(), expected.as_slice()); + // Auxiliary bits are dropped on extraction. + assert_eq!( + reduction + .extract_solution(&vec![true, true, false]) + .unwrap(), + vec![true, true] + ); +} + +#[test] +fn test_minimum_negative_weight_overflows() { + let source = MaxCut::::new(SimpleGraph::new(2, vec![(0, 1)]), vec![i64::MIN]); let error = ReduceTo::::reduce_to(&source).unwrap_err(); assert!(matches!( error, - crate::rules::ReductionError::InvalidTarget { .. } + crate::rules::ReductionError::IntegerOverflow { .. } )); } From ef18c7635bb68aa2bd36b41f995ed3c89c3db9db Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 28 Oct 2026 08:37:47 -0700 Subject: [PATCH 06/12] Simplify the MaxCut gadget, retype the COS bound, and clean up docs - ConsecutiveOnesSubmatrix stores its column-count bound as usize, so serde and the CLI reject negatives by type and the model and ILP rule drop their conversions. - The MaxCut -> MinimumMatrixCover gadget computes |w| + 1 as 1 - w with one checked subtraction; module docs and the paper's duplicate extraction paragraph now describe the auxiliary vertices. - The PartitionIntoPathsOfLength2 comment states why its counts are exact. - The degenerate-graph test covers every valid k; transform layouts are consistent. Co-Authored-By: Claude Opus 5.5 --- docs/paper/reductions.typ | 4 +--- .../algebraic/consecutive_ones_submatrix.rs | 22 +++++++++---------- src/rules/consecutiveonessubmatrix_ilp.rs | 2 +- ...tisfiability_decisionminimumvertexcover.rs | 4 ++-- src/rules/ksatisfiability_kclique.rs | 2 +- ...satisfiability_oneinthreesatisfiability.rs | 3 ++- src/rules/maxcut_minimummatrixcover.rs | 13 +++++------ src/rules/partitionintopathsoflength2_ilp.rs | 4 ++-- .../algebraic/consecutive_ones_submatrix.rs | 2 +- .../symbolic_parameter_contracts.rs | 13 +++++------ 10 files changed, 31 insertions(+), 38 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 0e2fd33c4..034ee6717 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -19994,9 +19994,7 @@ The following table shows concrete target-variable counts for example instances, _Correctness._ For any $f in \{-1, +1\}^n$ with $S = \{i : f(i) = +1\}$, each edge $\{i, j\} in E$ appears twice in $sum_(i, j) a_(i j) f(i) f(j)$. A non-cut edge contributes $+2 w(\{i, j\})$ (same signs, $f(i) f(j) = +1$); a cut edge contributes $-2 w(\{i, j\})$. Summing yields $sum_(i, j) a_(i j) f(i) f(j) = 2 (W - "cut"(S)) - 2 "cut"(S) = 2 W - 4 "cut"(S)$. Since $2 W$ is a constant, $min_f sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 max_S "cut"(S)$ on $G'$. Each gadget preserves maximum cuts: moving $t$ to the side opposite $v$ gains $|w| + 1$ and loses at most $|w|$, so every maximum cut of $G'$ separates $t$ from $v$. Then $\{t, u\}$ is cut exactly when $u$ and $v$ share a side, and $|w| dot [u, v "together"] = w dot [u, v "cut"] + |w|$. Each gadget therefore adds the constant $2|w| + 1$, and maximum cuts of $G'$ restrict to maximum cuts of $G$; every maximum cut of $G$ extends to one of $G'$. Hence the two problems share the same optimal partitions on $V$. ($arrow.r.double$) A maximum cut $S^*$ defines $f^*$ minimizing the quadratic form. ($arrow.l.double$) A minimizing $f^*$ defines $S^* = \{i : f^*(i) = +1\}$ achieving the maximum cut. - _Solution extraction._ Keep the signs of the original vertices and drop auxiliary vertices. - - _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction is the identity. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip. + _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction keeps the original vertices' bits and drops the auxiliary ones. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip. ] // 14. HamiltonianPath → IsomorphicSpanningTree (#912) diff --git a/src/models/algebraic/consecutive_ones_submatrix.rs b/src/models/algebraic/consecutive_ones_submatrix.rs index 2b9d2eb95..7cd3e6832 100644 --- a/src/models/algebraic/consecutive_ones_submatrix.rs +++ b/src/models/algebraic/consecutive_ones_submatrix.rs @@ -21,7 +21,7 @@ inventory::submit! { description: "Find K columns of a binary matrix that can be permuted to have the consecutive ones property", fields: &[ FieldInfo { name: "matrix", type_name: "Vec>", description: "m×n binary matrix A" }, - FieldInfo { name: "bound", type_name: "i64", description: "Required number of columns K" }, + FieldInfo { name: "bound", type_name: "usize", description: "Required number of columns K" }, ], } } @@ -62,13 +62,13 @@ inventory::submit! { #[serde(try_from = "ConsecutiveOnesSubmatrixData")] pub struct ConsecutiveOnesSubmatrix { matrix: Vec>, - bound: i64, + bound: usize, } #[derive(Deserialize)] struct ConsecutiveOnesSubmatrixData { matrix: Vec>, - bound: i64, + bound: usize, } impl TryFrom for ConsecutiveOnesSubmatrix { @@ -84,23 +84,21 @@ impl ConsecutiveOnesSubmatrix { /// /// # Panics /// - /// Panics if `bound` is negative or exceeds `n`, or if rows have inconsistent lengths. - pub fn new(matrix: Vec>, bound: i64) -> Self { + /// Panics if `bound > n`, or if rows have inconsistent lengths. + pub fn new(matrix: Vec>, bound: usize) -> Self { Self::try_new(matrix, bound).unwrap_or_else(|error| panic!("{error}")) } fn try_new( matrix: Vec>, - bound: i64, + bound: usize, ) -> Result { let n = matrix.first().map_or(0, Vec::len); if matrix.iter().any(|row| row.len() != n) { return Err("all matrix rows must have the same length".into()); } - if !usize::try_from(bound).is_ok_and(|bound| bound <= n) { - return Err( - format!("bound ({bound}) must be in 0..={n}, the number of columns").into(), - ); + if bound > n { + return Err(format!("bound ({bound}) must be <= number of columns ({n})").into()); } Ok(Self { matrix, bound }) } @@ -111,7 +109,7 @@ impl ConsecutiveOnesSubmatrix { } /// Returns the bound (the required number of columns). - pub fn bound(&self) -> i64 { + pub fn bound(&self) -> usize { self.bound } @@ -224,7 +222,7 @@ impl Problem for ConsecutiveOnesSubmatrix { .filter(|(_, &v)| v) .map(|(i, _)| i) .collect(); - if usize::try_from(self.bound) != Ok(selected.len()) { + if self.bound != selected.len() { return Ok(crate::types::Or(false)); } self.any_permutation_has_c1p(&selected) diff --git a/src/rules/consecutiveonessubmatrix_ilp.rs b/src/rules/consecutiveonessubmatrix_ilp.rs index 3c7eb412e..060040ce8 100644 --- a/src/rules/consecutiveonessubmatrix_ilp.rs +++ b/src/rules/consecutiveonessubmatrix_ilp.rs @@ -62,7 +62,7 @@ impl ReduceTo> for ConsecutiveOnesSubmatrix { fn reduce_to(&self) -> Result { let m = self.num_rows(); let n = self.num_cols(); - let k = usize::try_from(self.bound()).expect("construction keeps 0 <= bound <= num_cols"); + let k = self.bound(); // Variable layout (all binary): // s_c: n vars at [0, n) — column selection diff --git a/src/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/rules/ksatisfiability_decisionminimumvertexcover.rs index 6221cde56..071c53240 100644 --- a/src/rules/ksatisfiability_decisionminimumvertexcover.rs +++ b/src/rules/ksatisfiability_decisionminimumvertexcover.rs @@ -69,9 +69,9 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToDecisionMVC {} #[reduction( transform = { - exact { num_vertices = "2 * num_vars + 3 * num_clauses", }, + exact { num_vertices = "2 * num_vars + 3 * num_clauses" }, // A clause with fewer than three literals links fewer triangle corners. - upper_bound { num_edges = "num_vars + 6 * num_clauses", }, + upper_bound { num_edges = "num_vars + 6 * num_clauses" }, } )] impl ReduceTo>> for KSatisfiability { diff --git a/src/rules/ksatisfiability_kclique.rs b/src/rules/ksatisfiability_kclique.rs index ac3f830c1..2952e3326 100644 --- a/src/rules/ksatisfiability_kclique.rs +++ b/src/rules/ksatisfiability_kclique.rs @@ -58,7 +58,7 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToKClique {} #[reduction( transform = { - exact { k = "num_clauses + 1", }, + exact { k = "num_clauses + 1" }, // Clauses built with `new_allow_less` may have fewer than three literals. upper_bound { num_vertices = "3 * num_clauses + 1", diff --git a/src/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/rules/ksatisfiability_oneinthreesatisfiability.rs index f86ad1ac8..d8e7d3165 100644 --- a/src/rules/ksatisfiability_oneinthreesatisfiability.rs +++ b/src/rules/ksatisfiability_oneinthreesatisfiability.rs @@ -56,7 +56,8 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToOneInThreeSAT {} upper_bound { num_vars = "num_vars + 2 + 6 * num_clauses", }, -})] + } +)] impl ReduceTo for KSatisfiability { type Result = Reduction3SATToOneInThreeSAT; diff --git a/src/rules/maxcut_minimummatrixcover.rs b/src/rules/maxcut_minimummatrixcover.rs index 520f2d7cd..01c7b741a 100644 --- a/src/rules/maxcut_minimummatrixcover.rs +++ b/src/rules/maxcut_minimummatrixcover.rs @@ -1,14 +1,14 @@ //! Reduction from MaxCut to MinimumMatrixCover. //! -//! Given a MaxCut instance `(G, w)` with nonnegative integer edge weights, -//! the target matrix `A` is the symmetric weighted adjacency matrix of `G`: +//! For nonnegative edge weights, the target matrix `A` is the symmetric +//! weighted adjacency matrix of `G`: //! `a_{ij} = w({i, j})` if `{i, j} ∈ E`, otherwise `0` (diagonal is `0`). //! //! The key identity is //! `Σ_{i,j} a_{ij} · f(i) · f(j) = 2 W − 4 · cut(S)`, //! where `S = { i : f(i) = +1 }` and `W = Σ_{e ∈ E} w(e)`. Minimizing the //! quadratic form is therefore equivalent to maximizing the cut, and the -//! reduction is witness-preserving via the identity map between MaxCut's +//! original vertices keep their bits between MaxCut's //! partition encoding (`config[i] = 1 ⇔ i ∈ S`) and MinimumMatrixCover's //! sign encoding (`config[i] = 1 ⇔ f(i) = +1 ⇔ i ∈ S`). //! @@ -88,16 +88,15 @@ impl ReduceTo for MaxCut { link(u, v, w); continue; } - let magnitude = w.checked_neg(); - let anchor = magnitude.and_then(|m| m.checked_add(1)); - let (Some(magnitude), Some(anchor)) = (magnitude, anchor) else { + // anchor = |w| + 1 = 1 - w; then |w| = anchor - 1 cannot overflow. + let Some(anchor) = 1_i64.checked_sub(w) else { return Err(crate::rules::ReductionError::integer_overflow::< MaxCut, MinimumMatrixCover, >("negating a negative edge weight")); }; link(auxiliary, v, anchor); - link(auxiliary, u, magnitude); + link(auxiliary, u, anchor - 1); auxiliary += 1; } diff --git a/src/rules/partitionintopathsoflength2_ilp.rs b/src/rules/partitionintopathsoflength2_ilp.rs index 041374742..6e6d7b065 100644 --- a/src/rules/partitionintopathsoflength2_ilp.rs +++ b/src/rules/partitionintopathsoflength2_ilp.rs @@ -67,8 +67,8 @@ 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. +// Construction requires 3 | n and SimpleGraph has no loops or repeated edges, +// so q = n/3 and e = num_edges: q(n+e) variables, n+2q+3eq rows, 2nq+8eq terms. #[reduction(transform = { exact { num_vars = "num_vertices * (num_vertices + num_edges) / 3", diff --git a/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs b/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs index 1f6d60fe7..39874eba4 100644 --- a/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs +++ b/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs @@ -244,7 +244,7 @@ fn json_rejects_invalid_instance() { #[test] fn json_rejects_negative_bound() { - // A column count is nonnegative; a negative bound would break the u64 parameter. + // The bound counts columns, so its type rejects negative values. assert!(serde_json::from_value::( serde_json::json!({"matrix":[[true]],"bound":-1}) ) diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs index fee6ad490..1cb5eeca5 100644 --- a/src/unit_tests/symbolic_parameter_contracts.rs +++ b/src/unit_tests/symbolic_parameter_contracts.rs @@ -985,17 +985,14 @@ fn exact_construction_counts_hold_on_degenerate_graphs() { use crate::topology::{Graph, SimpleDigraph}; use crate::types::One; // Canonical examples are mid-sized; check the boundaries exact claims rely on: - // no vertices, no edges, k = 1, and k = n. + // no vertices, no edges, and every valid k. let exact = ParameterRelation::Exact; - let graphs = |n: usize| { - [ + for n in 0..=3 { + for graph in [ SimpleGraph::empty(n), SimpleGraph::path(n), SimpleGraph::complete(n), - ] - }; - for n in 0..=3 { - for graph in graphs(n) { + ] { let m = graph.num_edges(); check_reduced_parameters::<_, ILP>( HamiltonianCircuit::new(graph.clone()), @@ -1022,7 +1019,7 @@ fn exact_construction_counts_hold_on_degenerate_graphs() { &["universe_size", "num_subsets"], exact, ); - for k in [1, n].into_iter().filter(|&k| (1..=n).contains(&k)) { + for k in 1..=n { check_reduced_parameters::<_, ILP>( PartitionIntoPerfectMatchings::new(graph.clone(), k), &["num_vars", "num_constraints"], From 5e512c738b3d86390d0f7420b4514701e22e67d7 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 28 Oct 2026 10:41:36 -0700 Subject: [PATCH 07/12] Remove the KSatisfiability KN variant and short-clause constructors KSatisfiability was Satisfiability under another name: it checked no clause width and its only edges were identity casts into and out of it. Every path from K2 or K3 paid an extra hop through it. - Drop the KN variant; K2 and K3 now reduce directly to Satisfiability and K3 is the default variant. - Remove new_allow_less/try_new_allow_less. K2 and K3 always hold exactly K literals per clause, matching what serde and the CLI already enforced. - Delete the short- and empty-clause branches these constructors forced on 3-SAT rules, and declare 3SAT -> KClique num_vertices and 3SAT -> DecisionMVC num_edges exact again. Co-Authored-By: Claude Opus 5.5 --- docs/paper/reductions.typ | 46 +++++------ problemreductions-cli/src/cli.rs | 6 +- src/models/formula/ksat.rs | 65 +++------------- src/rules/ksatisfiability_bicliquecover.rs | 25 ++---- src/rules/ksatisfiability_casts.rs | 26 ------- src/rules/ksatisfiability_cyclicordering.rs | 38 ++++------ ...tisfiability_decisionminimumvertexcover.rs | 30 ++------ ...tisfiability_feasibleregisterassignment.rs | 25 ++---- src/rules/ksatisfiability_kclique.rs | 46 +++++------ src/rules/ksatisfiability_kernel.rs | 4 +- .../ksatisfiability_preemptivescheduling.rs | 23 +++--- src/rules/ksatisfiability_qubo.rs | 15 ++-- .../ksatisfiability_registersufficiency.rs | 21 ++--- src/rules/mod.rs | 1 - src/rules/sat_ksat.rs | 47 +++++++----- src/solvers/pipelines.rs | 2 +- src/unit_tests/ilp_overhead.rs | 42 +++++----- src/unit_tests/models/formula/ksat.rs | 60 ++++----------- src/unit_tests/reduction_graph.rs | 4 +- src/unit_tests/rules/aggregate_contracts.rs | 17 ++--- src/unit_tests/rules/graph.rs | 2 +- .../rules/ksatisfiability_acyclicpartition.rs | 11 ++- .../rules/ksatisfiability_bicliquecover.rs | 25 +++--- .../rules/ksatisfiability_cyclicordering.rs | 31 ++------ ...tisfiability_decisionminimumvertexcover.rs | 25 ++---- ...tisfiability_feasibleregisterassignment.rs | 61 ++------------- .../rules/ksatisfiability_kclique.rs | 76 ++++++++----------- .../rules/ksatisfiability_kernel.rs | 39 +++++----- .../ksatisfiability_monochromatictriangle.rs | 13 ++-- ...satisfiability_oneinthreesatisfiability.rs | 12 ++- .../ksatisfiability_preemptivescheduling.rs | 39 +++++----- .../ksatisfiability_quadraticcongruences.rs | 16 ++-- src/unit_tests/rules/ksatisfiability_qubo.rs | 36 +++++---- .../ksatisfiability_registersufficiency.rs | 42 ++++------ .../rules/ksatisfiability_timetabledesign.rs | 7 +- .../symbolic_parameter_contracts.rs | 33 ++++---- 36 files changed, 354 insertions(+), 657 deletions(-) delete mode 100644 src/rules/ksatisfiability_casts.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 034ee6717..c7a39e66d 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -12465,11 +12465,11 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with $ H = a y_3 + 2(y_1 y_2 - 2 y_1 a - 2 y_2 a + 3a). $ Rosenberg's penalty is zero when $a=y_1 y_2$ and positive otherwise @borosgruber2014quadratization. Its multiplier 2 strictly exceeds the possible unit gain from the $a y_3$ term. Thus minimizing over each independent auxiliary gives exactly the clause falsification indicator, including repeated or complementary literals. Expand with $x^2=x$ into an upper-triangular QUBO matrix, and retain the omitted constant $C$. - _Correctness._ For every source assignment, the minimum target energy over auxiliaries is the number of falsified clauses minus $C$. Every clause expression is nonnegative before subtracting $C$. Hence the formula is satisfiable iff the global target minimum is exactly $-C$. A satisfying assignment lifts by setting each cubic auxiliary to $y_1 y_2$; every zero-penalty target configuration projects to a satisfying source assignment. If an empty clause occurs, its constant penalty 1 prevents the threshold from being attained. Empty formulas have $C=0$ and every source assignment satisfies them. + _Correctness._ For every source assignment, the minimum target energy over auxiliaries is the number of falsified clauses minus $C$. Every clause expression is nonnegative before subtracting $C$. Hence the formula is satisfiable iff the global target minimum is exactly $-C$. A satisfying assignment lifts by setting each cubic auxiliary to $y_1 y_2$; every zero-penalty target configuration projects to a satisfying source assignment. Empty formulas have $C=0$ and every source assignment satisfies them. _Extraction._ Formal target validation precedes decoding. The DecisionQUBO target checks the bound $E <= -C$, and the registered aggregate decoder maps its completed `Or` value identically. Direct witness extraction rejects energies above the bound and reads the first $n$ coordinates only for a satisfying target witness. It does not solve SAT or repair auxiliary assignments. A completed target decision gives the source decision. - _Domain and overhead._ The K2 variant has $n$ variables; K3 reserves $n+m$, with unused auxiliaries mathematically free for short clauses. Native `new_allow_less` permits widths up to K; CLI and serde still require exactly K per actual clause. Source and target both use `Or`; the target wraps the integer QUBO with the signed bound $-C$. Matrix and constant accumulation use checked arithmetic; literal indices come from the formal `CNFClause::variables` API. Neither endpoint nor variant changes. + _Domain and overhead._ The K2 variant has $n$ variables; K3 reserves $n+m$, one auxiliary per clause. Every clause has exactly K literals. Source and target both use `Or`; the target wraps the integer QUBO with the signed bound $-C$. Matrix and constant accumulation use checked arithmetic; literal indices come from the formal `CNFClause::variables` API. Neither endpoint nor variant changes. ] #let ksat_qc = load-example("KSatisfiability", "QuadraticCongruences") @@ -17306,16 +17306,6 @@ Problems parameterized by graph type, weight type, target type, or clause width _Solution extraction._ Return the target configuration unchanged. ] -#reduction-rule("KSatisfiability", "KSatisfiability")[ - A $k$-SAT instance with fixed clause width ($k = 2$ or $k = 3$) converts to generic $k$-SAT by constructing the registered $K_N$ variant. The clauses and variables are preserved verbatim; the target uses `new_allow_less` to accept clauses with fewer than $k$ literals. -][ - _Construction._ Given $"KSat"_(K_j)(n, cal(C))$ with $j in {2, 3}$, construct $"KSat"_(K_N)(n, cal(C))$ with the same $n$ variables and clause set $cal(C)$. - - _Correctness._ Every clause in $cal(C)$ has at most $j$ literals. The $K_N$ variant accepts clauses of any width, so all clauses remain valid. The satisfiability condition (every clause has at least one true literal) is unchanged. - - _Solution extraction._ Return the target configuration unchanged. -] - #reduction-rule("SpinGlass", "SpinGlass")[ An Ising spin-glass instance with integer couplings and fields ($J_(i j), h_i in ZZ$) converts to the floating-point variant ($J_(i j), h_i in RR$) through exact `i64_to_exact_f64` embeddings. The graph topology is preserved. ][ @@ -17936,7 +17926,7 @@ The following table shows concrete target-variable counts for example instances, )[ Use the classical 3-SAT to Vertex Cover gadget construction, then ask whether the resulting graph has a vertex cover of size at most $k = n + 2m$ @garey1979. ][ - _Construction._ Given 3-CNF $phi$ with $n$ variables and $m$ clauses, build the graph $G = (V, E)$ used in the classical 3-SAT $arrow.r$ Minimum Vertex Cover reduction: for each variable $x_i$, add literal vertices $u_i$ and $overline(u)_i$ with one truth-setting edge between them; for each clause $c_j$, add triangle vertices $t^j_0, t^j_1, t^j_2$; for each literal position $(j, r)$, add a communication edge from $t^j_r$ to the literal vertex representing that literal. Assign unit weight to every vertex and set the decision threshold to $k = n + 2m$. For accepted short nonempty clauses, repeat their literals to fill three positions. For an empty clause, keep its triangle without communication edges and use threshold $-1$, making the decision instance infeasible. The vertex count stays exact; the edge count is at most $n+6m$. + _Construction._ Given 3-CNF $phi$ with $n$ variables and $m$ clauses, build the graph $G = (V, E)$ used in the classical 3-SAT $arrow.r$ Minimum Vertex Cover reduction: for each variable $x_i$, add literal vertices $u_i$ and $overline(u)_i$ with one truth-setting edge between them; for each clause $c_j$, add triangle vertices $t^j_0, t^j_1, t^j_2$; for each literal position $(j, r)$, add a communication edge from $t^j_r$ to the literal vertex representing that literal. Assign unit weight to every vertex and set the decision threshold to $k = n + 2m$. The graph has exactly $2n+3m$ vertices and $n+6m$ edges. _Correctness._ ($arrow.r.double$) If $phi$ is satisfiable, choose one literal vertex per variable according to a satisfying assignment and choose two triangle vertices per clause, omitting a vertex whose literal is true. This gives a cover of size $n + 2m$, so the decision instance is yes. ($arrow.l.double$) If the decision instance is yes, any cover of size at most $n + 2m$ must use exactly one literal vertex per variable edge and exactly two vertices per clause triangle. The omitted triangle vertex in each clause has its communication edge covered only by a selected literal vertex, so the corresponding literal is true. These selected literal vertices define a satisfying assignment for $phi$. @@ -17992,7 +17982,7 @@ The following table shows concrete target-variable counts for example instances, Conversely, either equal signal colouring extends: make that colour the cycles $u,v,w,a,b,u$ and $u,v,w,c,d,u$ in the two cliques, and give all remaining edges the other colour. Both cycles agree on the private triangle, and each clique has no monochromatic triangle. No triangle crosses between the two signal edges. - _Construction._ Let the source have $n$ variables and $m$ clauses of length at most three; the typed API also admits shorter clauses. Let $q$ count its length-three clauses. + _Construction._ Let the source have $n$ variables and $m$ clauses, each with three literal positions. Let $q$ count its length-three clauses. 1. Apply the existing typed embedding into Satisfiability and the existing SAT-to-NAE reduction. It adds a sentinel $s$, replacing each nonempty clause $C$ by $"NAE"(C,s)$ and an empty clause by $"NAE"(s,s)$. 2. Replace $"NAE"(a,b)$ by $"NAE"(a,b,b)$; keep triples unchanged; replace $"NAE"(a,b,c,d)$ by $"NAE"(a,b,z)$ and $"NAE"(overline(z),c,d)$ with a fresh variable $z$. There are $N=n+1+q$ logical variables and $m+q$ resulting triples. @@ -18104,9 +18094,9 @@ The following table shows concrete target-variable counts for example instances, #reduction-rule("KSatisfiability", "FeasibleRegisterAssignment", example: false, )[ - Sethi's Reduction 3 @sethi1973 builds a DAG with shared-register variable leaf pairs and $p\/q\/r\/overline(r)$ clause gadgets. Nonempty short clauses are padded by repeating a literal; occurring variables are compacted. For $s$ declared source variables and $c$ clauses, the target has at most $2s+12c$ vertices, $15c$ arcs, $s+9c$ registers, and $s+3c$ pairs of vertices sharing a register. + Sethi's Reduction 3 @sethi1973 builds a DAG with shared-register variable leaf pairs and $p\/q\/r\/overline(r)$ clause gadgets. Occurring variables are compacted. For $s$ declared source variables and $c$ clauses, the target has at most $2s+12c$ vertices, $15c$ arcs, $s+9c$ registers, and $s+3c$ pairs of vertices sharing a register. ][ - _Native normalization._ If any clause is empty, return the three-vertex DAG with dependencies $(2,0),(2,1)$ and register assignment $(0,0,1)$. Both predecessors must stay live until vertex 2, so neither can overwrite the other's register; this target is infeasible. Otherwise collect appearing source indices in increasing order and store their inverse map. Pad each nonempty clause to three literal occurrences by repeating its first literal. Repetition preserves a disjunction, and each occurrence has its own gadget and register pair, so no distinct-variable assumption is needed. An empty conjunction yields the empty DAG and empty realization. + _Native normalization._ Collect appearing source indices in increasing order and store their inverse map. Each of the three literal occurrences of a clause, including repeated literals, has its own gadget and register pair, so no distinct-variable assumption is needed. An empty conjunction yields the empty DAG and empty realization. _Construction._ Let $a$ be the number of appearing variables. For each compact variable $x_k$, create leaves $s_k^+,s_k^-$ sharing register $S_k$. For every clause position $(i,j)$ create $p_(i,j),q_(i,j),r_(i,j),overline(r)_(i,j)$. The $p$ and $q$ registers are unique, while $r$ and $overline(r)$ share a fresh register $R_(i,j)$. Arcs point from a consumer to its dependency: $q_(i,j) -> p_(i,j) -> r_(i,j)$ and $q_(i,j) -> overline(r)_(i,j+1)$, with positions cyclic modulo three. For positive literal $x_k$, add $r_(i,j) -> s_k^+$ and $overline(r)_(i,j) -> s_k^-$; reverse these attachments for a negative literal. This DAG has four levels: leaves, $r/overline(r)$, $p$, and $q$. @@ -18116,7 +18106,7 @@ The following table shows concrete target-variable counts for example instances, _Extraction._ Validate the complete position vector and reject $"Or(false)"$. Set each appearing source variable true iff its compact positive leaf occurs before its negative leaf. Restore original indices through the inverse map and assign false to unused variables. The target model's permitted last-use overwrite does not weaken the order-transfer proof: neither member of a shared pair is the other member's consumer in this construction. - _Bounds and native arithmetic._ For the ordinary construction $a <= min(s,3c)$, so the displayed upper bounds follow from the exact counts $2a+12c$, $15c$, $a+9c$, and $a+3c$. The fixed NO target has counts $(3,2,2,1)$ and also satisfies the bounds whenever an empty clause exists; the empty YES target has all counts zero. Let $I="isize::MAX"$. A native source clause stores a vector object of 24 bytes on 64-bit or 12 bytes on 32-bit, so successful allocation of its outer vector bounds $c$ by $I/24$ or $I/12$. Therefore $2a+12c <= 18c$, $a+9c <= 12c$, and $15c$ fit $"usize"$ before target allocation on both architectures. Once the target register-assignment vector is allocated, every indexed vertex is within that vector. All same-register groups have size two except the fixed target's singleton, so pair counting introduces no large product. Checked construction arithmetic is retained; allocation and solver limits are not infeasibility proofs. + _Bounds and native arithmetic._ For the ordinary construction $a <= min(s,3c)$, so the displayed upper bounds follow from the exact counts $2a+12c$, $15c$, $a+9c$, and $a+3c$. The empty YES target has all counts zero. Let $I="isize::MAX"$. A native source clause stores a vector object of 24 bytes on 64-bit or 12 bytes on 32-bit, so successful allocation of its outer vector bounds $c$ by $I/24$ or $I/12$. Therefore $2a+12c <= 18c$, $a+9c <= 12c$, and $15c$ fit $"usize"$ before target allocation on both architectures. Once the target register-assignment vector is allocated, every indexed vertex is within that vector. All same-register groups have size two, so pair counting introduces no large product. Checked construction arithmetic is retained; allocation and solver limits are not infeasibility proofs. ] #let ksat_rs = load-example("KSatisfiability", "RegisterSufficiency") @@ -18143,7 +18133,7 @@ The following table shows concrete target-variable counts for example instances, )[ Sethi's Reduction 1 and Theorem 3.11 @sethi1973 encode literal choices through register pressure. We extend the construction to the native zero-to-three-literal clause domain by truth-preserving normalization and explicit empty-formula boundaries. The original padding $b=max(2n-m,0)$ is retained. ][ - _Normalization._ A formula containing an empty clause is false; output a single output vertex with register bound zero. An empty conjunction is true; output the empty graph with bound zero. In every other case collect the appearing variables in increasing original-index order, map them to $1,dots,n$, and retain the inverse map. Keep the original clause order and literal occurrences. Repeat the first literal of each nonempty short clause until it has three positions. This preserves disjunction truth, gives $n,m>=1$, and never introduces a fictitious vertex for a missing literal. Let $Y_(i,j)$ denote the literal at position $j$ of clause $i$, allowing repeated literals. + _Normalization._ An empty conjunction is true; output the empty graph with bound zero. Otherwise collect the appearing variables in increasing original-index order, map them to $1,dots,n$, and retain the inverse map. Keep the original clause order and literal occurrences, which gives $n,m>=1$. Let $Y_(i,j)$ denote the literal at position $j$ of clause $i$, allowing repeated literals. _DAG construction._ Put $b=max(2n-m,0)$ and $K=3m+4n+1+b$. Arcs $(v,u)$ mean that $v$ depends on $u$. Create the following disjoint families, with one-based subscripts: $ |A|=2n+1, quad |B|=b, quad |C|=m, quad F={f_(i,j):1<=i<=m,1<=j<=3}, $ @@ -18305,13 +18295,13 @@ The following table shows concrete target-variable counts for example instances, *Multiplicity:* The fixture stores one canonical witness. The formula has multiple satisfying assignments; each induces at least one $k$-clique by choosing one true literal per clause. ], )[ - Karp's literal-compatibility construction @karp1972 is extended with an anchor and, when needed, isolated padding. This keeps the same endpoint and handles both empty formulas and the shorter clauses accepted by the native `new_allow_less` API. + Karp's literal-compatibility construction @karp1972 is extended with an anchor vertex, so the empty formula maps to a one-vertex clique instance. ][ - _Construction._ Let $m$ be the clause count and $t=sum_j |C_j|$ the actual occurrence count. Number literal vertices in clause/position order, with stored variable indices and polarities. Set $N=max(t,m)+1$, $k=m+1$, and anchor $a=t$. Connect two literal vertices iff they come from different clauses and are not opposite polarities of the same variable; then connect $a$ to all literal vertices. Any remaining vertices are isolated. Thus $1<=k<=N$, $N<=3m+1$, and the edge count is at most $9m^2+3m$. + _Construction._ Let $m$ be the clause count. Number the $3m$ literal occurrences in clause/position order, with stored variable indices and polarities. Set $N=3m+1$, $k=m+1$, and anchor $a=3m$. Connect two literal vertices iff they come from different clauses and are not opposite polarities of the same variable; then connect $a$ to all literal vertices. Thus $1<=k<=N$ and the edge count is at most $9m^2+3m$. - _Correctness._ A satisfying assignment selects a true occurrence from each clause; these mutually compatible vertices and the anchor form a $k$-clique. Conversely, the literal subgraph contains at most one vertex per clause in a clique, hence has clique number at most $m$. For $m>0$, any clique of size at least $k>=2$ excludes padding isolates and must contain the anchor plus one occurrence from every clause. Their polarities consistently satisfy all clauses. An empty clause prevents such a clique. For $m=0$, the target is a single anchor with $k=1$, and every source assignment satisfies the empty conjunction. + _Correctness._ A satisfying assignment selects a true occurrence from each clause; these mutually compatible vertices and the anchor form a $k$-clique. Conversely, the literal subgraph contains at most one vertex per clause in a clique, hence has clique number at most $m$. For $m>0$, any clique of size at least $k>=2$ must contain the anchor plus one occurrence from every clause. Their polarities consistently satisfy all clauses. For $m=0$, the target is a single anchor with $k=1$, and every source assignment satisfies the empty conjunction. - _Solution extraction._ Validate the complete target selection and its true clique predicate first. Decode the literal vertices via their stored source indices and signs, leaving unselected variables false; ignore the nonliteral anchor and padding by the defined mapping. Checked occurrence and output counts precede allocation. Formal `CNFClause::variables` supplies validated indices. Normal CLI/serde still requires exactly three literals per actual clause; native short-clause support does not change variants or serialization. + _Solution extraction._ Validate the complete target selection and its true clique predicate first. Decode the literal vertices via their stored source indices and signs, leaving unselected variables false; ignore the anchor by the defined mapping. Checked vertex and output counts precede allocation. Formal `CNFClause::variables` supplies validated indices. ] #let ksat_co = load-example("KSatisfiability", "CyclicOrdering") @@ -18340,7 +18330,7 @@ The following table shows concrete target-variable counts for example instances, )[ This reduction @galilMegiddo1977 first normalizes clauses to three distinct, globally ordered variables. With $s$ declared source variables and $c$ source clauses it produces at most $3s + 26c + 3$ elements and $40c + 2$ cyclic-order constraints. The original ten-constraint gadget is applied to the normalized formula. ][ - _Normalization._ An empty clause maps to the fixed NO target on three elements with constraints $(0,1,2)$ and $(0,2,1)$. Otherwise remove repeated literals within each clause and discard clauses containing both signs of a variable. Compact the remaining appearing variables in increasing original-index order, retaining the inverse map. Replace a two-literal clause $(a or b)$ by $(a or b or u) and (a or b or not u)$ with fresh $u$. Replace a unit clause $a$ by the four clauses $(a or (plus.minus u) or (plus.minus v))$ over both independent signs, with fresh $u,v$. These conjunctions are true for every auxiliary assignment when the original clause is true and false for at least one constituent clause under every auxiliary assignment when the original clause is false. Every resulting clause has three distinct variables; order its literals by increasing variable index. If no clauses remain, use the one-element unconstrained YES target. + _Normalization._ Remove repeated literals within each clause and discard clauses containing both signs of a variable. Compact the remaining appearing variables in increasing original-index order, retaining the inverse map. Replace a two-literal clause $(a or b)$ by $(a or b or u) and (a or b or not u)$ with fresh $u$. Replace a unit clause $a$ by the four clauses $(a or (plus.minus u) or (plus.minus v))$ over both independent signs, with fresh $u,v$. These conjunctions are true for every auxiliary assignment when the original clause is true and false for at least one constituent clause under every auxiliary assignment when the original clause is false. Every resulting clause has three distinct variables; order its literals by increasing variable index. If no clauses remain, use the one-element unconstrained YES target. _Construction._ Let the normalized formula have $N$ variables and $M$ clauses. For each variable $x_i$, create three target elements $alpha_i, beta_i, gamma_i$. A positive literal has associated triple $(alpha_i,beta_i,gamma_i)$; a negative literal has $(alpha_i,gamma_i,beta_i)$. For each normalized clause, let its three literal triples be $(a,b,c)$, $(d,e,f)$, $(g,h,i)$ in increasing variable order. Add five fresh elements $j,k,l,m,n$ and the ten constraints $ @@ -18400,7 +18390,7 @@ The following table shows concrete target-variable counts for example instances, )[ Ullman's reduction first builds a variable-capacity unit-task scheduling instance for 3-SAT, then pads each time slot with chained filler jobs so a fixed number of processors simulates the desired capacity profile. Because every task has length $1$, preemption is irrelevant: the resulting instance is already a valid preemptive scheduling instance whose optimal makespan is at most $T = n + 3$ iff the formula is satisfiable @ullman1975 @garey1979. ][ - Short nonempty clauses are padded by repeating literals. An empty conjunction maps to one unit task with threshold 1; a formula containing an empty clause maps to the same task with threshold 0. The following construction handles the remaining instances. + An empty conjunction maps to one unit task with threshold 1. The following construction handles the remaining instances. _Construction._ Let $phi$ be a 3-CNF formula with variables $x_1, dots, x_n$ and clauses $C_1, dots, C_m$. Create unit jobs $x_(i,j)$ and $overline(x)_(i,j)$ for $1 <= i <= n$ and $0 <= j <= n$, plus forcing jobs $y_i, overline(y)_i$, and clause jobs $D_(r,s)$ for $1 <= r <= m$, $1 <= s <= 7$. Add chain precedences $x_(i,j) prec x_(i,j+1)$ and $overline(x)_(i,j) prec overline(x)_(i,j+1)$, and branching precedences $x_(i,i-1) prec y_i$, $overline(x)_(i,i-1) prec overline(y)_i$. Set $T = n + 3$ and slot capacities $c_0 = n$, $c_1 = 2n + 1$, $c_t = 2n + 2$ for $2 <= t <= n$, $c_(n+1) = m + n + 1$, and $c_(n+2) = 6m$. For each clause $C_r = (ell_1 or ell_2 or ell_3)$ and each nonzero bit pattern $b in {1, dots, 7}$, create clause job $D_(r,b)$. Its predecessors are the three chain endpoints chosen according to the bits of $b$: for literal position $k$, use the endpoint of $ell_k$ when bit $k$ is 1 and of $not ell_k$ when bit $k$ is 0. This makes exactly one clause job per clause ready one slot earlier when the clause is satisfied. @@ -18483,7 +18473,7 @@ The following table shows concrete target-variable counts for example instances, _Solution extraction._ Validate the target partition, select precisely those vertex items sharing the label of $s$, and invoke the formal clique-to-SAT extractor. This mapping is independent of the numerical names of partition blocks. - _Overhead._ There are exactly $h+e+2$ vertices and $2h+4e$ arcs. With $m$ source clauses, $h<=3m+1$ and $e<=9m(m-1)/2+3m$, including native short or empty clauses. Thus target sizes are at most $(9m^2+3m+6)/2$ vertices and $18m^2+2$ arcs. The construction checks representability of counts and signed integer coefficients before allocating its incidence graph. + _Overhead._ There are exactly $h+e+2$ vertices and $2h+4e$ arcs. With $m$ source clauses, $h<=3m+1$ and $e<=9m(m-1)/2+3m$. Thus target sizes are at most $(9m^2+3m+6)/2$ vertices and $18m^2+2$ arcs. The construction checks representability of counts and signed integer coefficients before allocating its incidence graph. ] #let hc_bicon = load-example("HamiltonianCircuit", "BiconnectivityAugmentation") @@ -19010,7 +19000,7 @@ The following table shows concrete target-variable counts for example instances, #reduction-rule("KSatisfiability", "BicliqueCover")[ Polynomial reduction (Chandran, Issac, and Karrenbauer, IPEC 2016 @chandran_et_al:LIPIcs.IPEC.2016.11) from 3-SAT to BicliqueCover with logarithmic rank. Each appearing source variable is split into a positive/negative pair $(t_i, f_i)$, exactly-one clauses tie them to opposite truth values, and the formula is padded so that $n = 2^ell$ normalized variables admit a balanced satisfying assignment with exactly $n / 2$ true variables. The construction then assembles a bipartite gadget whose biclique cover rank equals $k_f + 2 ell + 2$ iff the (normalized) formula is satisfiable. ][ - _Construction._ Let $psi$ have $n_s$ declared variables and $m_s$ clauses. The native Rust API also permits clauses of at most three literals. An empty clause maps to a single-edge, rank-zero NO target. A formula with no clauses maps to an empty, rank-zero YES target. Otherwise compact the $a$ variables that actually appear, recording their original indices, and repeat one literal in each nonempty short clause to obtain exactly three positions. Repetition preserves disjunction, and absent variables may be assigned false in the inverse map. *Normalize* this compact formula: + _Construction._ Let $psi$ have $n_s$ declared variables and $m_s$ three-literal clauses. A formula with no clauses maps to an empty, rank-zero YES target. Otherwise compact the $a$ variables that actually appear, recording their original indices; absent variables may be assigned false in the inverse map. *Normalize* this compact formula: $ "vars:" quad & "introduce" t_i, f_i "for each appearing" x_i "and pad to" n = 2^ell "variables" \ "clauses:" quad & "replace literal" x_i "by" t_i ";" not x_i "by" f_i \ @@ -19185,7 +19175,7 @@ The following table shows concrete target-variable counts for example instances, )[ This reduction uses variable digons and clause three-cycles, following the kernel hardness approach of @chvatal1973. With $a$ appearing variables, $m$ clauses and $L$ literal occurrences, the target has $2a + 3m$ vertices and $2a + 3m + L$ arcs. These are bounded by $2n + 3m$ and $2n + 6m$ on the native source domain. Each occurrence has its own clause vertex; kernels may include clause vertices as well as literals. ][ - _Construction._ Collect the sorted original indices $J$ of appearing variables, with $a = |J|$. For each compact variable $i$, create literal vertices $p_i, n_i$ and both digon arcs. Each native clause has zero through three literals. Create three vertices $c_(j,0), c_(j,1), c_(j,2)$ and the directed cycle in that order, then add $(c_(j,t), v(ell_(j,t)))$ only for its actual literal positions. Repeated literals keep separate occurrence vertices. An empty clause therefore produces a three-cycle with no outgoing literal arcs, which has no kernel; an empty formula produces an empty graph, whose empty selection is a kernel. No padding is needed. + _Construction._ Collect the sorted original indices $J$ of appearing variables, with $a = |J|$. For each compact variable $i$, create literal vertices $p_i, n_i$ and both digon arcs. For each clause create three vertices $c_(j,0), c_(j,1), c_(j,2)$ and the directed cycle in that order, then add $(c_(j,t), v(ell_(j,t)))$ for its three literal positions. Repeated literals keep separate occurrence vertices. An empty formula produces an empty graph, whose empty selection is a kernel. _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, choose its true literal in each digon. Let $t_r$ indicate whether the literal at clause position $r$ is selected, with missing positions set to false. Select clause vertex $r$ exactly when $not t_r and t_((r+1) mod 3)$. A selected vertex points to no selected literal, and its successor cannot be selected, so independence holds. An unselected vertex with $t_r$ true is absorbed through its literal arc. Otherwise both $t_r$ and $t_((r+1) mod 3)$ are false. Since the clause is satisfied, $t_((r+2) mod 3)$ is true; its cycle successor is therefore selected and absorbs it. Unselected literal vertices are absorbed by their digon partners. @@ -19193,7 +19183,7 @@ The following table shows concrete target-variable counts for example instances, _Solution extraction._ Validate the target selection once using the formal target evaluator and reject $"Or(false)"$. Initialize a length-$n$ false vector and restore each original position $J_i$ from the selection of $p_i$. Unused variables remain false; selected clause vertices are ignored. The concrete value types are $"Or" arrow.r "Or"$. - _Bounds and native arithmetic._ Since $a <= L <= 3m$, the target has at most $9m$ vertices and $12m$ arcs. The registered relations use upper bounds in the declared source parameters, covering sparse variables and short clauses. Counts are checked before allocation, and every vertex index is bounded by the checked total. A successfully allocated native clause vector also bounds $m$ by its element layout and the address space; original sparse indices are never doubled. Allocation limits do not represent mathematical infeasibility. + _Bounds and native arithmetic._ Since $a <= L <= 3m$, the target has at most $9m$ vertices and $12m$ arcs. The registered relations use upper bounds in the declared source parameters, covering sparse variables. Counts are checked before allocation, and every vertex index is bounded by the checked total. A successfully allocated native clause vector also bounds $m$ by its element layout and the address space; original sparse indices are never doubled. Allocation limits do not represent mathematical infeasibility. ] diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index 05edafeb9..13a3bd934 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -507,17 +507,17 @@ mod tests { let cli = Cli::try_parse_from([ "pred", "create", - "3SAT", + "2SAT", "--num-vars", "3", "--clauses", - "1,2,3", + "1,2", ]) .expect("variant alias parses"); let Commands::Create(args) = cli.command else { panic!("expected create command"); }; - assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K3")); + assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K2")); assert_eq!(args.raw("num-vars"), Some("3")); } diff --git a/src/models/formula/ksat.rs b/src/models/formula/ksat.rs index dede5be57..6d2e9bb7c 100644 --- a/src/models/formula/ksat.rs +++ b/src/models/formula/ksat.rs @@ -7,7 +7,7 @@ use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension}; use crate::traits::Problem; -use crate::variant::{KValue, K2, K3, KN}; +use crate::variant::{KValue, K2, K3}; use serde::{de::Error as _, Deserialize, Deserializer, Serialize}; use super::{sat::validate_cnf_literals, CNFClause}; @@ -53,7 +53,7 @@ inventory::submit! { name: "KSatisfiability", display_name: "K-Satisfiability", aliases: &["KSAT"], - dimensions: &[VariantDimension::new("k", "KN", &["KN", "K2", "K3"])], + dimensions: &[VariantDimension::new("k", "K3", &["K3", "K2"])], category: crate::registry::ProblemCategory::Formula, module_path: module_path!(), description: "SAT with exactly k literals per clause", @@ -124,63 +124,24 @@ impl KSatisfiability { /// Create a new K-SAT problem. /// /// # Panics - /// Panics if any clause does not have exactly K literals (when K is a - /// concrete value like K2, K3). When K is KN (arbitrary), no clause-length - /// validation is performed. + /// Panics if any clause does not have exactly K literals. pub fn new(num_vars: usize, clauses: Vec) -> Self { Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}")) } - /// Create a K-SAT problem after validating its clauses. + /// Create a K-SAT problem after validating that every clause has exactly + /// K literals. pub fn try_new( num_vars: usize, clauses: Vec, ) -> Result { validate_cnf_literals(num_vars, &clauses)?; - if let Some(k) = K::K { - for (i, clause) in clauses.iter().enumerate() { - if clause.len() != k { - return Err( - format!("Clause {i} has {} literals, expected {k}", clause.len()).into(), - ); - } - } - } - Ok(Self { - num_vars, - clauses, - _phantom: std::marker::PhantomData, - }) - } - - /// Create a new K-SAT problem allowing clauses with fewer than K literals. - /// - /// This is useful when the reduction algorithm produces clauses with - /// fewer literals (e.g., when allow_less is true in the Julia implementation). - /// - /// # Panics - /// Panics if any clause has more than K literals (when K is a concrete - /// value like K2, K3). When K is KN (arbitrary), no clause-length - /// validation is performed. - pub fn new_allow_less(num_vars: usize, clauses: Vec) -> Self { - Self::try_new_allow_less(num_vars, clauses).unwrap_or_else(|message| panic!("{message}")) - } - - /// Create a K-SAT problem with shorter clauses after validation. - pub fn try_new_allow_less( - num_vars: usize, - clauses: Vec, - ) -> Result { - validate_cnf_literals(num_vars, &clauses)?; - if let Some(k) = K::K { - for (i, clause) in clauses.iter().enumerate() { - if clause.len() > k { - return Err(format!( - "Clause {i} has {} literals, expected at most {k}", - clause.len() - ) - .into()); - } + let k = K::K.ok_or("KSatisfiability requires a fixed clause width K")?; + for (i, clause) in clauses.iter().enumerate() { + if clause.len() != k { + return Err( + format!("Clause {i} has {} literals, expected {k}", clause.len()).into(), + ); } } Ok(Self { @@ -273,13 +234,11 @@ impl crate::solvers::BruteForceProblem for KSatisfiability { } crate::declare_variants! { - default KSatisfiability => "2^num_vars", + default KSatisfiability => "1.307^num_vars" aliases ["3SAT"], KSatisfiability => "num_vars + num_clauses" aliases ["2SAT"], - KSatisfiability => "1.307^num_vars" aliases ["3SAT"], } crate::register_brute_force! { - KSatisfiability decode |_, indices: Vec| crate::config::config_to_bits(&indices), KSatisfiability decode |_, indices: Vec| crate::config::config_to_bits(&indices), KSatisfiability decode |_, indices: Vec| crate::config::config_to_bits(&indices), } diff --git a/src/rules/ksatisfiability_bicliquecover.rs b/src/rules/ksatisfiability_bicliquecover.rs index dec116ab8..b26e9f457 100644 --- a/src/rules/ksatisfiability_bicliquecover.rs +++ b/src/rules/ksatisfiability_bicliquecover.rs @@ -5,8 +5,7 @@ //! //! 1. **Normalize** the source 3-CNF formula: //! - Compact the variables appearing in clauses, retaining the inverse map. -//! Repeat literals to pad nonempty short clauses to three positions. -//! Empty formulas and empty clauses map to fixed YES and NO targets. +//! The empty formula maps to a fixed YES target. //! - For each appearing variable `x_i`, create two normalized variables //! `t_i` and `f_i`. Replace literal `x_i` by `t_i`, replace literal //! `¬x_i` by `f_i`. Add exactly-one clauses @@ -205,9 +204,6 @@ fn normalize( translated.push(f_lit(compact)?); } } - // Nonempty short clauses are equivalent after repeating a literal. - // Empty clauses are handled by the fixed NO construction before here. - translated.resize(3, translated[0]); clauses.push(translated); } @@ -233,7 +229,7 @@ fn free_edge_budget(ell: usize, m: usize) -> Option { // With s source variables and m source clauses, the normalized counts // satisfy n <= 4(s+1), M <= m+4(s+1), ell <= s+1, ceil(log2 M) <= M. // Hence each partition is <= 31s+5m+39 and rank <= 14s+2m+22. -// The declared coarser bounds also cover the fixed YES and NO targets. +// The declared coarser bounds also cover the fixed YES target. #[crate::aggregate_reduction] impl crate::rules::AggregateReductionResult for ReductionKSatisfiabilityToBicliqueCover { type Source = KSatisfiability; @@ -261,21 +257,10 @@ impl ReduceTo for KSatisfiability { fn reduce_to(&self) -> Result { // ---------------- Stage 1: normalize ---------------- let source_num_vars = self.num_vars(); - let has_empty_clause = self - .clauses() - .iter() - .any(|clause| clause.literals.is_empty()); - if has_empty_clause || self.clauses().is_empty() { - // The empty conjunction is YES; a conjunction with an empty - // disjunction is NO. Zero bicliques cover only the empty graph. - let size = usize::from(has_empty_clause); - let edges = if has_empty_clause { - vec![(0, 0)] - } else { - vec![] - }; + if self.clauses().is_empty() { + // The empty conjunction is YES: zero bicliques cover the empty graph. return Ok(ReductionKSatisfiabilityToBicliqueCover { - target: BicliqueCover::new(BipartiteGraph::new(size, size, edges), 0), + target: BicliqueCover::new(BipartiteGraph::new(0, 0, vec![]), 0), source_num_vars, normalized_n: 0, s1_left_offset: 0, diff --git a/src/rules/ksatisfiability_casts.rs b/src/rules/ksatisfiability_casts.rs deleted file mode 100644 index 898c324fa..000000000 --- a/src/rules/ksatisfiability_casts.rs +++ /dev/null @@ -1,26 +0,0 @@ -//! Variant reductions for KSatisfiability. - -use crate::impl_variant_reduction; -use crate::models::formula::KSatisfiability; -use crate::variant::{K2, K3, KN}; - -impl_variant_reduction!( - KSatisfiability, - => , - fields: [num_vars, num_clauses, num_literals], - |src| KSatisfiability::new_allow_less(src.num_vars(), src.clauses().to_vec()) -); - -impl_variant_reduction!( - KSatisfiability, - => , - fields: [num_vars, num_clauses, num_literals], - |src| KSatisfiability::new_allow_less(src.num_vars(), src.clauses().to_vec()) -); - -crate::register_aggregate_reduction!( - crate::rules::VariantReductionResult, KSatisfiability> -); -crate::register_aggregate_reduction!( - crate::rules::VariantReductionResult, KSatisfiability> -); diff --git a/src/rules/ksatisfiability_cyclicordering.rs b/src/rules/ksatisfiability_cyclicordering.rs index 313728a7e..5ee098cf3 100644 --- a/src/rules/ksatisfiability_cyclicordering.rs +++ b/src/rules/ksatisfiability_cyclicordering.rs @@ -9,10 +9,11 @@ //! "true" one. //! //! Before applying the gadget, remove tautologies and repeated literals, -//! compact occurring variables, and expand short clauses with fresh variables. -//! Each resulting clause has three distinct variables in global index order. -//! This is the hypothesis needed to combine the paper's local cyclic orders. -//! Empty clauses and empty conjunctions map to fixed NO and YES targets. +//! compact occurring variables, and expand clauses left with fewer than three +//! distinct literals using fresh variables. Each resulting clause has three +//! distinct variables in global index order. This is the hypothesis needed to +//! combine the paper's local cyclic orders. The empty conjunction maps to a +//! fixed YES target. //! //! Reference: Galil and Megiddo, "Cyclic ordering is NP-complete", 1977. @@ -138,18 +139,21 @@ fn normalize( match *literals.as_slice() { [a, b, c] => normalized.push([a, b, c]), [a, b] => { - let u = variables.allocate() - .map_err( as ReduceTo>::target_construction)?; + let u = variables.allocate().map_err( + as ReduceTo>::target_construction, + )?; normalized.extend([[a, b, u], [a, b, -u]]); } [a] => { - let u = variables.allocate() - .map_err( as ReduceTo>::target_construction)?; - let v = variables.allocate() - .map_err( as ReduceTo>::target_construction)?; + let u = variables.allocate().map_err( + as ReduceTo>::target_construction, + )?; + let v = variables.allocate().map_err( + as ReduceTo>::target_construction, + )?; normalized.extend([[a, u, v], [a, u, -v], [a, -u, v], [a, -u, -v]]); } - _ => unreachable!("empty clauses are handled before normalization; native clauses have at most three literals"), + _ => unreachable!("deduplicated three-literal clauses keep one to three literals"), } } // Original compact indices precede all fresh indices. Every emitted @@ -174,18 +178,6 @@ impl ReduceTo for KSatisfiability { type Result = Reduction3SATToCyclicOrdering; fn reduce_to(&self) -> Result { - if self - .clauses() - .iter() - .any(|clause| clause.literals.is_empty()) - { - return Ok(Reduction3SATToCyclicOrdering { - target: CyclicOrdering::try_new(3, vec![(0, 1, 2), (0, 2, 1)]) - .map_err(>::target_construction)?, - source_num_vars: self.num_vars(), - source_variables: Vec::new(), - }); - } let normalized = normalize(self)?; let num_vars = normalized.num_vars; let num_clauses = normalized.clauses.len(); diff --git a/src/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/rules/ksatisfiability_decisionminimumvertexcover.rs index 071c53240..ec37318f2 100644 --- a/src/rules/ksatisfiability_decisionminimumvertexcover.rs +++ b/src/rules/ksatisfiability_decisionminimumvertexcover.rs @@ -68,10 +68,9 @@ impl ReductionResult for Reduction3SATToDecisionMVC { impl crate::rules::AggregateReductionResult for Reduction3SATToDecisionMVC {} #[reduction( - transform = { - exact { num_vertices = "2 * num_vars + 3 * num_clauses" }, - // A clause with fewer than three literals links fewer triangle corners. - upper_bound { num_edges = "num_vars + 6 * num_clauses" }, + transform = exact { + num_vertices = "2 * num_vars + 3 * num_clauses", + num_edges = "num_vars + 6 * num_clauses", } )] impl ReduceTo>> for KSatisfiability { @@ -100,12 +99,7 @@ impl ReduceTo>> for KSatisfiabilit edges.push((base, base + 2)); // Communication edges: connect triangle vertex k to the literal vertex - for k in 0..3 { - if clause.literals.is_empty() { - continue; - } - // Repeating a literal pads a short clause without changing it. - let lit = clause.literals[k % clause.literals.len()]; + for (k, &lit) in clause.literals.iter().enumerate() { let var_idx = lit.unsigned_abs() as usize - 1; // 0-indexed variable let literal_vertex = if lit > 0 { 2 * var_idx // positive literal vertex @@ -123,18 +117,10 @@ impl ReduceTo>> for KSatisfiabilit Ok(Reduction3SATToDecisionMVC { target: Decision::new( target, - if self - .clauses() - .iter() - .any(|clause| clause.literals.is_empty()) - { - -1 // No nonnegative vertex-cover size can satisfy an empty clause. - } else { - >>>::exact_i64( - n + 2 * m, - "computing the cover bound", - )? - }, + >>>::exact_i64( + n + 2 * m, + "computing the cover bound", + )?, ), source_num_vars: n, }) diff --git a/src/rules/ksatisfiability_feasibleregisterassignment.rs b/src/rules/ksatisfiability_feasibleregisterassignment.rs index c7e20a609..f4ed96f3b 100644 --- a/src/rules/ksatisfiability_feasibleregisterassignment.rs +++ b/src/rules/ksatisfiability_feasibleregisterassignment.rs @@ -1,9 +1,8 @@ //! Reduction from KSatisfiability (3-SAT) to Feasible Register Assignment. //! //! This follows Sethi's Reduction 3 / Theorem 5.11 (STOC 1973): -//! Nonempty short clauses are padded by literal repetition, an empty clause -//! maps to a fixed infeasible DAG, and appearing variables are compacted with -//! an inverse map. No ordering or distinct-variable hypothesis is needed. +//! Appearing variables are compacted with an inverse map. No ordering or +//! distinct-variable hypothesis is needed. //! - Variable leaf pairs `s_pos[k], s_neg[k]` share register `S[k]` //! - Each literal occurrence adds `p[i,j], q[i,j], r[i,j], rbar[i,j]` //! - `r[i,j]` and `rbar[i,j]` share register `R[i,j]` @@ -109,19 +108,6 @@ impl ReduceTo for KSatisfiability { type Result = Reduction3SATToFeasibleRegisterAssignment; fn reduce_to(&self) -> Result { - if self - .clauses() - .iter() - .any(|clause| clause.literals.is_empty()) - { - // Both predecessors must remain live until vertex 2, but they - // share a register. This acyclic target has no realization. - return Ok(Reduction3SATToFeasibleRegisterAssignment { - target: FeasibleRegisterAssignment::new(3, vec![(2, 0), (2, 1)], 2, vec![0, 0, 1]), - num_vars: self.num_vars(), - source_variables: Vec::new(), - }); - } let source_variables: Vec<_> = self .clauses() .iter() @@ -166,10 +152,9 @@ impl ReduceTo for KSatisfiability { } for (clause_idx, clause) in self.clauses().iter().enumerate() { - // Repetition preserves a nonempty disjunction. Every occurrence - // keeps its own gadget and register pair, even for repeated literals. - let mut literals = clause.literals.clone(); - literals.resize(3, literals[0]); + // Every occurrence keeps its own gadget and register pair, even + // for repeated literals. + let literals = &clause.literals; for literal_pos in 0..3 { assignment[p_idx(num_vars, clause_idx, literal_pos)] = p_register(num_vars, clause_idx, literal_pos); diff --git a/src/rules/ksatisfiability_kclique.rs b/src/rules/ksatisfiability_kclique.rs index 2952e3326..ceec31431 100644 --- a/src/rules/ksatisfiability_kclique.rs +++ b/src/rules/ksatisfiability_kclique.rs @@ -1,10 +1,8 @@ //! Karp's literal-compatibility construction with a universal vertex. //! -//! Use actual literal occurrences, including shorter clauses accepted by -//! KSatisfiability::new_allow_less. For m clauses and t occurrences, create -//! max(t,m)+1 vertices and request a clique of size m+1. Vertex t is adjacent -//! to all literal vertices; remaining padding vertices are isolated. This -//! uniformly represents empty formulas and formulas containing empty clauses. +//! For m clauses, create one vertex per literal occurrence plus an anchor +//! (3m+1 vertices) and request a clique of size m+1. The anchor is adjacent to +//! every literal vertex, so the empty formula maps to the one-vertex clique. use crate::models::formula::KSatisfiability; use crate::models::graph::KClique; @@ -58,20 +56,18 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToKClique {} #[reduction( transform = { - exact { k = "num_clauses + 1" }, - // Clauses built with `new_allow_less` may have fewer than three literals. - upper_bound { + exact { + k = "num_clauses + 1", num_vertices = "3 * num_clauses + 1", - num_edges = "9 * num_clauses^2 + 3 * num_clauses", }, + upper_bound { num_edges = "9 * num_clauses^2 + 3 * num_clauses" }, } )] impl ReduceTo> for KSatisfiability { type Result = Reduction3SATToKClique; fn reduce_to(&self) -> Result { - let (num_vertices, k) = - clique_sizes(self.num_clauses(), self.clauses().iter().map(|c| c.len()))?; + let (num_vertices, k) = clique_sizes(self.num_clauses())?; // CNFClause::variables performs the formal literal-to-index conversion; // the source constructor has already validated its range and polarity. let positions: Vec<_> = self @@ -104,22 +100,18 @@ impl ReduceTo> for KSatisfiability { } } -/// Check occurrence and output counts before allocating the compatibility graph. -fn clique_sizes( - m: usize, - lengths: impl IntoIterator, -) -> Result<(usize, usize), crate::rules::ReductionError> { - let overflow = || { - crate::rules::ReductionError::integer_overflow::, KClique>( - "counting SAT clique occurrences and auxiliary vertices", - ) - }; - let t = lengths - .into_iter() - .try_fold(0usize, |sum, len| sum.checked_add(len)) - .ok_or_else(overflow)?; - let vertices = t.max(m).checked_add(1).ok_or_else(overflow)?; - // m+1 <= max(t,m)+1, whose representability was checked above. +/// Check the vertex and clique sizes before allocating the compatibility graph. +fn clique_sizes(m: usize) -> Result<(usize, usize), crate::rules::ReductionError> { + let vertices = m + .checked_mul(3) + .and_then(|t| t.checked_add(1)) + .ok_or_else(|| { + crate::rules::ReductionError::integer_overflow::< + KSatisfiability, + KClique, + >("counting SAT clique literal and anchor vertices") + })?; + // m+1 <= 3m+1, whose representability was checked above. Ok((vertices, m + 1)) } diff --git a/src/rules/ksatisfiability_kernel.rs b/src/rules/ksatisfiability_kernel.rs index cef509831..2c3c1dc44 100644 --- a/src/rules/ksatisfiability_kernel.rs +++ b/src/rules/ksatisfiability_kernel.rs @@ -2,8 +2,8 @@ //! //! This is Chvatal's 1973 construction using variable digons and clause //! 3-cycles with arcs to literal vertices. Appearing variables are compacted -//! with an inverse map; native clauses of length zero through three keep -//! their original occurrence arcs, including the empty clause's kernel-free cycle. +//! with an inverse map; each clause keeps its three occurrence arcs, including +//! repeated literals. use crate::models::formula::KSatisfiability; use crate::models::graph::Kernel; diff --git a/src/rules/ksatisfiability_preemptivescheduling.rs b/src/rules/ksatisfiability_preemptivescheduling.rs index c3d799ced..7d3291e2f 100644 --- a/src/rules/ksatisfiability_preemptivescheduling.rs +++ b/src/rules/ksatisfiability_preemptivescheduling.rs @@ -4,8 +4,8 @@ //! scheduling instance. Since every task has length 1, preemption is inert: //! the constructed instance is a valid preemptive scheduling problem whose //! optimal makespan hits the threshold `T = num_vars + 3` iff a nontrivial -//! 3-SAT instance is satisfiable. Empty formulas and empty clauses use a -//! one-task instance with bound 1 and 0 respectively. +//! 3-SAT instance is satisfiable. The empty formula uses a one-task instance +//! with bound 1. //! //! Reference: Jeffrey D. Ullman, "NP-complete scheduling problems", JCSS 10, //! 1975; Garey & Johnson, Appendix A5.2. @@ -147,8 +147,7 @@ fn build_ullman_construction(source: &KSatisfiability) -> UllmanConstruction for (clause_index, clause) in source.clauses().iter().enumerate() { for (pattern_index, &clause_job) in clause_jobs[clause_index].iter().enumerate() { let pattern = pattern_index + 1; - // Repeating literals preserves shorter nonempty disjunctions. - for (position, &literal) in clause.literals.iter().cycle().take(3).enumerate() { + for (position, &literal) in clause.literals.iter().enumerate() { let bit_is_one = ((pattern >> (2 - position)) & 1) == 1; precedences.push(( literal_endpoint( @@ -202,7 +201,7 @@ fn clause_pattern_for_assignment( assignment: &[bool], ) -> usize { let mut pattern = 0usize; - for (position, &literal) in clause.literals.iter().cycle().take(3).enumerate() { + for (position, &literal) in clause.literals.iter().enumerate() { let variable = literal.unsigned_abs() as usize - 1; let value = assignment[variable]; let literal_true = if literal > 0 { value } else { !value }; @@ -219,11 +218,8 @@ fn construct_schedule_from_assignment( assignment: &[bool], source: &KSatisfiability, ) -> Option>> { - if source.num_clauses() == 0 || source.clauses().iter().any(|c| c.literals.is_empty()) { - return crate::traits::Problem::evaluate(source, &assignment.to_vec()) - .unwrap() - .0 - .then(|| vec![vec![true]]); + if source.num_clauses() == 0 { + return (assignment.len() == source.num_vars()).then(|| vec![vec![true]]); } let construction = build_ullman_construction(source); if assignment.len() != source.num_vars() || target.num_tasks() != construction.num_jobs { @@ -383,14 +379,13 @@ impl ReduceTo for KSatisfiability { type Result = Reduction3SATToPreemptiveScheduling; fn reduce_to(&self) -> Result { - let has_empty_clause = self.clauses().iter().any(|c| c.literals.is_empty()); - if self.num_clauses() == 0 || has_empty_clause { - // A one-task schedule meets bound 1, but cannot meet bound 0. + if self.num_clauses() == 0 { + // The empty conjunction is YES: a one-task schedule meets bound 1. return Ok(Reduction3SATToPreemptiveScheduling { target: PreemptiveScheduling::new(vec![1], 1, vec![]) .map_err(>::target_construction)?, positive_start_jobs: vec![0; self.num_vars()], - threshold: usize::from(!has_empty_clause), + threshold: 1, }); } let construction = build_ullman_construction(self); diff --git a/src/rules/ksatisfiability_qubo.rs b/src/rules/ksatisfiability_qubo.rs index f6d4d2337..c7ab13983 100644 --- a/src/rules/ksatisfiability_qubo.rs +++ b/src/rules/ksatisfiability_qubo.rs @@ -278,8 +278,8 @@ fn add_3sat_clause_penalty( } /// Expand clause penalties and retain the constant omitted by QUBO. -/// K3 reserves one auxiliary per clause, including free auxiliaries for short -/// clauses; K2 reserves none. The source constructor validates clause widths. +/// K3 reserves one auxiliary per clause; K2 reserves none. The source +/// constructor guarantees every clause has exactly K literals. fn build_qubo_matrix( num_vars: usize, clauses: &[crate::models::formula::CNFClause], @@ -301,20 +301,15 @@ fn build_qubo_matrix( .map(|(variable, &literal)| (variable, literal < 0)) .collect(); let offset = match literals.as_slice() { - [] => 1, - &[(v, neg)] => { - add_coefficient(&mut matrix, v, v, if neg { 1 } else { -1 })?; - i64::from(!neg) - } - &[(_, n1), (_, n2)] => { + [(_, n1), (_, n2)] => { add_2sat_clause_penalty(&mut matrix, &literals)?; i64::from(!n1 && !n2) } - &[(_, n1), (_, n2), _] => { + [(_, n1), (_, n2), _] => { add_3sat_clause_penalty(&mut matrix, &literals, num_vars + idx)?; 2 * i64::from(!n1 && !n2) } - _ => unreachable!("the source validates clause width at most three"), + _ => unreachable!("the source validates clause width two or three"), }; constant = constant .checked_add(offset) diff --git a/src/rules/ksatisfiability_registersufficiency.rs b/src/rules/ksatisfiability_registersufficiency.rs index c4acc61c9..537d429dc 100644 --- a/src/rules/ksatisfiability_registersufficiency.rs +++ b/src/rules/ksatisfiability_registersufficiency.rs @@ -1,8 +1,7 @@ //! Reduction from KSatisfiability (3-SAT) to RegisterSufficiency. //! -//! This is Sethi's Reduction I / Theorem 3.11 (STOC 1973), with native -//! empty-formula/empty-clause boundary targets, compact variables, and literal -//! repetition for nonempty short clauses. The corrected extraction +//! This is Sethi's Reduction I / Theorem 3.11 (STOC 1973), with an +//! empty-formula boundary target and compact variables. The corrected extraction //! rule from issue #872: //! - the snapshot is taken immediately after `w[n]` //! - `x_k = true` iff `x_pos[k]` has been computed by that snapshot @@ -337,15 +336,10 @@ impl ReduceTo for KSatisfiability { type Result = Reduction3SATToRegisterSufficiency; fn reduce_to(&self) -> Result { - let empty_clause = self - .clauses() - .iter() - .any(|clause| clause.literals.is_empty()); - if empty_clause || self.num_clauses() == 0 { - // Zero vertices need zero registers (YES); one output vertex - // cannot be computed with zero registers (NO). + if self.num_clauses() == 0 { + // Zero vertices need zero registers (YES). return Ok(Reduction3SATToRegisterSufficiency { - target: RegisterSufficiency::new(usize::from(empty_clause), Vec::new(), 0), + target: RegisterSufficiency::new(0, Vec::new(), 0), layout: None, source_num_vars: self.num_vars(), source_variables: Vec::new(), @@ -378,11 +372,6 @@ impl ReduceTo for KSatisfiability { let variable = i64::try_from(compact + 1).expect("compact SAT indices fit i64"); literals[position] = if literal > 0 { variable } else { -variable }; } - // Repeating a literal preserves a nonempty disjunction. Every - // slot has a real literal and the original first-true lock proof. - for position in clause.literals.len()..3 { - literals[position] = literals[0]; - } literals }) .collect(); diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 5815a32ed..e9d97f464 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -68,7 +68,6 @@ pub(crate) mod kcoloring_twodimensionalconsecutivesets; mod knapsack_qubo; pub(crate) mod ksatisfiability_acyclicpartition; pub(crate) mod ksatisfiability_bicliquecover; -mod ksatisfiability_casts; pub(crate) mod ksatisfiability_cyclicordering; pub(crate) mod ksatisfiability_decisionminimumvertexcover; pub(crate) mod ksatisfiability_directedtwocommodityintegralflow; diff --git a/src/rules/sat_ksat.rs b/src/rules/sat_ksat.rs index fd5607f92..599d6c9b3 100644 --- a/src/rules/sat_ksat.rs +++ b/src/rules/sat_ksat.rs @@ -10,7 +10,7 @@ use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability}; use crate::reduction; use crate::rules::sat_helpers::SatVariableAllocator; use crate::rules::traits::{ReduceTo, ReductionResult}; -use crate::variant::{KValue, K2, K3, KN}; +use crate::variant::{KValue, K2, K3}; /// Result of reducing general SAT to K-SAT. /// @@ -206,7 +206,8 @@ impl ReductionResult for ReductionKSATToSAT { } } -crate::register_aggregate_reduction!(ReductionKSATToSAT); +crate::register_aggregate_reduction!(ReductionKSATToSAT); +crate::register_aggregate_reduction!(ReductionKSATToSAT); #[crate::aggregate_reduction(identity)] impl crate::rules::AggregateReductionResult for ReductionKSATToSAT {} @@ -243,24 +244,8 @@ macro_rules! impl_ksat_to_sat { }; } -// Register KN for the reduction graph (covers all K values as the generic entry) -impl_ksat_to_sat!(KN); - -// K3 and K2 keep their ReduceTo impls for typed use, -// but are NOT registered as separate primitive graph edges (KN covers them). -impl ReduceTo for KSatisfiability { - type Result = ReductionKSATToSAT; - fn reduce_to(&self) -> Result { - Ok(reduce_ksat_to_sat(self)) - } -} - -impl ReduceTo for KSatisfiability { - type Result = ReductionKSATToSAT; - fn reduce_to(&self) -> Result { - Ok(reduce_ksat_to_sat(self)) - } -} +impl_ksat_to_sat!(K2); +impl_ksat_to_sat!(K3); #[cfg(feature = "example-db")] pub(crate) fn canonical_rule_example_specs() -> Vec { @@ -297,7 +282,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec::new( + let source = KSatisfiability::::new( 4, vec![ CNFClause::new(vec![1, -2, 3]), @@ -314,6 +299,26 @@ pub(crate) fn canonical_rule_example_specs() -> Vec::new( + 3, + vec![ + CNFClause::new(vec![1, -2]), + CNFClause::new(vec![2, 3]), + CNFClause::new(vec![-1, -3]), + ], + ); + crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>( + source, + SolutionPair { + source_config: serde_json::json!(vec![true, true, false]), + target_config: serde_json::json!(vec![true, true, false]), + }, + ) + }, + }, ] } diff --git a/src/solvers/pipelines.rs b/src/solvers/pipelines.rs index 4260a470d..b9615dead 100644 --- a/src/solvers/pipelines.rs +++ b/src/solvers/pipelines.rs @@ -278,7 +278,7 @@ register_ilp_pipeline! { } register_ilp_pipeline! { - ("KSatisfiability", [("k", "KN")]), + ("KSatisfiability", [("k", "K3")]), ("Satisfiability", []), ("NAESatisfiability", []), ("ILP", [("variable", "bool"), ("coefficient", "i64"), ("bounds", "general")]), diff --git a/src/unit_tests/ilp_overhead.rs b/src/unit_tests/ilp_overhead.rs index 5b33193a1..c1c17fcfe 100644 --- a/src/unit_tests/ilp_overhead.rs +++ b/src/unit_tests/ilp_overhead.rs @@ -205,27 +205,24 @@ fn nae_support_ignores_repeated_literals_and_bounds_cancellation() { 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( + let source = KSatisfiability::::new( 1, - vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -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), + ("num_nonzero_requirements", 128, 132), + ("num_available_assignments", 258, 264), + ("period_count_bits", 5, 9), + ("num_craftsmen", 61, 63), + ("num_tasks", 62, 64), ], ); - check_contract::<_, TimetableDesign>(&KSatisfiability::::new_allow_less(0, vec![])); - check_contract::<_, TimetableDesign>(&KSatisfiability::::new_allow_less( - 0, - vec![CNFClause::new(vec![])], - )); + check_contract::<_, TimetableDesign>(&KSatisfiability::::new(0, vec![])); } #[test] @@ -396,9 +393,12 @@ fn ensemble_terms_include_ordering_and_target_matches() { 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( + let source = KSatisfiability::::new( 1, - vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], ); for intermediate in [ step::(), @@ -583,20 +583,14 @@ fn sentinel_literal_pairs_count_each_clause_once() { 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])]), + &KSatisfiability::::new(1, vec![CNFClause::new(vec![1, 1, 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, - )); - } + check_contract::<_, PreemptiveScheduling>(&KSatisfiability::::new(0, vec![])); } #[test] diff --git a/src/unit_tests/models/formula/ksat.rs b/src/unit_tests/models/formula/ksat.rs index 4ec78e2a4..72cdaee92 100644 --- a/src/unit_tests/models/formula/ksat.rs +++ b/src/unit_tests/models/formula/ksat.rs @@ -1,4 +1,5 @@ use super::*; +use crate::registry::ConstructionError; use crate::solvers::BruteForce; use crate::solvers::BruteForceProblem as _; use crate::traits::Problem; @@ -70,16 +71,24 @@ fn test_3sat_brute_force() { } #[test] -fn test_ksat_allow_less() { - // This should work - clause has 2 literals which is <= 3 - let problem = KSatisfiability::::new_allow_less(2, vec![CNFClause::new(vec![1, 2])]); - assert_eq!(problem.num_clauses(), 1); +fn test_ksat_rejects_clause_widths_other_than_k() { + for literals in [vec![], vec![1], vec![1, 2], vec![1, 2, 3, 4]] { + let width = literals.len(); + let error = KSatisfiability::::try_new(4, vec![CNFClause::new(literals)]).unwrap_err(); + assert_eq!( + error, + ConstructionError::Conversion(format!("Clause 0 has {width} literals, expected 3")) + ); + } } #[test] -#[should_panic(expected = "Clause 0 has 4 literals, expected at most 3")] -fn test_ksat_allow_less_too_many() { - let _ = KSatisfiability::::new_allow_less(4, vec![CNFClause::new(vec![1, 2, 3, 4])]); +fn test_ksat_rejects_unbounded_clause_width() { + let error = KSatisfiability::::try_new(1, vec![CNFClause::new(vec![1])]).unwrap_err(); + assert_eq!( + error, + ConstructionError::Conversion("KSatisfiability requires a fixed clause width K".into()) + ); } #[test] @@ -181,43 +190,6 @@ fn test_jl_parity_evaluation() { } } -#[test] -fn test_kn_creation() { - // KN accepts clauses of any length without validation - let problem = KSatisfiability::::new( - 3, - vec![ - CNFClause::new(vec![1, 2, 3]), // 3 literals - CNFClause::new(vec![-1, -2]), // 2 literals - CNFClause::new(vec![1]), // 1 literal - ], - ); - assert_eq!(problem.num_vars(), 3); - assert_eq!(problem.num_clauses(), 3); - assert!(problem.evaluate(&vec![true, false, false]).unwrap()); // x1=T, x2=F, x3=F -} - -#[test] -fn test_kn_from_k3_clauses() { - // KN can be constructed from clauses originally built for K3 - let k3 = KSatisfiability::::new( - 3, - vec![ - CNFClause::new(vec![1, 2, -3]), - CNFClause::new(vec![-1, -2, -3]), - ], - ); - let kn = KSatisfiability::::new(k3.num_vars(), k3.clauses().to_vec()); - // Both should agree on evaluations - for config in &[ - vec![true, false, false], - vec![false, true, false], - vec![true, true, true], - ] { - assert_eq!(k3.evaluate(config).unwrap(), kn.evaluate(config).unwrap()); - } -} - #[test] fn test_parameter_getters() { let problem = KSatisfiability::::new( diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs index caa9d2744..2dcab2e53 100644 --- a/src/unit_tests/reduction_graph.rs +++ b/src/unit_tests/reduction_graph.rs @@ -810,8 +810,8 @@ fn default_variant_for_ksat_uses_declared_default() { let variant = default.unwrap(); assert_eq!( variant.get("k").map(|s| s.as_str()), - Some("KN"), - "default KSatisfiability variant should use KN" + Some("K3"), + "default KSatisfiability variant should use K3" ); } diff --git a/src/unit_tests/rules/aggregate_contracts.rs b/src/unit_tests/rules/aggregate_contracts.rs index af36839a9..c5aab992d 100644 --- a/src/unit_tests/rules/aggregate_contracts.rs +++ b/src/unit_tests/rules/aggregate_contracts.rs @@ -225,18 +225,15 @@ fn matching_decoding_threshold_handles_empty_and_unsatisfiable_instances() { } #[test] -fn sat_cover_threshold_supports_short_and_empty_clauses() { +fn sat_cover_threshold_supports_repeated_literals() { for clauses in [ vec![], - vec![vec![]], - vec![vec![1]], - vec![vec![1], vec![-1]], + vec![vec![1, 1, 1]], + vec![vec![1, 1, 1], vec![-1, -1, -1]], vec![vec![1, -1, 1]], ] { - let source = KSatisfiability::::new_allow_less( - 1, - clauses.into_iter().map(CNFClause::new).collect(), - ); + let source = + KSatisfiability::::new(1, clauses.into_iter().map(CNFClause::new).collect()); check_decision::< _, crate::models::decision::Decision>, @@ -302,11 +299,11 @@ fn sat_empty_conjunction_and_empty_clause_preserve_opposite_answers() { use crate::models::graph::KColoring; use crate::models::misc::TimetableDesign; for clauses in [vec![], vec![CNFClause::new(vec![])]] { - let source = Satisfiability::new(0, clauses.clone()); + let source = Satisfiability::new(0, clauses); check_decision::<_, KSatisfiability>(&source); check_decision::<_, KColoring>(&source); - check_decision::<_, TimetableDesign>(&KSatisfiability::::new_allow_less(0, clauses)); } + check_decision::<_, TimetableDesign>(&KSatisfiability::::new(0, vec![])); } #[test] diff --git a/src/unit_tests/rules/graph.rs b/src/unit_tests/rules/graph.rs index c2cb4a0d3..d30d52b95 100644 --- a/src/unit_tests/rules/graph.rs +++ b/src/unit_tests/rules/graph.rs @@ -1892,7 +1892,7 @@ fn test_reduction_chain_with_variant_reductions() { ) .into_iter() .find(|path| { - path.len() == 5 + path.len() == 4 && path.type_names() == [ "KSatisfiability", diff --git a/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs b/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs index 7b68f443c..9ee40d61f 100644 --- a/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs +++ b/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs @@ -86,7 +86,7 @@ fn test_acyclicpartition_extraction_rejects_invalid_targets() { } #[test] -fn test_acyclicpartition_native_empty_and_short_clauses() { +fn test_acyclicpartition_empty_and_unsatisfiable_formulas() { for n in [0, 3] { let source = KSatisfiability::::new(n, vec![]); let reduction = ReduceTo::>::reduce_to(&source).unwrap(); @@ -103,10 +103,13 @@ fn test_acyclicpartition_native_empty_and_short_clauses() { ); } } - for clauses in [vec![vec![]], vec![vec![1], vec![-1]]] { - let source = KSatisfiability::::new_allow_less( + { + let source = KSatisfiability::::new( 1, - clauses.into_iter().map(CNFClause::new).collect(), + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], ); let reduction = ReduceTo::>::reduce_to(&source).unwrap(); assert!(BruteForce::new().solve(&source).unwrap().is_none()); diff --git a/src/unit_tests/rules/ksatisfiability_bicliquecover.rs b/src/unit_tests/rules/ksatisfiability_bicliquecover.rs index 9c6b4b2c9..901eb6fee 100644 --- a/src/unit_tests/rules/ksatisfiability_bicliquecover.rs +++ b/src/unit_tests/rules/ksatisfiability_bicliquecover.rs @@ -207,7 +207,7 @@ fn test_ksatisfiability_to_bicliquecover_construct_two_vars_no_panic() { fn test_ksatisfiability_to_bicliquecover_sparse_variable_inverse() { // The only used variable has a high source index. Its normalized gadget // equals the canonical one-variable gadget; unused variables map to false. - let source = KSatisfiability::::new_allow_less(7, vec![CNFClause::new(vec![7])]); + let source = KSatisfiability::::new(7, vec![CNFClause::new(vec![7, 7, 7])]); let reduction = ReduceTo::::reduce_to(&source).unwrap(); assert_eq!(reduction.source_variables, vec![6]); assert_eq!(reduction.normalized_n, 2); @@ -237,30 +237,25 @@ fn test_ksatisfiability_to_bicliquecover_sparse_variable_inverse() { } #[test] -fn test_ksatisfiability_to_bicliquecover_empty_conjunction_and_clause() { +fn test_ksatisfiability_to_bicliquecover_empty_conjunction() { for n in [0, 3] { let yes = KSatisfiability::::new(n, vec![]); let reduction = ReduceTo::::reduce_to(&yes).unwrap(); assert_eq!(reduction.target_problem().num_vertices(), 0); assert_eq!(reduction.extract_solution(&vec![]).unwrap(), vec![false; n]); assert!(yes.evaluate(&vec![false; n]).unwrap().0); - let no = KSatisfiability::::new_allow_less(n, vec![CNFClause::new(vec![])]); - let reduction = ReduceTo::::reduce_to(&no).unwrap(); - assert!(reduction - .target_problem() - .evaluate(&vec![]) - .unwrap() - .0 - .is_none()); - assert!(reduction.extract_solution(&vec![]).is_err()); - assert!(!no.evaluate(&vec![false; n]).unwrap().0); } } #[test] -fn test_ksatisfiability_to_bicliquecover_normalization_preserves_short_clauses() { - for literals in [vec![2], vec![-2], vec![2, -5], vec![-2, 5, 5]] { - let source = KSatisfiability::::new_allow_less(6, vec![CNFClause::new(literals)]); +fn test_ksatisfiability_to_bicliquecover_normalization_preserves_repeated_literals() { + for literals in [ + vec![2, 2, 2], + vec![-2, -2, -2], + vec![2, -5, -5], + vec![-2, 5, 5], + ] { + let source = KSatisfiability::::new(6, vec![CNFClause::new(literals)]); let reduction = ReduceTo::::reduce_to(&source).unwrap(); let (n, clauses) = super::normalize(&source, &reduction.source_variables).unwrap(); let normalized = diff --git a/src/unit_tests/rules/ksatisfiability_cyclicordering.rs b/src/unit_tests/rules/ksatisfiability_cyclicordering.rs index 75c1ab6f7..078a004ae 100644 --- a/src/unit_tests/rules/ksatisfiability_cyclicordering.rs +++ b/src/unit_tests/rules/ksatisfiability_cyclicordering.rs @@ -207,22 +207,19 @@ fn test_ksatisfiability_to_cyclicordering_closed_loop() { } #[test] -fn repeated_short_and_unsorted_clauses_preserve_all_source_assignments() { +fn repeated_and_unsorted_clauses_preserve_all_source_assignments() { let formulas = [ vec![vec![5, 5, 5]], vec![vec![-5, -5, -5]], vec![vec![5, -5, 5]], vec![vec![5, 2, 5]], - vec![vec![5]], - vec![vec![-5, 2]], + vec![vec![-5, 2, 2]], vec![vec![5, 1, -3], vec![-1, 5, 2], vec![-3, 2, -5]], ]; for clauses in formulas { - let source = KSatisfiability::::try_new_allow_less( - 6, - clauses.into_iter().map(CNFClause::new).collect(), - ) - .unwrap(); + let source = + KSatisfiability::::try_new(6, clauses.into_iter().map(CNFClause::new).collect()) + .unwrap(); let reduction = ReduceTo::::reduce_to(&source).unwrap(); let normalized = normalize(&source).unwrap(); assert!(normalized @@ -248,7 +245,7 @@ fn repeated_short_and_unsorted_clauses_preserve_all_source_assignments() { } #[test] -fn empty_formula_and_empty_clause_have_opposite_fixed_targets() { +fn empty_formula_has_a_fixed_yes_target() { for num_vars in [0, 3] { let source = KSatisfiability::::new(num_vars, vec![]); let reduction = ReduceTo::::reduce_to(&source).unwrap(); @@ -257,22 +254,6 @@ fn empty_formula_and_empty_clause_have_opposite_fixed_targets() { reduction.extract_solution(&vec![0]).unwrap(), vec![false; num_vars] ); - let source = - KSatisfiability::::try_new_allow_less(num_vars, vec![CNFClause::new(vec![])]) - .unwrap(); - let reduction = ReduceTo::::reduce_to(&source).unwrap(); - assert_eq!(reduction.target_problem().num_elements(), 3); - for config in [ - vec![0, 1, 2], - vec![0, 2, 1], - vec![1, 0, 2], - vec![1, 2, 0], - vec![2, 0, 1], - vec![2, 1, 0], - ] { - assert!(!reduction.target_problem().evaluate(&config).unwrap().0); - assert!(reduction.extract_solution(&config).is_err()); - } } } diff --git a/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs index fc8d8f05d..4e42374c3 100644 --- a/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs +++ b/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs @@ -88,30 +88,19 @@ fn test_ksatisfiability_to_decisionminimumvertexcover_extract_solution() { } #[test] -fn test_ksatisfiability_to_decisionminimumvertexcover_short_clauses_closed_loop() { - let source = KSatisfiability::::new_allow_less( +fn test_ksatisfiability_to_decisionminimumvertexcover_repeated_literals_closed_loop() { + let source = KSatisfiability::::new( 2, - vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1, 2])], + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, 2, 2]), + ], ); let reduction = ReduceTo::>>::reduce_to(&source).unwrap(); assert_satisfaction_round_trip_from_satisfaction_target( &source, &reduction, - "short clauses -> Decision MVC", + "repeated literals -> Decision MVC", ); } - -#[test] -fn test_ksatisfiability_to_decisionminimumvertexcover_empty_clause() { - let source = KSatisfiability::::new_allow_less(0, vec![CNFClause::new(vec![])]); - let reduction = - ReduceTo::>>::reduce_to(&source).unwrap(); - assert_eq!(reduction.target_problem().bound(), &-1); - assert!(BruteForce::new().solve(&source).unwrap().is_none()); - assert!(BruteForce::new() - .solve(reduction.target_problem()) - .unwrap() - .is_none()); - assert!(reduction.extract_solution(&vec![true; 3]).is_err()); -} diff --git a/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs b/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs index e242c81cf..5dffd13ee 100644 --- a/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs +++ b/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs @@ -178,24 +178,8 @@ fn test_ksatisfiability_to_feasible_register_assignment_unsatisfiable_instance() } #[test] -fn native_empty_clause_is_infeasible_and_empty_conjunction_is_feasible() { +fn empty_conjunction_is_feasible() { for num_vars in [0, 3] { - let source = - KSatisfiability::::try_new_allow_less(num_vars, vec![CNFClause::new(vec![])]) - .unwrap(); - let reduction = ReduceTo::::reduce_to(&source).unwrap(); - assert_eq!(reduction.target_problem().num_vertices(), 3); - for config in [ - vec![0, 1, 2], - vec![0, 2, 1], - vec![1, 0, 2], - vec![1, 2, 0], - vec![2, 0, 1], - vec![2, 1, 0], - ] { - assert!(!reduction.target_problem().evaluate(&config).unwrap().0); - assert!(reduction.extract_solution(&config).is_err()); - } let source = KSatisfiability::::new(num_vars, vec![]); let reduction = ReduceTo::::reduce_to(&source).unwrap(); assert_eq!(reduction.target_problem().num_vertices(), 0); @@ -207,21 +191,17 @@ fn native_empty_clause_is_infeasible_and_empty_conjunction_is_feasible() { } #[test] -fn short_repeated_and_mixed_clauses_have_complete_forward_witnesses() { +fn repeated_and_mixed_clauses_have_complete_forward_witnesses() { for formula in [ - vec![vec![5]], - vec![vec![-5]], - vec![vec![5, 2]], - vec![vec![-5, 2]], + vec![vec![-5, -5, -5]], + vec![vec![-5, 2, 2]], vec![vec![5, 5, 5]], vec![vec![5, -5, 5]], vec![vec![5, 1, -3], vec![-1, 5, 2], vec![-3, 2, -5]], ] { - let source = KSatisfiability::::try_new_allow_less( - 6, - formula.into_iter().map(CNFClause::new).collect(), - ) - .unwrap(); + let source = + KSatisfiability::::try_new(6, formula.into_iter().map(CNFClause::new).collect()) + .unwrap(); let reduction = ReduceTo::::reduce_to(&source).unwrap(); let a = reduction.source_variables.len(); assert_eq!( @@ -250,33 +230,6 @@ fn short_repeated_and_mixed_clauses_have_complete_forward_witnesses() { } } -#[test] -fn short_clause_padding_matches_its_equivalent_three_literal_formula() { - let short = KSatisfiability::::try_new_allow_less( - 3, - vec![CNFClause::new(vec![3]), CNFClause::new(vec![-3])], - ) - .unwrap(); - let padded = KSatisfiability::::new( - 3, - vec![ - CNFClause::new(vec![3, 3, 3]), - CNFClause::new(vec![-3, -3, -3]), - ], - ); - let a = ReduceTo::::reduce_to(&short).unwrap(); - let b = ReduceTo::::reduce_to(&padded).unwrap(); - assert_eq!(a.target_problem().arcs(), b.target_problem().arcs()); - assert_eq!( - a.target_problem().assignment(), - b.target_problem().assignment() - ); - assert_eq!( - a.target_problem().num_vertices(), - b.target_problem().num_vertices() - ); -} - #[test] fn invalid_realizations_are_rejected() { let source = issue_example(); diff --git a/src/unit_tests/rules/ksatisfiability_kclique.rs b/src/unit_tests/rules/ksatisfiability_kclique.rs index 0e0bf789b..baa3dc457 100644 --- a/src/unit_tests/rules/ksatisfiability_kclique.rs +++ b/src/unit_tests/rules/ksatisfiability_kclique.rs @@ -48,7 +48,7 @@ fn test_ksatisfiability_to_kclique_closed_loop() { } #[test] -fn test_kclique_empty_formulas_and_short_clauses() { +fn test_kclique_empty_formulas_and_repeated_literals() { for n in [0, 3, 4] { let source = KSatisfiability::::new(n, vec![]); let reduction = ReduceTo::>::reduce_to(&source).unwrap(); @@ -65,16 +65,11 @@ fn test_kclique_empty_formulas_and_short_clauses() { ); } for clauses in [ - vec![vec![]], - vec![vec![], vec![]], - vec![vec![], vec![1]], - vec![vec![1], vec![-1]], - vec![vec![1], vec![2, -1]], + vec![vec![1, 1, 1], vec![-1, -1, -1]], + vec![vec![1, 1, 1], vec![2, -1, -1]], ] { - let source = KSatisfiability::::new_allow_less( - 2, - clauses.into_iter().map(CNFClause::new).collect(), - ); + let source = + KSatisfiability::::new(2, clauses.into_iter().map(CNFClause::new).collect()); let reduction = ReduceTo::>::reduce_to(&source).unwrap(); let sat = BruteForce::new().solve(&source).unwrap().is_some(); let solutions = BruteForce::new() @@ -94,28 +89,25 @@ fn test_kclique_empty_formulas_and_short_clauses() { #[test] fn test_kclique_all_two_clause_formulas_and_target_selections() { - // All ordered clauses of width 0..3 on one variable, including repetitions + // All ordered three-literal clauses on one variable, including repetitions // and tautologies; every ordered pair and every raw target bitvector. - let mut clauses = vec![vec![]]; - for width in 1..=3 { - for mask in 0..(1usize << width) { - clauses.push( - (0..width) - .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 }) - .collect(), - ); - } - } + let clauses: Vec> = (0..8usize) + .map(|mask| { + (0..3) + .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 }) + .collect() + }) + .collect(); for a in &clauses { for b in &clauses { - let source = KSatisfiability::::new_allow_less( + let source = KSatisfiability::::new( 1, vec![CNFClause::new(a.clone()), CNFClause::new(b.clone())], ); let reduction = ReduceTo::>::reduce_to(&source).unwrap(); let target = reduction.target_problem(); let t = a.len() + b.len(); - assert_eq!(target.num_vertices(), t.max(2) + 1); + assert_eq!(target.num_vertices(), t + 1); assert_eq!(target.k(), 3); let mut source_yes = false; for value in [false, true] { @@ -157,17 +149,20 @@ fn test_kclique_all_two_clause_formulas_and_target_selections() { #[test] fn test_kclique_rejects_malformed_or_non_clique_selections() { - let source = KSatisfiability::::new_allow_less( + let source = KSatisfiability::::new( 3, - vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])], + vec![ + CNFClause::new(vec![1, 2, 2]), + CNFClause::new(vec![-1, 3, 3]), + ], ); let reduction = ReduceTo::>::reduce_to(&source).unwrap(); for bad in [ vec![], - vec![true; 6], - vec![false; 5], - vec![true, true, false, false, true], - vec![true, false, true, false, true], + vec![true; 8], + vec![false; 7], + vec![true, true, false, false, false, false, true], + vec![true, false, false, true, false, false, true], ] { assert!(reduction.extract_solution(&bad).is_err()); } @@ -175,22 +170,17 @@ fn test_kclique_rejects_malformed_or_non_clique_selections() { #[test] fn test_kclique_count_boundaries() { - assert_eq!(clique_sizes(0, []).unwrap(), (1, 1)); - assert_eq!(clique_sizes(3, [0, 0, 1]).unwrap(), (4, 4)); - assert_eq!(clique_sizes(2, [3, 3]).unwrap(), (7, 3)); - for (m, lengths) in [ - (2, vec![usize::MAX, 1]), - (1, vec![usize::MAX]), - (usize::MAX, vec![]), - ] { + assert_eq!(clique_sizes(0).unwrap(), (1, 1)); + assert_eq!(clique_sizes(2).unwrap(), (7, 3)); + let largest = (usize::MAX - 1) / 3; + assert_eq!( + clique_sizes(largest).unwrap(), + (3 * largest + 1, largest + 1) + ); + for m in [largest + 1, usize::MAX] { assert!(matches!( - clique_sizes(m, lengths), + clique_sizes(m), Err(crate::rules::ReductionError::IntegerOverflow { .. }) )); } - assert_eq!( - clique_sizes(usize::MAX - 1, []).unwrap(), - (usize::MAX, usize::MAX) - ); - assert_eq!(clique_sizes(1, [usize::MAX - 1]).unwrap(), (usize::MAX, 2)); } diff --git a/src/unit_tests/rules/ksatisfiability_kernel.rs b/src/unit_tests/rules/ksatisfiability_kernel.rs index 200045a36..9805e42ac 100644 --- a/src/unit_tests/rules/ksatisfiability_kernel.rs +++ b/src/unit_tests/rules/ksatisfiability_kernel.rs @@ -79,18 +79,15 @@ fn test_ksatisfiability_to_kernel_extract_solution_reads_variable_gadgets() { } #[test] -fn test_ksatisfiability_to_kernel_native_clause_domain() { +fn test_ksatisfiability_to_kernel_one_variable_clause_domain() { use crate::traits::Problem; - let mut clauses = vec![vec![]]; - for len in 1..=3 { - for mask in 0..(1 << len) { - clauses.push( - (0..len) - .map(|j| if mask & (1 << j) == 0 { 1 } else { -1 }) - .collect(), - ); - } - } + let clauses: Vec> = (0..8) + .map(|mask| { + (0..3) + .map(|j| if mask & (1 << j) == 0 { 1 } else { -1 }) + .collect() + }) + .collect(); let mut formulas = vec![vec![]]; for first in &clauses { formulas.push(vec![first.clone()]); @@ -99,20 +96,16 @@ fn test_ksatisfiability_to_kernel_native_clause_domain() { } } for formula in formulas { - let source = KSatisfiability::::try_new_allow_less( + let source = KSatisfiability::::try_new( 1, formula.iter().cloned().map(CNFClause::new).collect(), ) .unwrap(); let reduction = ReduceTo::::reduce_to(&source).unwrap(); let target = reduction.target_problem(); - let active = usize::from(formula.iter().any(|clause| !clause.is_empty())); - let occurrences: usize = formula.iter().map(Vec::len).sum(); + let active = usize::from(!formula.is_empty()); assert_eq!(target.num_vertices(), 2 * active + 3 * formula.len()); - assert_eq!( - target.num_arcs(), - 2 * active + 3 * formula.len() + occurrences - ); + assert_eq!(target.num_arcs(), 2 * active + 6 * formula.len()); let mut witnessed = [false; 2]; for mask in 0..(1usize << target.num_vertices()) { let config = (0..target.num_vertices()) @@ -139,10 +132,14 @@ fn test_ksatisfiability_to_kernel_native_clause_domain() { #[test] fn test_ksatisfiability_to_kernel_sparse_inverse() { use crate::traits::Problem; - for literals in [vec![5], vec![-5], vec![5, -2], vec![5, -5, 2]] { + for literals in [ + vec![5, 5, 5], + vec![-5, -5, -5], + vec![5, -2, -2], + vec![5, -5, 2], + ] { let source = - KSatisfiability::::try_new_allow_less(6, vec![CNFClause::new(literals.clone())]) - .unwrap(); + KSatisfiability::::try_new(6, vec![CNFClause::new(literals.clone())]).unwrap(); let reduction = ReduceTo::::reduce_to(&source).unwrap(); let target = reduction.target_problem(); let mut found = false; diff --git a/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs b/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs index eaa8484bd..b70a1fc25 100644 --- a/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs +++ b/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs @@ -129,19 +129,16 @@ fn test_ksatisfiability_to_monochromatic_triangle_unsatisfiable_all_signs() { } #[test] -fn test_ksatisfiability_to_monochromatic_triangle_short_and_repeated_literals() { +fn test_ksatisfiability_to_monochromatic_triangle_repeated_literals() { for clauses in [ vec![], - vec![vec![]], - vec![vec![1]], - vec![vec![1, -2]], + vec![vec![1, 1, 1]], + vec![vec![1, -2, -2]], vec![vec![1, 1, 1], vec![-1, -1, -1]], vec![vec![1, -1, 2]], ] { - let source = KSatisfiability::::new_allow_less( - 3, - clauses.into_iter().map(CNFClause::new).collect(), - ); + let source = + KSatisfiability::::new(3, clauses.into_iter().map(CNFClause::new).collect()); let feasible = (0..8).any(|bits| { source .evaluate(&(0..3).map(|i| bits & (1 << i) != 0).collect()) diff --git a/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs index 5792a4456..b9d92bce7 100644 --- a/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs +++ b/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs @@ -110,18 +110,16 @@ fn test_ksatisfiability_to_oneinthreesatisfiability_extract_solution() { } #[test] -fn test_oneinthree_native_empty_short_and_sparse_clauses() { +fn test_oneinthree_empty_repeated_and_sparse_clauses() { for (num_vars, formula) in [ (0, vec![]), (3, vec![]), - (0, vec![vec![]]), - (3, vec![vec![]]), - (5, vec![vec![5]]), - (5, vec![vec![-5]]), - (5, vec![vec![5, -2]]), + (5, vec![vec![5, 5, 5]]), + (5, vec![vec![-5, -5, -5]]), + (5, vec![vec![5, -2, -2]]), (5, vec![vec![5, -5, 2]]), ] { - let source = KSatisfiability::::try_new_allow_less( + let source = KSatisfiability::::try_new( num_vars, formula.iter().cloned().map(CNFClause::new).collect(), ) diff --git a/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs b/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs index 6fb987b1a..25c7c3e93 100644 --- a/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs +++ b/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs @@ -142,20 +142,15 @@ fn test_ksatisfiability_to_preemptivescheduling_unsatisfiable_threshold_gap() { } #[test] -fn test_threshold_value_mapping_and_short_clauses() { +fn test_threshold_value_mapping_and_repeated_literals() { use crate::rules::AggregateReductionResult; use crate::types::Or; for source in [ KSatisfiability::::new(0, vec![]), KSatisfiability::::new(2, vec![]), - KSatisfiability::::new_allow_less(0, vec![CNFClause::new(vec![])]), - KSatisfiability::::new_allow_less(1, vec![CNFClause::new(vec![1])]), - KSatisfiability::::new_allow_less(2, vec![CNFClause::new(vec![1, -2])]), - KSatisfiability::::new_allow_less( - 1, - vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], - ), + KSatisfiability::::new(1, vec![CNFClause::new(vec![1, 1, 1])]), + KSatisfiability::::new(2, vec![CNFClause::new(vec![1, -2, -2])]), yes_single_variable_instance(), no_single_variable_instance(), ] { @@ -238,14 +233,22 @@ fn test_registered_aggregate_mapping() { && edge.target_name == "PreemptiveScheduling" }) .unwrap(); - for (clauses, expected) in [(vec![], true), (vec![CNFClause::new(vec![])], false)] { - let source = KSatisfiability::::new_allow_less(0, clauses); - let result = (edge.reduce_aggregate_fn.unwrap())(&source).unwrap(); - assert_eq!( - result - .extract_value_from_solution_dyn(&vec![vec![true]]) - .unwrap(), - serde_json::json!(expected), - ); - } + let yes = KSatisfiability::::new(0, vec![]); + let result = (edge.reduce_aggregate_fn.unwrap())(&yes).unwrap(); + assert_eq!( + result + .extract_value_from_solution_dyn(&vec![vec![true]]) + .unwrap(), + serde_json::json!(true), + ); + // An all-idle schedule leaves every task unfinished, so it is never feasible. + let no = no_single_variable_instance(); + let target = ReduceTo::::reduce_to(&no).unwrap(); + let target = ReductionResult::target_problem(&target); + let idle = vec![vec![false; target.d_max()]; target.num_tasks()]; + let result = (edge.reduce_aggregate_fn.unwrap())(&no).unwrap(); + assert_eq!( + result.extract_value_from_solution_dyn(&idle).unwrap(), + serde_json::json!(false), + ); } diff --git a/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs b/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs index 098a88b18..94b893ba2 100644 --- a/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs +++ b/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs @@ -6,8 +6,7 @@ use crate::types::Or; use num_traits::ToPrimitive; fn source(n: usize, clauses: Vec>) -> KSatisfiability { - KSatisfiability::try_new_allow_less(n, clauses.into_iter().map(CNFClause::new).collect()) - .unwrap() + KSatisfiability::new(n, clauses.into_iter().map(CNFClause::new).collect()) } #[test] @@ -35,15 +34,13 @@ fn test_ksatisfiability_to_quadraticcongruences_closed_loop() { fn test_native_clauses_and_arbitrary_crt_signs() { for source in [ source(0, vec![]), - source(0, vec![vec![]]), source(3, vec![vec![1, 1, 1]]), source(3, vec![vec![-1, -1, -1]]), - source(3, vec![vec![1, 2]]), + source(3, vec![vec![1, 2, 2]]), source(3, vec![vec![1, 2, 3]]), source(3, vec![vec![-3, -1, 2]]), - source(2, vec![vec![1], vec![-1]]), - source(2, vec![vec![1, 2], vec![-1, -2]]), - source(2, vec![vec![], vec![1, 2]]), + source(2, vec![vec![1, 1, 1], vec![-1, -1, -1]]), + source(2, vec![vec![1, 2, 2], vec![-1, -2, -2]]), source(17, vec![vec![17, 17, 17]]), ] { let construction = build_construction(&source).unwrap(); @@ -146,7 +143,7 @@ fn test_unsatisfiable_formula_has_no_quadratic_sign_witness() { #[test] fn test_normalization_preserves_free_variables_and_formula() { - let canonical = source(5, vec![vec![-5, 2]]); + let canonical = source(5, vec![vec![-5, 2, 2]]); let redundant = source(5, vec![vec![2, -5, 2], vec![-5, 2, -5], vec![1, -1, 4]]); let first = ReduceTo::::reduce_to(&canonical).unwrap(); let second = ReduceTo::::reduce_to(&redundant).unwrap(); @@ -200,9 +197,8 @@ fn test_prime_generation_and_parameter_bounds() { assert_eq!(admissible_primes(4).unwrap(), vec![13, 17, 19, 23]); for source in [ source(0, vec![]), - source(0, vec![vec![]]), source(3, vec![vec![1, 2, 3]]), - source(1, vec![vec![1], vec![-1]]), + source(1, vec![vec![1, 1, 1], vec![-1, -1, -1]]), ] { let reduction = ReduceTo::::reduce_to(&source).unwrap(); let n = 2 * source.num_clauses() + source.num_vars() + 1; diff --git a/src/unit_tests/rules/ksatisfiability_qubo.rs b/src/unit_tests/rules/ksatisfiability_qubo.rs index 2d9aae200..4a03d7869 100644 --- a/src/unit_tests/rules/ksatisfiability_qubo.rs +++ b/src/unit_tests/rules/ksatisfiability_qubo.rs @@ -234,24 +234,21 @@ fn test_k3satisfiability_to_qubo_all_negated() { } #[test] -fn test_sat_qubo_all_short_clauses_and_raw_targets() { +fn test_sat_qubo_all_one_variable_clause_pairs_and_raw_targets() { use crate::rules::AggregateReductionResult; use crate::types::{Min, Or}; macro_rules! verify { ($k:ty, $width:expr) => {{ - let mut clauses = vec![vec![]]; - for width in 1..=$width { - for mask in 0..(1 << width) { - clauses.push( - (0..width) - .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 }) - .collect(), - ); - } - } + let clauses: Vec> = (0..1 << $width) + .map(|mask| { + (0..$width) + .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 }) + .collect() + }) + .collect(); for a in &clauses { for b in &clauses { - let source = KSatisfiability::<$k>::new_allow_less( + let source = KSatisfiability::<$k>::new( 1, vec![CNFClause::new(a.clone()), CNFClause::new(b.clone())], ); @@ -270,8 +267,6 @@ fn test_sat_qubo_all_short_clauses_and_raw_targets() { .map(|&l| i64::from(witness[0] != (l > 0))) .collect(); penalty += match y.as_slice() { - [] => 1, - &[u] => u, &[u, v] => u * v, &[u, v, w] => { let z = i64::from(witness[1 + j]); @@ -363,9 +358,12 @@ fn test_sat_qubo_checked_numeric_boundaries() { #[test] fn test_sat_qubo_registered_aggregate_threshold() { macro_rules! check { - ($k:ty) => { - for (clauses, expected) in [(vec![vec![1]], true), (vec![vec![1], vec![-1]], false)] { - let source = KSatisfiability::<$k>::new_allow_less( + ($k:ty, $width:expr) => { + for (clauses, expected) in [ + (vec![vec![1; $width]], true), + (vec![vec![1; $width], vec![-1; $width]], false), + ] { + let source = KSatisfiability::<$k>::new( 1, clauses.into_iter().map(CNFClause::new).collect(), ); @@ -390,6 +388,6 @@ fn test_sat_qubo_registered_aggregate_threshold() { } }; } - check!(K2); - check!(K3); + check!(K2, 2); + check!(K3, 3); } diff --git a/src/unit_tests/rules/ksatisfiability_registersufficiency.rs b/src/unit_tests/rules/ksatisfiability_registersufficiency.rs index 301cf7af3..036f7ac98 100644 --- a/src/unit_tests/rules/ksatisfiability_registersufficiency.rs +++ b/src/unit_tests/rules/ksatisfiability_registersufficiency.rs @@ -148,48 +148,39 @@ fn test_ksatisfiability_to_register_sufficiency_canonical_example_spec() { } #[test] -fn test_ksatisfiability_to_registersufficiency_closed_loop_boundaries() { +fn test_ksatisfiability_to_registersufficiency_empty_formula() { use crate::solvers::BruteForce; for declared in [0, 5] { - let yes = KSatisfiability::::new(declared, vec![]); - let no = KSatisfiability::::try_new_allow_less(declared, vec![CNFClause::new(vec![])]) + let source = KSatisfiability::::new(declared, vec![]); + let reduction = ReduceTo::::reduce_to(&source).unwrap(); + let solution = BruteForce::new() + .solve(reduction.target_problem()) + .unwrap() .unwrap(); - for (source, feasible) in [(yes, true), (no, false)] { - let reduction = ReduceTo::::reduce_to(&source).unwrap(); - let solution = BruteForce::new().solve(reduction.target_problem()).unwrap(); - assert_eq!(solution.is_some(), feasible); - if let Some(solution) = solution { - let extracted = reduction.extract_solution(&solution).unwrap(); - assert_eq!(extracted, vec![false; declared]); - assert_eq!(source.evaluate(&extracted).unwrap(), Or(true)); - } else { - assert!(reduction.extract_solution(&vec![0]).is_err()); - } - } + let extracted = reduction.extract_solution(&solution).unwrap(); + assert_eq!(extracted, vec![false; declared]); + assert_eq!(source.evaluate(&extracted).unwrap(), Or(true)); } } #[test] -fn test_short_repeated_and_tautological_clauses() { +fn test_repeated_and_tautological_clauses() { for num_vars in 1..=3 { let literals: Vec = (1..=num_vars) .flat_map(|i| [i as i64, -(i as i64)]) .collect(); - for width in 1..=3 { - for code in 0..literals.len().pow(width) { + { + for code in 0..literals.len().pow(3) { let mut remaining = code; - let clause: Vec<_> = (0..width) + let clause: Vec<_> = (0..3) .map(|_| { let lit = literals[remaining % literals.len()]; remaining /= literals.len(); lit }) .collect(); - let source = KSatisfiability::::try_new_allow_less( - num_vars, - vec![CNFClause::new(clause)], - ) - .unwrap(); + let source = + KSatisfiability::::try_new(num_vars, vec![CNFClause::new(clause)]).unwrap(); let reduction = ReduceTo::::reduce_to(&source).unwrap(); let layout = reduction.layout.as_ref().unwrap(); for mask in 0..(1usize << num_vars) { @@ -227,8 +218,7 @@ fn test_short_repeated_and_tautological_clauses() { #[test] fn test_sparse_original_variables_and_padding_bound() { - let source = - KSatisfiability::::try_new_allow_less(17, vec![CNFClause::new(vec![-17, 2])]).unwrap(); + let source = KSatisfiability::::new(17, vec![CNFClause::new(vec![-17, 2, 2])]); let reduction = ReduceTo::::reduce_to(&source).unwrap(); assert_eq!(reduction.source_variables, vec![1, 16]); let layout = reduction.layout.as_ref().unwrap(); diff --git a/src/unit_tests/rules/ksatisfiability_timetabledesign.rs b/src/unit_tests/rules/ksatisfiability_timetabledesign.rs index ea24af2bd..6daf8db98 100644 --- a/src/unit_tests/rules/ksatisfiability_timetabledesign.rs +++ b/src/unit_tests/rules/ksatisfiability_timetabledesign.rs @@ -18,9 +18,12 @@ fn satisfiable_instance() -> KSatisfiability { } fn unsatisfiable_instance() -> KSatisfiability { - KSatisfiability::::new_allow_less( + KSatisfiability::::new( 1, - vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], ) } diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs index 1cb5eeca5..a09adf374 100644 --- a/src/unit_tests/symbolic_parameter_contracts.rs +++ b/src/unit_tests/symbolic_parameter_contracts.rs @@ -684,12 +684,8 @@ fn sat_flow_and_scheduling_bounds_cover_fixed_outputs() { misc::PreemptiveScheduling, }; use crate::variant::K3; - for clauses in [ - vec![], - vec![CNFClause::new(vec![])], - vec![CNFClause::new(vec![1, 1, -2])], - ] { - let source = KSatisfiability::::new_allow_less(2, clauses); + for clauses in [vec![], vec![CNFClause::new(vec![1, 1, -2])]] { + let source = KSatisfiability::::new(2, clauses); check_reduced_parameters::<_, DirectedTwoCommodityIntegralFlow>( source.clone(), &["max_capacity"], @@ -935,33 +931,32 @@ fn vertex_cover_lcs_transition_bounds_cover_empty_strings() { } #[test] -fn three_sat_contracts_cover_short_clauses() { +fn three_sat_counts_are_exact_on_repeated_literals() { use crate::models::decision::Decision; use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability}; use crate::models::graph::{KClique, MinimumVertexCover}; use crate::models::misc::SubsetSum; use crate::types::One; use crate::variant::K3; - // `new_allow_less` admits clauses with fewer than three literals, so - // counts that grow with each literal are only upper bounds. - let upper = ParameterRelation::UpperBound; let exact = ParameterRelation::Exact; for clauses in [ - vec![CNFClause::new(vec![1])], - vec![CNFClause::new(vec![])], - vec![CNFClause::new(vec![1, -2]), CNFClause::new(vec![2])], + vec![], + vec![CNFClause::new(vec![1, 1, 1])], + vec![ + CNFClause::new(vec![1, -2, -2]), + CNFClause::new(vec![2, 2, 2]), + ], ] { - let source = KSatisfiability::::new_allow_less(2, clauses); + let source = KSatisfiability::::new(2, clauses); check_reduced_parameters::<_, KClique>( source.clone(), - &["num_vertices"], - upper, + &["k", "num_vertices"], + exact, ); - check_reduced_parameters::<_, KClique>(source.clone(), &["k"], exact); check_reduced_parameters::<_, Decision>>( source.clone(), - &["num_edges"], - upper, + &["num_vertices", "num_edges"], + exact, ); check_reduced_parameters::<_, OneInThreeSatisfiability>( source.clone(), From 86d6808e77a1a328ea327d917a2f413b6fbf7434 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 28 Oct 2026 10:49:19 -0700 Subject: [PATCH 08/12] Declare MonochromaticTriangle counts exact and drop stale short-clause text SAT -> NAE turns every three-literal clause into a four-literal one, so the MonochromaticTriangle vertex, edge and triangle counts are equalities and its two-literal branch was dead. Also remove leftover short- and empty-clause wording and dead padding in OneInThree, QuadraticCongruences and Kernel. Co-Authored-By: Claude Opus 5.5 --- docs/paper/reductions.typ | 20 ++++++------- .../ksatisfiability_monochromatictriangle.rs | 30 ++++++++----------- ...satisfiability_oneinthreesatisfiability.rs | 9 ++---- .../ksatisfiability_quadraticcongruences.rs | 4 +-- .../symbolic_parameter_contracts.rs | 7 ++++- 5 files changed, 34 insertions(+), 36 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index c7a39e66d..7dc51eb83 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -12505,7 +12505,7 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with )[ The bounded quadratic-congruence construction of Manders and Adleman @mandersAdleman1976 converts an odd signed-knapsack target into a square congruence using prime powers and the Chinese Remainder Theorem. We give base-eight positions only to the actual normalized clauses. The same slack equation handles every native clause width from zero through three. ][ - _Construction._ Delete tautologies and duplicate literals and clauses, retaining empty clauses. Compact the $l$ occurring variables, recording their original positions. Let $C_1, dots, C_m$ be the remaining clauses, $r_j = |C_j|$, $N = 2m+l+1$, and $D=8^(m+1)$. Let $f_i^+$ and $f_i^-$ be the sums of $8^j$ over clauses containing variable $i$ positively and negatively. Define $N$ integer coefficients and an odd target: + _Construction._ Delete tautologies and duplicate literals and clauses. Compact the $l$ occurring variables, recording their original positions. Let $C_1, dots, C_m$ be the remaining clauses, $r_j = |C_j|$, $N = 2m+l+1$, and $D=8^(m+1)$. Let $f_i^+$ and $f_i^-$ be the sums of $8^j$ over clauses containing variable $i$ positively and negatively. Define $N$ integer coefficients and an odd target: $ c_0=1, quad c_(2j-1)=-8^j/2, quad c_(2j)=-8^j, quad c_(2m+i)=(f_i^+-f_i^-)/2, $ $ tau=1+sum_(j=1)^m (r_j-5)8^j/2. $ Take the first $N$ primes starting at $13$, indexed from zero, and put $q_i=p_i^N$ and $K=product_i q_i$. Let $theta_i$ be the least positive integer satisfying $theta_i equiv c_i mod D$, $theta_i equiv 0 mod (K/q_i)$, and $p_i$ not dividing $theta_i$. CRT gives a residue modulo $D K/q_i$; choosing the first positive representative and, if necessary, adding that modulus once gives $theta_i$. Set $H=sum_i theta_i$ and @@ -12514,7 +12514,7 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with _Clause encoding._ For signs $alpha_i in {-1,+1}$, put $t_i=(1-alpha_(2m+i))/2$ and $y_j=(3-alpha_(2j-1)-2alpha_(2j))/2 in {0,1,2,3}$. Let $T_j$ count true literals in $C_j$ and $R_j=y_j-T_j+1$. Direct expansion gives $ sum_i c_i alpha_i-tau=alpha_0-1+sum_(j=1)^m R_j 8^j. $ - Here $-2<=R_j<=4$ and $alpha_0-1 in {-2,0}$. The right side has absolute value less than $D$. Taking successive residues modulo eight shows that it vanishes exactly when $alpha_0=1$ and all $R_j=0$. Thus the linear congruence modulo $D$ encodes precisely the satisfying assignments. An empty clause has $T_j=0$ and cannot have $R_j=0$; it requires no exceptional construction. + Here $-2<=R_j<=4$ and $alpha_0-1 in {-2,0}$. The right side has absolute value less than $D$. Taking successive residues modulo eight shows that it vanishes exactly when $alpha_0=1$ and all $R_j=0$. Thus the linear congruence modulo $D$ encodes precisely the satisfying assignments. _Magnitude and square-root lemmas._ Each $theta_i<=2D K/q_i$. For $m>=1$, $N>=2m+1>=3$ and $13^N>4N D$, giving $2H> for KSatisfiability { let sat = ReduceTo::::reduce_to(self)?; let nae_reduction = ReduceTo::::reduce_to(sat.target_problem())?; let nae = nae_reduction.target_problem(); - let auxiliary_count = nae.clauses().iter().filter(|c| c.len() == 4).count(); + // SAT -> NAE appends the sentinel to every three-literal clause. + let auxiliary_count = nae.num_clauses(); let overflow = || { crate::rules::ReductionError::integer_overflow::>( "computing signal-sender graph size", @@ -124,21 +125,16 @@ impl ReduceTo> for KSatisfiability { triples.push([literal, literal, -literal]); } for clause in nae.clauses() { - let literals = &clause.literals; - if literals.len() == 4 { - let z = variables.allocate().map_err( - crate::rules::ReductionError::construction::< - Self, - MonochromaticTriangle, - >, - )?; - triples.push([literals[0], literals[1], z]); - triples.push([-z, literals[2], literals[3]]); - } else { - // NAE(a,b) = NAE(a,b,b). Formal SAT -> NAE produces only - // lengths 2, 3 and 4, including NAE(s,s) for an empty clause. - triples.push([literals[0], literals[1], literals[literals.len() - 1]]); - } + let [a, b, c, d] = <[i64; 4]>::try_from(clause.literals.as_slice()) + .expect("SAT -> NAE maps each three-literal clause to four literals"); + let z = variables.allocate().map_err( + crate::rules::ReductionError::construction::< + Self, + MonochromaticTriangle, + >, + )?; + triples.push([a, b, z]); + triples.push([-z, c, d]); } let mut edges = Vec::with_capacity(num_edges); diff --git a/src/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/rules/ksatisfiability_oneinthreesatisfiability.rs index d8e7d3165..39e6922b1 100644 --- a/src/rules/ksatisfiability_oneinthreesatisfiability.rs +++ b/src/rules/ksatisfiability_oneinthreesatisfiability.rs @@ -1,9 +1,8 @@ //! Reduction from KSatisfiability (3-SAT) to One-In-Three Satisfiability. //! //! Schaefer's Lemma 3.5 (STOC 1978) expresses a three-input disjunction -//! using five one-in-three constraints. Missing native clause positions -//! use the forced false variable; appearing source variables are compacted -//! and restored through an inverse map during extraction. +//! using five one-in-three constraints. Appearing source variables are +//! compacted and restored through an inverse map during extraction. use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability}; use crate::reduction; @@ -106,9 +105,7 @@ impl ReduceTo for KSatisfiability { clauses.push(CNFClause::new(vec![z_false, z_false, z_true])); for clause in self.clauses() { - // Adding false disjuncts preserves every native clause, including - // the empty disjunction, while using the same three-input gadget. - let mut literals = [z_false; 3]; + let mut literals = [0; 3]; for (position, &literal) in clause.literals.iter().enumerate() { let original = usize::try_from(literal.unsigned_abs()) .expect("native SAT indices fit usize") diff --git a/src/rules/ksatisfiability_quadraticcongruences.rs b/src/rules/ksatisfiability_quadraticcongruences.rs index 74680d9b8..3ccc6266d 100644 --- a/src/rules/ksatisfiability_quadraticcongruences.rs +++ b/src/rules/ksatisfiability_quadraticcongruences.rs @@ -2,8 +2,8 @@ //! //! Manders and Adleman (ERL-M615, 1976), Section 2: an odd signed-knapsack //! target and prime-power CRT encode the clauses. Only the actual normalized -//! clauses need base-eight positions; widths zero through three use the same -//! slack equation. Squaring uses twice the linear modulus, and extraction +//! clauses need base-eight positions; deduplicated widths one through three +//! use the same slack equation. Squaring uses twice the linear modulus, and extraction //! orients every sign by the distinguished odd coordinate. use std::collections::{BTreeMap, BTreeSet}; diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs index a09adf374..c881b99c7 100644 --- a/src/unit_tests/symbolic_parameter_contracts.rs +++ b/src/unit_tests/symbolic_parameter_contracts.rs @@ -934,7 +934,7 @@ fn vertex_cover_lcs_transition_bounds_cover_empty_strings() { fn three_sat_counts_are_exact_on_repeated_literals() { use crate::models::decision::Decision; use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability}; - use crate::models::graph::{KClique, MinimumVertexCover}; + use crate::models::graph::{KClique, MinimumVertexCover, MonochromaticTriangle}; use crate::models::misc::SubsetSum; use crate::types::One; use crate::variant::K3; @@ -963,6 +963,11 @@ fn three_sat_counts_are_exact_on_repeated_literals() { &["num_clauses"], exact, ); + check_reduced_parameters::<_, MonochromaticTriangle>( + source.clone(), + &["num_vertices", "num_edges", "num_triangles"], + exact, + ); check_reduced_parameters::<_, SubsetSum>(source, &["num_elements"], exact); } } From eafd02adfbe0b3b8459581f3907530d701290092 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 28 Oct 2026 10:56:36 -0700 Subject: [PATCH 09/12] Bound KSatisfiability by FixedK and tidy the K-SAT reductions - Add a FixedK sub-trait implemented by K1..K5, and bound KSatisfiability and the SAT/K-SAT results by it, so KSatisfiability no longer type-checks instead of failing at construction. - Register each K-SAT aggregate mapping inside the macro that registers its witness edge, and take the SAT -> K-SAT clause width from the type. - Allocate CyclicOrdering's fresh padding variables with allocate_many. - Drop leftover braces in two tests and a stale QuadraticCongruences note. Co-Authored-By: Claude Opus 5.5 --- src/models/formula/ksat.rs | 16 ++-- src/rules/ksatisfiability_cyclicordering.rs | 23 ++---- .../ksatisfiability_quadraticcongruences.rs | 2 +- src/rules/sat_ksat.rs | 31 ++++---- src/unit_tests/models/formula/ksat.rs | 11 +-- .../rules/ksatisfiability_acyclicpartition.rs | 30 ++++---- .../ksatisfiability_registersufficiency.rs | 76 +++++++++---------- src/variant.rs | 26 +++++-- 8 files changed, 103 insertions(+), 112 deletions(-) diff --git a/src/models/formula/ksat.rs b/src/models/formula/ksat.rs index 6d2e9bb7c..f509f578b 100644 --- a/src/models/formula/ksat.rs +++ b/src/models/formula/ksat.rs @@ -7,7 +7,7 @@ use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension}; use crate::traits::Problem; -use crate::variant::{KValue, K2, K3}; +use crate::variant::{FixedK, K2, K3}; use serde::{de::Error as _, Deserialize, Deserializer, Serialize}; use super::{sat::validate_cnf_literals, CNFClause}; @@ -72,7 +72,7 @@ inventory::submit! { /// This is the decision version of the problem. /// /// # Type Parameters -/// * `K` - A type implementing `KValue` that specifies the number of literals per clause +/// * `K` - A `FixedK` type that specifies the number of literals per clause /// /// # Example /// @@ -95,7 +95,7 @@ inventory::submit! { /// assert!(!solutions.is_empty()); /// ``` #[derive(Debug, Clone, Serialize)] -pub struct KSatisfiability { +pub struct KSatisfiability { /// Number of variables. num_vars: usize, /// Clauses in CNF, each with exactly K literals. @@ -110,7 +110,7 @@ struct KSatisfiabilityDef { clauses: Vec, } -impl<'de, K: KValue> Deserialize<'de> for KSatisfiability { +impl<'de, K: FixedK> Deserialize<'de> for KSatisfiability { fn deserialize(deserializer: D) -> Result where D: Deserializer<'de>, @@ -120,7 +120,7 @@ impl<'de, K: KValue> Deserialize<'de> for KSatisfiability { } } -impl KSatisfiability { +impl KSatisfiability { /// Create a new K-SAT problem. /// /// # Panics @@ -136,7 +136,7 @@ impl KSatisfiability { clauses: Vec, ) -> Result { validate_cnf_literals(num_vars, &clauses)?; - let k = K::K.ok_or("KSatisfiability requires a fixed clause width K")?; + let k = K::WIDTH; for (i, clause) in clauses.iter().enumerate() { if clause.len() != k { return Err( @@ -199,7 +199,7 @@ impl KSatisfiability { } } -impl Problem for KSatisfiability { +impl Problem for KSatisfiability { const NAME: &'static str = "KSatisfiability"; type Solution = Vec; type Value = crate::types::Or; @@ -227,7 +227,7 @@ impl Problem for KSatisfiability { } } -impl crate::solvers::BruteForceProblem for KSatisfiability { +impl crate::solvers::BruteForceProblem for KSatisfiability { fn dimensions(&self) -> Vec { vec![2; self.num_vars] } diff --git a/src/rules/ksatisfiability_cyclicordering.rs b/src/rules/ksatisfiability_cyclicordering.rs index 5ee098cf3..0c2115133 100644 --- a/src/rules/ksatisfiability_cyclicordering.rs +++ b/src/rules/ksatisfiability_cyclicordering.rs @@ -136,21 +136,14 @@ fn normalize( } }) .collect(); - match *literals.as_slice() { - [a, b, c] => normalized.push([a, b, c]), - [a, b] => { - let u = variables.allocate().map_err( - as ReduceTo>::target_construction, - )?; - normalized.extend([[a, b, u], [a, b, -u]]); - } - [a] => { - let u = variables.allocate().map_err( - as ReduceTo>::target_construction, - )?; - let v = variables.allocate().map_err( - as ReduceTo>::target_construction, - )?; + // Deduplication leaves one to three literals; fill the rest with fresh variables. + let fresh = variables + .allocate_many(3 - literals.len()) + .map_err( as ReduceTo>::target_construction)?; + match (literals.as_slice(), fresh.as_slice()) { + (&[a, b, c], []) => normalized.push([a, b, c]), + (&[a, b], &[u]) => normalized.extend([[a, b, u], [a, b, -u]]), + (&[a], &[u, v]) => { normalized.extend([[a, u, v], [a, u, -v], [a, -u, v], [a, -u, -v]]); } _ => unreachable!("deduplicated three-literal clauses keep one to three literals"), diff --git a/src/rules/ksatisfiability_quadraticcongruences.rs b/src/rules/ksatisfiability_quadraticcongruences.rs index 3ccc6266d..585b7fdd4 100644 --- a/src/rules/ksatisfiability_quadraticcongruences.rs +++ b/src/rules/ksatisfiability_quadraticcongruences.rs @@ -195,7 +195,7 @@ fn build_construction( coefficients[2 * j + 1] = -&half_weight; coefficients[2 * j + 2] = -BigInt::from(weight.clone()); let width = - i64::try_from(clause.len()).expect("native K3 clauses have at most three literals"); + i64::try_from(clause.len()).expect("deduplicated clauses have one to three literals"); tau += (width - 5) * &half_weight; for &literal in clause { let variable = diff --git a/src/rules/sat_ksat.rs b/src/rules/sat_ksat.rs index 599d6c9b3..9a8ccbf39 100644 --- a/src/rules/sat_ksat.rs +++ b/src/rules/sat_ksat.rs @@ -10,21 +10,21 @@ use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability}; use crate::reduction; use crate::rules::sat_helpers::SatVariableAllocator; use crate::rules::traits::{ReduceTo, ReductionResult}; -use crate::variant::{KValue, K2, K3}; +use crate::variant::{FixedK, K2, K3}; /// Result of reducing general SAT to K-SAT. /// /// This reduction transforms a SAT formula into an equisatisfiable K-SAT formula /// by introducing ancilla (auxiliary) variables. #[derive(Debug, Clone)] -pub struct ReductionSATToKSAT { +pub struct ReductionSATToKSAT { /// Number of original variables in the source problem. source_num_vars: usize, /// The target K-SAT problem. target: KSatisfiability, } -impl ReductionResult for ReductionSATToKSAT { +impl ReductionResult for ReductionSATToKSAT { type Source = Satisfiability; type Target = KSatisfiability; @@ -50,10 +50,8 @@ impl ReductionResult for ReductionSATToKSAT { } } -crate::register_aggregate_reduction!(ReductionSATToKSAT); - #[crate::aggregate_reduction(identity)] -impl crate::rules::AggregateReductionResult for ReductionSATToKSAT {} +impl crate::rules::AggregateReductionResult for ReductionSATToKSAT {} /// Add a clause to the K-SAT formula, splitting or padding as necessary. /// @@ -127,7 +125,9 @@ fn add_clause_to_ksat( /// Note: We implement this for specific K values rather than generic K /// because the `#[reduction]` proc macro requires concrete types. macro_rules! impl_sat_to_ksat { - ($ktype:ty, $k:expr) => { + ($ktype:ty) => { + crate::register_aggregate_reduction!(ReductionSATToKSAT<$ktype>); + #[rustfmt::skip] #[reduction(transform = upper_bound { num_clauses = "8 * num_clauses + num_literals", @@ -149,7 +149,7 @@ macro_rules! impl_sat_to_ksat { >)?; for clause in self.clauses() { - add_clause_to_ksat($k, clause, &mut result_clauses, &mut variables) + add_clause_to_ksat(<$ktype as FixedK>::WIDTH, clause, &mut result_clauses, &mut variables) .map_err(crate::rules::ReductionError::construction::< Satisfiability, KSatisfiability<$ktype>, @@ -168,19 +168,19 @@ macro_rules! impl_sat_to_ksat { } // Implement for K=3 (the canonical NP-complete case) -impl_sat_to_ksat!(K3, 3); +impl_sat_to_ksat!(K3); /// Result of reducing K-SAT to general SAT. /// /// This is a trivial embedding since K-SAT is a special case of SAT. #[derive(Debug, Clone)] -pub struct ReductionKSATToSAT { +pub struct ReductionKSATToSAT { /// The target SAT problem. target: Satisfiability, _phantom: std::marker::PhantomData, } -impl ReductionResult for ReductionKSATToSAT { +impl ReductionResult for ReductionKSATToSAT { type Source = KSatisfiability; type Target = Satisfiability; @@ -206,14 +206,11 @@ impl ReductionResult for ReductionKSATToSAT { } } -crate::register_aggregate_reduction!(ReductionKSATToSAT); -crate::register_aggregate_reduction!(ReductionKSATToSAT); - #[crate::aggregate_reduction(identity)] -impl crate::rules::AggregateReductionResult for ReductionKSATToSAT {} +impl crate::rules::AggregateReductionResult for ReductionKSATToSAT {} /// Helper function for KSAT -> SAT reduction logic (generic over K). -fn reduce_ksat_to_sat(ksat: &KSatisfiability) -> ReductionKSATToSAT { +fn reduce_ksat_to_sat(ksat: &KSatisfiability) -> ReductionKSATToSAT { let clauses = ksat.clauses().to_vec(); let target = Satisfiability::new(ksat.num_vars(), clauses); @@ -227,6 +224,8 @@ fn reduce_ksat_to_sat(ksat: &KSatisfiability) -> ReductionKSATToSA /// The `#[reduction]` macro requires concrete types. macro_rules! impl_ksat_to_sat { ($ktype:ty) => { + crate::register_aggregate_reduction!(ReductionKSATToSAT<$ktype>); + #[rustfmt::skip] #[reduction( transform = exact { diff --git a/src/unit_tests/models/formula/ksat.rs b/src/unit_tests/models/formula/ksat.rs index 72cdaee92..df7bd70f1 100644 --- a/src/unit_tests/models/formula/ksat.rs +++ b/src/unit_tests/models/formula/ksat.rs @@ -3,7 +3,7 @@ use crate::registry::ConstructionError; use crate::solvers::BruteForce; use crate::solvers::BruteForceProblem as _; use crate::traits::Problem; -use crate::variant::{K2, K3, KN}; +use crate::variant::{K2, K3}; include!("../../jl_helpers.rs"); #[test] @@ -82,15 +82,6 @@ fn test_ksat_rejects_clause_widths_other_than_k() { } } -#[test] -fn test_ksat_rejects_unbounded_clause_width() { - let error = KSatisfiability::::try_new(1, vec![CNFClause::new(vec![1])]).unwrap_err(); - assert_eq!( - error, - ConstructionError::Conversion("KSatisfiability requires a fixed clause width K".into()) - ); -} - #[test] fn test_ksat_get_clause() { let problem = KSatisfiability::::new(3, vec![CNFClause::new(vec![1, 2, 3])]); diff --git a/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs b/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs index 9ee40d61f..b6bb1ce14 100644 --- a/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs +++ b/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs @@ -103,22 +103,20 @@ fn test_acyclicpartition_empty_and_unsatisfiable_formulas() { ); } } - { - let source = KSatisfiability::::new( - 1, - vec![ - CNFClause::new(vec![1, 1, 1]), - CNFClause::new(vec![-1, -1, -1]), - ], - ); - let reduction = ReduceTo::>::reduce_to(&source).unwrap(); - assert!(BruteForce::new().solve(&source).unwrap().is_none()); - let items = reduction.target_problem().num_vertices() - 2; - for mask in 0..(1usize << items) { - let mut labels: Vec = (0..items).map(|i| (mask >> i) & 1).collect(); - labels.extend([0, 1]); - assert!(!reduction.target_problem().evaluate(&labels).unwrap().0); - } + let source = KSatisfiability::::new( + 1, + vec![ + CNFClause::new(vec![1, 1, 1]), + CNFClause::new(vec![-1, -1, -1]), + ], + ); + let reduction = ReduceTo::>::reduce_to(&source).unwrap(); + assert!(BruteForce::new().solve(&source).unwrap().is_none()); + let items = reduction.target_problem().num_vertices() - 2; + for mask in 0..(1usize << items) { + let mut labels: Vec = (0..items).map(|i| (mask >> i) & 1).collect(); + labels.extend([0, 1]); + assert!(!reduction.target_problem().evaluate(&labels).unwrap().0); } } diff --git a/src/unit_tests/rules/ksatisfiability_registersufficiency.rs b/src/unit_tests/rules/ksatisfiability_registersufficiency.rs index 036f7ac98..e9a2fbced 100644 --- a/src/unit_tests/rules/ksatisfiability_registersufficiency.rs +++ b/src/unit_tests/rules/ksatisfiability_registersufficiency.rs @@ -169,47 +169,45 @@ fn test_repeated_and_tautological_clauses() { let literals: Vec = (1..=num_vars) .flat_map(|i| [i as i64, -(i as i64)]) .collect(); - { - for code in 0..literals.len().pow(3) { - let mut remaining = code; - let clause: Vec<_> = (0..3) - .map(|_| { - let lit = literals[remaining % literals.len()]; - remaining /= literals.len(); - lit - }) + for code in 0..literals.len().pow(3) { + let mut remaining = code; + let clause: Vec<_> = (0..3) + .map(|_| { + let lit = literals[remaining % literals.len()]; + remaining /= literals.len(); + lit + }) + .collect(); + let source = + KSatisfiability::::try_new(num_vars, vec![CNFClause::new(clause)]).unwrap(); + let reduction = ReduceTo::::reduce_to(&source).unwrap(); + let layout = reduction.layout.as_ref().unwrap(); + for mask in 0..(1usize << num_vars) { + let original: Vec<_> = (0..num_vars).map(|i| mask & (1 << i) != 0).collect(); + let compact: Vec<_> = reduction + .source_variables + .iter() + .map(|&i| original[i]) .collect(); - let source = - KSatisfiability::::try_new(num_vars, vec![CNFClause::new(clause)]).unwrap(); - let reduction = ReduceTo::::reduce_to(&source).unwrap(); - let layout = reduction.layout.as_ref().unwrap(); - for mask in 0..(1usize << num_vars) { - let original: Vec<_> = (0..num_vars).map(|i| mask & (1 << i) != 0).collect(); - let compact: Vec<_> = reduction - .source_variables - .iter() - .map(|&i| original[i]) - .collect(); - let positions = layout.schedule_for_assignment(&compact); - assert!(reduction - .target_problem() - .simulate_registers(&positions) - .unwrap() - .is_some()); - let source_value = source.evaluate(&original).unwrap(); - assert_eq!( - reduction.target_problem().evaluate(&positions).unwrap(), - source_value - ); - if source_value.0 { - let decoded = reduction.extract_solution(&positions).unwrap(); - assert_eq!(source.evaluate(&decoded).unwrap(), Or(true)); - for &i in &reduction.source_variables { - assert_eq!(decoded[i], original[i]); - } - } else { - assert!(reduction.extract_solution(&positions).is_err()); + let positions = layout.schedule_for_assignment(&compact); + assert!(reduction + .target_problem() + .simulate_registers(&positions) + .unwrap() + .is_some()); + let source_value = source.evaluate(&original).unwrap(); + assert_eq!( + reduction.target_problem().evaluate(&positions).unwrap(), + source_value + ); + if source_value.0 { + let decoded = reduction.extract_solution(&positions).unwrap(); + assert_eq!(source.evaluate(&decoded).unwrap(), Or(true)); + for &i in &reduction.source_variables { + assert_eq!(decoded[i], original[i]); } + } else { + assert!(reduction.extract_solution(&positions).is_err()); } } } diff --git a/src/variant.rs b/src/variant.rs index f318d5bc7..7915730e4 100644 --- a/src/variant.rs +++ b/src/variant.rs @@ -24,6 +24,12 @@ pub trait KValue: VariantParam + Clone + 'static { const K: Option; } +/// A `KValue` with a concrete K, such as `K3`; excludes the arbitrary `KN`. +pub trait FixedK: KValue { + /// The concrete K value. + const WIDTH: usize; +} + /// Implement `VariantParam` and optionally `KValue` for a type. /// /// # Usage @@ -35,8 +41,8 @@ pub trait KValue: VariantParam + Clone + 'static { /// // Generic K value: /// impl_variant_param!(KN, "k", k: None); /// -/// // Concrete K value: -/// impl_variant_param!(K3, "k", k: Some(3)); +/// // Concrete K value (also implements `FixedK`): +/// impl_variant_param!(K3, "k", fixed_k: 3); /// ``` #[macro_export] macro_rules! impl_variant_param { @@ -52,6 +58,12 @@ macro_rules! impl_variant_param { const K: Option = $k; } }; + ($ty:ty, $cat:expr, fixed_k: $k:literal) => { + $crate::impl_variant_param!($ty, $cat, k: Some($k)); + impl $crate::variant::FixedK for $ty { + const WIDTH: usize = $k; + } + }; } /// Compose a `Problem::variant()` body from type parameter names. @@ -100,11 +112,11 @@ pub struct K5; pub struct KN; impl_variant_param!(KN, "k", k: None); -impl_variant_param!(K5, "k", k: Some(5)); -impl_variant_param!(K4, "k", k: Some(4)); -impl_variant_param!(K3, "k", k: Some(3)); -impl_variant_param!(K2, "k", k: Some(2)); -impl_variant_param!(K1, "k", k: Some(1)); +impl_variant_param!(K5, "k", fixed_k: 5); +impl_variant_param!(K4, "k", fixed_k: 4); +impl_variant_param!(K3, "k", fixed_k: 3); +impl_variant_param!(K2, "k", fixed_k: 2); +impl_variant_param!(K1, "k", fixed_k: 1); // --- VariantSpec: canonical runtime representation of a problem variant --- From 3c2f9bdaf00c0f265dc567f4b593b24f8c37a625 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Wed, 28 Oct 2026 11:28:49 -0700 Subject: [PATCH 10/12] Drop the FixedK trait Removing the KSatisfiability KN variant does not need a new variant trait. Keep KSatisfiability bounded by KValue with the runtime width check. Co-Authored-By: Claude Opus 5.5 --- src/models/formula/ksat.rs | 16 ++++++++-------- src/rules/sat_ksat.rs | 22 +++++++++++----------- src/unit_tests/models/formula/ksat.rs | 11 ++++++++++- src/variant.rs | 26 +++++++------------------- 4 files changed, 36 insertions(+), 39 deletions(-) diff --git a/src/models/formula/ksat.rs b/src/models/formula/ksat.rs index f509f578b..6d2e9bb7c 100644 --- a/src/models/formula/ksat.rs +++ b/src/models/formula/ksat.rs @@ -7,7 +7,7 @@ use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension}; use crate::traits::Problem; -use crate::variant::{FixedK, K2, K3}; +use crate::variant::{KValue, K2, K3}; use serde::{de::Error as _, Deserialize, Deserializer, Serialize}; use super::{sat::validate_cnf_literals, CNFClause}; @@ -72,7 +72,7 @@ inventory::submit! { /// This is the decision version of the problem. /// /// # Type Parameters -/// * `K` - A `FixedK` type that specifies the number of literals per clause +/// * `K` - A type implementing `KValue` that specifies the number of literals per clause /// /// # Example /// @@ -95,7 +95,7 @@ inventory::submit! { /// assert!(!solutions.is_empty()); /// ``` #[derive(Debug, Clone, Serialize)] -pub struct KSatisfiability { +pub struct KSatisfiability { /// Number of variables. num_vars: usize, /// Clauses in CNF, each with exactly K literals. @@ -110,7 +110,7 @@ struct KSatisfiabilityDef { clauses: Vec, } -impl<'de, K: FixedK> Deserialize<'de> for KSatisfiability { +impl<'de, K: KValue> Deserialize<'de> for KSatisfiability { fn deserialize(deserializer: D) -> Result where D: Deserializer<'de>, @@ -120,7 +120,7 @@ impl<'de, K: FixedK> Deserialize<'de> for KSatisfiability { } } -impl KSatisfiability { +impl KSatisfiability { /// Create a new K-SAT problem. /// /// # Panics @@ -136,7 +136,7 @@ impl KSatisfiability { clauses: Vec, ) -> Result { validate_cnf_literals(num_vars, &clauses)?; - let k = K::WIDTH; + let k = K::K.ok_or("KSatisfiability requires a fixed clause width K")?; for (i, clause) in clauses.iter().enumerate() { if clause.len() != k { return Err( @@ -199,7 +199,7 @@ impl KSatisfiability { } } -impl Problem for KSatisfiability { +impl Problem for KSatisfiability { const NAME: &'static str = "KSatisfiability"; type Solution = Vec; type Value = crate::types::Or; @@ -227,7 +227,7 @@ impl Problem for KSatisfiability { } } -impl crate::solvers::BruteForceProblem for KSatisfiability { +impl crate::solvers::BruteForceProblem for KSatisfiability { fn dimensions(&self) -> Vec { vec![2; self.num_vars] } diff --git a/src/rules/sat_ksat.rs b/src/rules/sat_ksat.rs index 9a8ccbf39..966f7ae1a 100644 --- a/src/rules/sat_ksat.rs +++ b/src/rules/sat_ksat.rs @@ -10,21 +10,21 @@ use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability}; use crate::reduction; use crate::rules::sat_helpers::SatVariableAllocator; use crate::rules::traits::{ReduceTo, ReductionResult}; -use crate::variant::{FixedK, K2, K3}; +use crate::variant::{KValue, K2, K3}; /// Result of reducing general SAT to K-SAT. /// /// This reduction transforms a SAT formula into an equisatisfiable K-SAT formula /// by introducing ancilla (auxiliary) variables. #[derive(Debug, Clone)] -pub struct ReductionSATToKSAT { +pub struct ReductionSATToKSAT { /// Number of original variables in the source problem. source_num_vars: usize, /// The target K-SAT problem. target: KSatisfiability, } -impl ReductionResult for ReductionSATToKSAT { +impl ReductionResult for ReductionSATToKSAT { type Source = Satisfiability; type Target = KSatisfiability; @@ -51,7 +51,7 @@ impl ReductionResult for ReductionSATToKSAT { } #[crate::aggregate_reduction(identity)] -impl crate::rules::AggregateReductionResult for ReductionSATToKSAT {} +impl crate::rules::AggregateReductionResult for ReductionSATToKSAT {} /// Add a clause to the K-SAT formula, splitting or padding as necessary. /// @@ -125,7 +125,7 @@ fn add_clause_to_ksat( /// Note: We implement this for specific K values rather than generic K /// because the `#[reduction]` proc macro requires concrete types. macro_rules! impl_sat_to_ksat { - ($ktype:ty) => { + ($ktype:ty, $k:expr) => { crate::register_aggregate_reduction!(ReductionSATToKSAT<$ktype>); #[rustfmt::skip] @@ -149,7 +149,7 @@ macro_rules! impl_sat_to_ksat { >)?; for clause in self.clauses() { - add_clause_to_ksat(<$ktype as FixedK>::WIDTH, clause, &mut result_clauses, &mut variables) + add_clause_to_ksat($k, clause, &mut result_clauses, &mut variables) .map_err(crate::rules::ReductionError::construction::< Satisfiability, KSatisfiability<$ktype>, @@ -168,19 +168,19 @@ macro_rules! impl_sat_to_ksat { } // Implement for K=3 (the canonical NP-complete case) -impl_sat_to_ksat!(K3); +impl_sat_to_ksat!(K3, 3); /// Result of reducing K-SAT to general SAT. /// /// This is a trivial embedding since K-SAT is a special case of SAT. #[derive(Debug, Clone)] -pub struct ReductionKSATToSAT { +pub struct ReductionKSATToSAT { /// The target SAT problem. target: Satisfiability, _phantom: std::marker::PhantomData, } -impl ReductionResult for ReductionKSATToSAT { +impl ReductionResult for ReductionKSATToSAT { type Source = KSatisfiability; type Target = Satisfiability; @@ -207,10 +207,10 @@ impl ReductionResult for ReductionKSATToSAT { } #[crate::aggregate_reduction(identity)] -impl crate::rules::AggregateReductionResult for ReductionKSATToSAT {} +impl crate::rules::AggregateReductionResult for ReductionKSATToSAT {} /// Helper function for KSAT -> SAT reduction logic (generic over K). -fn reduce_ksat_to_sat(ksat: &KSatisfiability) -> ReductionKSATToSAT { +fn reduce_ksat_to_sat(ksat: &KSatisfiability) -> ReductionKSATToSAT { let clauses = ksat.clauses().to_vec(); let target = Satisfiability::new(ksat.num_vars(), clauses); diff --git a/src/unit_tests/models/formula/ksat.rs b/src/unit_tests/models/formula/ksat.rs index df7bd70f1..72cdaee92 100644 --- a/src/unit_tests/models/formula/ksat.rs +++ b/src/unit_tests/models/formula/ksat.rs @@ -3,7 +3,7 @@ use crate::registry::ConstructionError; use crate::solvers::BruteForce; use crate::solvers::BruteForceProblem as _; use crate::traits::Problem; -use crate::variant::{K2, K3}; +use crate::variant::{K2, K3, KN}; include!("../../jl_helpers.rs"); #[test] @@ -82,6 +82,15 @@ fn test_ksat_rejects_clause_widths_other_than_k() { } } +#[test] +fn test_ksat_rejects_unbounded_clause_width() { + let error = KSatisfiability::::try_new(1, vec![CNFClause::new(vec![1])]).unwrap_err(); + assert_eq!( + error, + ConstructionError::Conversion("KSatisfiability requires a fixed clause width K".into()) + ); +} + #[test] fn test_ksat_get_clause() { let problem = KSatisfiability::::new(3, vec![CNFClause::new(vec![1, 2, 3])]); diff --git a/src/variant.rs b/src/variant.rs index 7915730e4..f318d5bc7 100644 --- a/src/variant.rs +++ b/src/variant.rs @@ -24,12 +24,6 @@ pub trait KValue: VariantParam + Clone + 'static { const K: Option; } -/// A `KValue` with a concrete K, such as `K3`; excludes the arbitrary `KN`. -pub trait FixedK: KValue { - /// The concrete K value. - const WIDTH: usize; -} - /// Implement `VariantParam` and optionally `KValue` for a type. /// /// # Usage @@ -41,8 +35,8 @@ pub trait FixedK: KValue { /// // Generic K value: /// impl_variant_param!(KN, "k", k: None); /// -/// // Concrete K value (also implements `FixedK`): -/// impl_variant_param!(K3, "k", fixed_k: 3); +/// // Concrete K value: +/// impl_variant_param!(K3, "k", k: Some(3)); /// ``` #[macro_export] macro_rules! impl_variant_param { @@ -58,12 +52,6 @@ macro_rules! impl_variant_param { const K: Option = $k; } }; - ($ty:ty, $cat:expr, fixed_k: $k:literal) => { - $crate::impl_variant_param!($ty, $cat, k: Some($k)); - impl $crate::variant::FixedK for $ty { - const WIDTH: usize = $k; - } - }; } /// Compose a `Problem::variant()` body from type parameter names. @@ -112,11 +100,11 @@ pub struct K5; pub struct KN; impl_variant_param!(KN, "k", k: None); -impl_variant_param!(K5, "k", fixed_k: 5); -impl_variant_param!(K4, "k", fixed_k: 4); -impl_variant_param!(K3, "k", fixed_k: 3); -impl_variant_param!(K2, "k", fixed_k: 2); -impl_variant_param!(K1, "k", fixed_k: 1); +impl_variant_param!(K5, "k", k: Some(5)); +impl_variant_param!(K4, "k", k: Some(4)); +impl_variant_param!(K3, "k", k: Some(3)); +impl_variant_param!(K2, "k", k: Some(2)); +impl_variant_param!(K1, "k", k: Some(1)); // --- VariantSpec: canonical runtime representation of a problem variant --- From 9b281d770bd1a37cb823a2c7e041beae161ae7a8 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Thu, 29 Oct 2026 12:18:50 +0800 Subject: [PATCH 11/12] Align K3 reduction proofs with exact-width clauses --- docs/paper/reductions.typ | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 7dc51eb83..947d23aba 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -12503,7 +12503,7 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with *Multiplicity:* The fixture stores one canonical satisfying witness. ], )[ - The bounded quadratic-congruence construction of Manders and Adleman @mandersAdleman1976 converts an odd signed-knapsack target into a square congruence using prime powers and the Chinese Remainder Theorem. We give base-eight positions only to the actual normalized clauses. The same slack equation handles every native clause width from zero through three. + The bounded quadratic-congruence construction of Manders and Adleman @mandersAdleman1976 converts an odd signed-knapsack target into a square congruence using prime powers and the Chinese Remainder Theorem. We give base-eight positions only to the actual normalized clauses. The same slack equation handles clauses of at most three literals after normalization. ][ _Construction._ Delete tautologies and duplicate literals and clauses. Compact the $l$ occurring variables, recording their original positions. Let $C_1, dots, C_m$ be the remaining clauses, $r_j = |C_j|$, $N = 2m+l+1$, and $D=8^(m+1)$. Let $f_i^+$ and $f_i^-$ be the sums of $8^j$ over clauses containing variable $i$ positively and negatively. Define $N$ integer coefficients and an odd target: $ c_0=1, quad c_(2j-1)=-8^j/2, quad c_(2j)=-8^j, quad c_(2m+i)=(f_i^+-f_i^-)/2, $ @@ -18048,9 +18048,9 @@ The following table shows concrete target-variable counts for example instances, $ Here $R$ counts literal occurrences, so its repeated $z_0$ in the global constraint is intentional. Negative literals remain permitted by the target model. Every clause uses this same construction; no empty-clause target case is needed. - _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, assign its appearing coordinates to the compact target variables and set the constants as above. Let $(x,y,z)$ be one padded clause's literal truth values. Set $d=(1-x)(1-y)$, $a=1-x-d$, $b=1-y-d$, $c=1-z$, $e=1-a-b$ and $f=z-d$. If $x=y=0$, satisfaction forces $z=1$, giving $(a,b,c,d,e,f)=(0,0,0,1,1,0)$. Otherwise $d=0$, $a=1-x$, $b=1-y$, $e=x+y-1$, and $f=z$; these and $c=1-z$ are Boolean because $x+y>=1$. Substitution gives $x+a+d=y+b+d=a+b+e=c+d+f=z+c=1$, satisfying all five constraints. Auxiliary variables are disjoint across clauses, so the assignments combine. + _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, assign its appearing coordinates to the compact target variables and set the constants as above. Let $(x,y,z)$ be one source clause's literal truth values. Set $d=(1-x)(1-y)$, $a=1-x-d$, $b=1-y-d$, $c=1-z$, $e=1-a-b$ and $f=z-d$. If $x=y=0$, satisfaction forces $z=1$, giving $(a,b,c,d,e,f)=(0,0,0,1,1,0)$. Otherwise $d=0$, $a=1-x$, $b=1-y$, $e=x+y-1$, and $f=z$; these and $c=1-z$ are Boolean because $x+y>=1$. Substitution gives $x+a+d=y+b+d=a+b+e=c+d+f=z+c=1$, satisfying all five constraints. Auxiliary variables are disjoint across clauses, so the assignments combine. - ($arrow.l.double$) Every target solution forces $z_0=0$. If a padded clause had $x=y=z=0$, the final constraint would force $c=1$; the fourth would then force $d=f=0$. The first two would force $a=b=1$, contradicting the third. Thus every padded disjunction is true, which implies every original clause is true. Repetition, opposite signs and missing positions do not change this argument. + ($arrow.l.double$) Every target solution forces $z_0=0$. If a source clause had $x=y=z=0$, the final constraint would force $c=1$; the fourth would then force $d=f=0$. The first two would force $a=b=1$, contradicting the third. Thus every source clause is true. Repeated literals and opposite signs do not change this argument. _Solution extraction._ Validate the target assignment once using the formal evaluator and reject $"Or(false)"$. Initialize a length-$n$ false vector, then restore the compact source coordinates to their original positions in $J$. Unused source variables stay false. The resolved value types are $"Or" arrow.r "Or"$. @@ -18131,7 +18131,7 @@ The following table shows concrete target-variable counts for example instances, *Multiplicity:* The fixture stores one canonical satisfying assignment. Different satisfying assignments can induce different valid computation orders in the target DAG. ], )[ - Sethi's Reduction 1 and Theorem 3.11 @sethi1973 encode literal choices through register pressure. We extend the construction to the native zero-to-three-literal clause domain by truth-preserving normalization and explicit empty-formula boundaries. The original padding $b=max(2n-m,0)$ is retained. + Sethi's Reduction 1 and Theorem 3.11 @sethi1973 encode literal choices through register pressure. The native source has exactly three literals per clause, with repeated literals permitted. We compact appearing variables and handle the empty formula explicitly. The original padding $b=max(2n-m,0)$ is retained. ][ _Normalization._ An empty conjunction is true; output the empty graph with bound zero. Otherwise collect the appearing variables in increasing original-index order, map them to $1,dots,n$, and retain the inverse map. Keep the original clause order and literal occurrences, which gives $n,m>=1$. Let $Y_(i,j)$ denote the literal at position $j$ of clause $i$, allowing repeated literals. @@ -19177,7 +19177,7 @@ The following table shows concrete target-variable counts for example instances, ][ _Construction._ Collect the sorted original indices $J$ of appearing variables, with $a = |J|$. For each compact variable $i$, create literal vertices $p_i, n_i$ and both digon arcs. For each clause create three vertices $c_(j,0), c_(j,1), c_(j,2)$ and the directed cycle in that order, then add $(c_(j,t), v(ell_(j,t)))$ for its three literal positions. Repeated literals keep separate occurrence vertices. An empty formula produces an empty graph, whose empty selection is a kernel. - _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, choose its true literal in each digon. Let $t_r$ indicate whether the literal at clause position $r$ is selected, with missing positions set to false. Select clause vertex $r$ exactly when $not t_r and t_((r+1) mod 3)$. A selected vertex points to no selected literal, and its successor cannot be selected, so independence holds. An unselected vertex with $t_r$ true is absorbed through its literal arc. Otherwise both $t_r$ and $t_((r+1) mod 3)$ are false. Since the clause is satisfied, $t_((r+2) mod 3)$ is true; its cycle successor is therefore selected and absorbs it. Unselected literal vertices are absorbed by their digon partners. + _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, choose its true literal in each digon. Let $t_r$ indicate whether the literal at clause position $r$ is selected. Select clause vertex $r$ exactly when $not t_r and t_((r+1) mod 3)$. A selected vertex points to no selected literal, and its successor cannot be selected, so independence holds. An unselected vertex with $t_r$ true is absorbed through its literal arc. Otherwise both $t_r$ and $t_((r+1) mod 3)$ are false. Since the clause is satisfied, $t_((r+2) mod 3)$ is true; its cycle successor is therefore selected and absorbs it. Unselected literal vertices are absorbed by their digon partners. ($arrow.l.double$) Each literal vertex has only its digon partner as an outgoing neighbor. Independence and absorption force exactly one selected endpoint per variable. If a clause has no selected literal, absorption must occur entirely within its directed three-cycle. Independence permits at most one selected cycle vertex, which cannot absorb both others. This contradiction proves that every clause is satisfied. This proof does not require distinct variables or a particular literal order. From 52bd171a0685cf6ab1c7b41238c7c7bf7142ee94 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Thu, 29 Oct 2026 12:38:51 +0800 Subject: [PATCH 12/12] Check matrix-cover objective range before reduction --- src/rules/maxcut_minimummatrixcover.rs | 24 +++++++++ .../rules/maxcut_minimummatrixcover.rs | 50 +++++++++++++++++++ 2 files changed, 74 insertions(+) diff --git a/src/rules/maxcut_minimummatrixcover.rs b/src/rules/maxcut_minimummatrixcover.rs index 01c7b741a..65ab21868 100644 --- a/src/rules/maxcut_minimummatrixcover.rs +++ b/src/rules/maxcut_minimummatrixcover.rs @@ -75,6 +75,30 @@ impl ReduceTo for MaxCut { fn reduce_to(&self) -> Result { let n = self.graph().num_vertices(); let edges = self.edges(); + let overflow = || { + crate::rules::ReductionError::integer_overflow::( + "bounding the matrix-cover objective", + ) + }; + // All entries are nonnegative. Their sum is attained by equal signs and + // bounds the absolute value of every signed evaluation prefix. Checking + // this sum is therefore necessary and sufficient for i64 evaluation. + let mut matrix_sum = 0_i64; + for &(_, _, weight) in &edges { + let link_sum = if weight < 0 { + weight + .checked_neg() + .and_then(|magnitude| magnitude.checked_mul(2)) + .and_then(|sum| sum.checked_add(1)) + } else { + Some(weight) + } + .ok_or_else(overflow)?; + matrix_sum = link_sum + .checked_mul(2) + .and_then(|sum| matrix_sum.checked_add(sum)) + .ok_or_else(overflow)?; + } let size = n + edges.iter().filter(|&&(_, _, w)| w < 0).count(); let mut matrix: Vec> = vec![vec![0i64; size]; size]; let mut link = |a: usize, b: usize, weight: i64| { diff --git a/src/unit_tests/rules/maxcut_minimummatrixcover.rs b/src/unit_tests/rules/maxcut_minimummatrixcover.rs index 6ad377025..78a7acd48 100644 --- a/src/unit_tests/rules/maxcut_minimummatrixcover.rs +++ b/src/unit_tests/rules/maxcut_minimummatrixcover.rs @@ -286,3 +286,53 @@ fn test_minimum_negative_weight_overflows() { crate::rules::ReductionError::IntegerOverflow { .. } )); } + +#[test] +fn test_unrepresentable_matrix_objective_is_rejected() { + for (n, edges, weights) in [ + (2, vec![(0, 1)], vec![-3_000_000_000_000_000_000]), + (2, vec![(0, 1)], vec![-((i64::MAX - 2) / 4 + 1)]), + (2, vec![(0, 1)], vec![i64::MAX / 2 + 1]), + (3, vec![(0, 1), (1, 2)], vec![-2_000_000_000_000_000_000; 2]), + ( + 3, + vec![(0, 1), (1, 2)], + vec![-1_000_000_000_000_000_000, 3_000_000_000_000_000_000], + ), + ] { + let source = MaxCut::::new(SimpleGraph::new(n, edges), weights); + // Every source configuration is evaluable, including its optimum. + let optimum = BruteForce::new().solve(&source).unwrap().unwrap(); + assert!(source.evaluate(&optimum).unwrap().0.is_some()); + assert!(matches!( + ReduceTo::::reduce_to(&source), + Err(crate::rules::ReductionError::IntegerOverflow { .. }) + )); + } +} + +#[test] +fn test_representable_matrix_objective_boundaries() { + for (weight, expected) in [(-((i64::MAX - 2) / 4), 0), (i64::MAX / 2, i64::MAX / 2)] { + let source = + MaxCut::::new(SimpleGraph::new(2, vec![(0, 1)]), vec![weight]); + let reduction = ReduceTo::::reduce_to(&source).unwrap(); + assert_optimization_round_trip_from_optimization_target( + &source, + &reduction, + "MaxCut at the matrix objective boundary", + ); + let target = reduction.target_problem(); + assert_eq!( + target.evaluate(&vec![false; target.num_rows()]).unwrap(), + Min(Some(i64::MAX - 1)) + ); + let target_optimum = BruteForce::new().solve(target).unwrap().unwrap(); + assert_eq!( + target.evaluate(&target_optimum).unwrap(), + Min(Some(-(i64::MAX - 1))) + ); + let extracted = reduction.extract_solution(&target_optimum).unwrap(); + assert_eq!(source.evaluate(&extracted).unwrap(), Max(Some(expected))); + } +}