Merge pull request #1222 from CodingThrust/fix/ilp-nonzeros-bounds

Tighten ILP num_nonzeros bounds to per-constraint counts

Author: GiggleLiu

docs/paper/reductions.typ

@@ -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"));
     }
 

problemreductions-cli/src/cli.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<Vec<bool>>", 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<Vec<bool>>,
-    bound: i64,
+    bound: usize,
 }
 
 #[derive(Deserialize)]
 struct ConsecutiveOnesSubmatrixData {
     matrix: Vec<Vec<bool>>,
-    bound: i64,
+    bound: usize,
 }
 
 impl TryFrom<ConsecutiveOnesSubmatrixData> for ConsecutiveOnesSubmatrix {
@@ -85,19 +85,19 @@ impl ConsecutiveOnesSubmatrix {
     /// # Panics
     ///
     /// Panics if `bound > n`, or if rows have inconsistent lengths.
-    pub fn new(matrix: Vec<Vec<bool>>, bound: i64) -> Self {
+    pub fn new(matrix: Vec<Vec<bool>>, bound: usize) -> Self {
         Self::try_new(matrix, bound).unwrap_or_else(|error| panic!("{error}"))
     }
 
     fn try_new(
         matrix: Vec<Vec<bool>>,
-        bound: i64,
+        bound: usize,
     ) -> Result<Self, crate::registry::ConstructionError> {
         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 !(bound < 0 || usize::try_from(bound).is_ok_and(|bound| bound <= n)) {
+        if bound > n {
             return Err(format!("bound ({bound}) must be <= number of columns ({n})").into());
         }
         Ok(Self { matrix, bound })
@@ -109,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
     }
 
@@ -222,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)

src/models/algebraic/consecutive_ones_submatrix.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<K: KValue> KSatisfiability<K> {
     /// 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<CNFClause>) -> 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<CNFClause>,
     ) -> Result<Self, crate::registry::ConstructionError> {
         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<CNFClause>) -> 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<CNFClause>,
-    ) -> Result<Self, crate::registry::ConstructionError> {
-        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<K: KValue> crate::solvers::BruteForceProblem for KSatisfiability<K> {
 }
 
 crate::declare_variants! {
-    default KSatisfiability<KN> => "2^num_vars",
+    default KSatisfiability<K3> => "1.307^num_vars" aliases ["3SAT"],
     KSatisfiability<K2> => "num_vars + num_clauses" aliases ["2SAT"],
-    KSatisfiability<K3> => "1.307^num_vars" aliases ["3SAT"],
 }
 
 crate::register_brute_force! {
-    KSatisfiability<KN> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
     KSatisfiability<K2> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
     KSatisfiability<K3> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
 }

src/models/formula/ksat.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)",
     },

src/rules/biconnectivityaugmentation_ilp.rs

@@ -55,7 +55,7 @@ impl ReductionResult for ReductionBPToILP {
     },
     upper_bound {
         max_constraint_magnitude_bits = "max_numeric_magnitude_bits",
-        num_nonzeros = "(num_items * num_items + num_items) * (2 * num_items)",
+        num_nonzeros = "2 * num_items * num_items + num_items",
     },
 })]
 impl ReduceTo<ILP<bool>> for BinPacking<i64> {

src/rules/binpacking_ilp.rs

@@ -125,7 +125,7 @@ fn decode_one_hot(
     },
     upper_bound {
         max_constraint_magnitude_bits = "substring_length + 1",
-        num_nonzeros = "(alphabet_size * substring_length + total_num_windows + 1) * (substring_length + num_strings + total_num_windows + 1)",
+        num_nonzeros = "alphabet_size * substring_length + 1 + total_num_windows * (substring_length + 3)",
     },
 })]
 impl ReduceTo<ILP<i64, i64, Bounded>> for ClosestSubstring {

src/rules/closestsubstring_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 {
-    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 * (num_elements - 1) / 2 * num_clusters)",
+#[reduction(transform = {
+    exact {
+        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",
+    },
 })]
 impl ReduceTo<ILP<bool>> for Clustering {
     type Result = ReductionClusteringToILP;

src/rules/clustering_ilp.rs

@@ -43,11 +43,15 @@ impl ReductionResult for ReductionCBMToILP {
 impl crate::rules::AggregateReductionResult for ReductionCBMToILP {}
 
 #[reduction(
-    transform = upper_bound {
-        max_constraint_magnitude_bits = "num_rows * num_cols + 1",
-        num_vars = "num_cols * num_cols + num_rows * num_cols + num_rows * num_cols",
-        num_constraints = "num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1",
-        num_nonzeros = "(num_cols * num_cols + num_rows * num_cols + num_rows * num_cols) * (num_cols + num_cols + num_rows * num_cols + num_rows + 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<ILP<bool>> for ConsecutiveBlockMinimization {

src/rules/consecutiveblockminimization_ilp.rs

@@ -46,19 +46,23 @@ impl ReductionResult for ReductionCOSToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionCOSToILP {}
 
-#[reduction(transform = 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 = "(num_cols + num_cols * bound + 5 * num_rows * bound) * (2 + num_cols + bound + 3 * num_rows + 8 * num_rows * 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_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<ILP<bool>> for ConsecutiveOnesSubmatrix {
     type Result = ReductionCOSToILP;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         let m = self.num_rows();
         let n = self.num_cols();
-        let k = self.bound() as usize;
+        let k = self.bound();
 
         // Variable layout (all binary):
         // s_c: n vars at [0, n)  — column selection