Merge pull request #1218 from CodingThrust/feat/binary-ilp-to-sat

Add binary decision ILP to SAT and fix solution validators

Author: GiggleLiu

docs/paper/reductions.typ

@@ -2332,3 +2332,14 @@ @article{axler2019
   year = {2019},
   url = {https://www.maths.tcd.ie/EMIS/journals/JIS/VOL22/Axler/axler17.pdf}
 }
+
+@article{een2006,
+  author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
+  title = {Translating Pseudo-Boolean Constraints into {SAT}},
+  journal = {Journal on Satisfiability, Boolean Modeling and Computation},
+  year = {2006},
+  volume = {2},
+  number = {1--4},
+  pages = {1--26},
+  doi = {10.3233/SAT190014},
+}

docs/paper/references.bib

@@ -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

@@ -747,7 +747,7 @@ fn test_create_path_constrained_network_flow_rejects_invalid_paths() {
 }
 
 #[test]
-fn test_create_staff_scheduling_reports_invalid_schedule_without_panic() {
+fn test_create_staff_scheduling_rejects_ragged_schedule() {
     let cli = Cli::try_parse_from([
         "pred",
         "create",
@@ -775,14 +775,7 @@ fn test_create_staff_scheduling_reports_invalid_schedule_without_panic() {
         auto_json: false,
     };
 
-    let result = std::panic::catch_unwind(|| create(&args, &out));
-    assert!(result.is_ok(), "create should return an error, not panic");
-    let err = result.unwrap().unwrap_err().to_string();
-    // parse_bool_rows catches ragged rows before validate_staff_scheduling_args
-    assert!(
-        err.contains("All rows") || err.contains("schedule 1 has 6 periods, expected 7"),
-        "expected row-length validation error, got: {err}"
-    );
+    assert!(create(&args, &out).is_err());
 }
 
 #[test]
@@ -955,7 +948,7 @@ fn test_create_timetable_design_outputs_problem_json() {
 }
 
 #[test]
-fn test_create_timetable_design_reports_invalid_matrix_without_panic() {
+fn test_create_timetable_design_rejects_invalid_matrix() {
     let cli = Cli::try_parse_from([
         "pred",
         "create",
@@ -987,13 +980,7 @@ fn test_create_timetable_design_reports_invalid_matrix_without_panic() {
         auto_json: false,
     };
 
-    let result = std::panic::catch_unwind(|| create(&args, &out));
-    assert!(result.is_ok(), "create should return an error, not panic");
-    let err = result.unwrap().unwrap_err().to_string();
-    assert!(
-        err.contains("--craftsman-avail"),
-        "expected timetable matrix validation error, got: {err}"
-    );
+    assert!(create(&args, &out).is_err());
 }
 
 #[test]

problemreductions-cli/src/commands/create/tests.rs

@@ -1340,38 +1340,6 @@ mod tests {
         assert_eq!(error.to_string(), "duplicate `create` clause");
     }
 
-    #[test]
-    fn declare_variants_generates_model_dispatch_without_solver_dispatch() {
-        let input: DeclareVariantsInput = syn::parse_quote! {
-            default Foo => "1",
-        };
-        let tokens = generate_declare_variants(&input).unwrap().to_string();
-        assert!(tokens.contains("factory :"), "expected factory field");
-        assert!(
-            tokens.contains("serialize_fn :"),
-            "expected serialize_fn field"
-        );
-        assert!(!tokens.contains("solve_typed_fn :"));
-        assert!(!tokens.contains("solve_fn :"));
-        assert!(
-            !tokens.contains("factory : None"),
-            "factory should not be None"
-        );
-        assert!(
-            !tokens.contains("serialize_fn : None"),
-            "serialize_fn should not be None"
-        );
-        assert!(!tokens.contains("find_cartesian"));
-        assert!(
-            !tokens.contains("find_best"),
-            "did not expect legacy find_best in tokens"
-        );
-        assert!(
-            !tokens.contains("SolutionSize :: Invalid"),
-            "did not expect legacy invalid fallback in tokens"
-        );
-    }
-
     #[test]
     fn reduction_rejects_unexpected_attribute() {
         let extra_attr = syn::Ident::new("extra", proc_macro2::Span::call_site());

problemreductions-macros/src/lib.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

@@ -690,9 +690,41 @@ crate::declare_variants! {
     ILP<i64, f64> => "num_vars^num_vars",
 }
 
+impl crate::solvers::BruteForceProblem for ILP<bool> {
+    fn dimensions(&self) -> Vec<usize> {
+        vec![2; self.num_vars()]
+    }
+}
+
+crate::decision_problem_meta!(ILP<bool>, "DecisionILP");
+crate::register_decision_variant!(without_turing;
+    ILP<bool>, "DecisionILP", "2^num_vars", &[],
+    "Does a binary ILP have a feasible solution meeting its objective bound?",
+    category: crate::registry::ProblemCategory::Algebraic,
+    dims: [
+        VariantDimension::new("variable", "bool", &["bool"]),
+        VariantDimension::new("coefficient", "i64", &["i64"]),
+        VariantDimension::new("bounds", "general", &["general"]),
+    ],
+    fields: [
+        FieldInfo { name: "variables", type_name: "Vec<IntegerVariable>", description: "Binary variable bounds [0, 1]" },
+        FieldInfo { name: "constraints", type_name: "Vec<LinearConstraint<i64>>", description: "Sparse integer linear constraints" },
+        FieldInfo { name: "objective", type_name: "Vec<(usize, i64)>", description: "Sparse integer objective coefficients" },
+        FieldInfo { name: "sense", type_name: "ObjectiveSense", description: "Optimization direction" },
+        FieldInfo { name: "bound", type_name: "i64", description: "Upper bound for minimization, lower bound for maximization" },
+    ],
+    decode: |_, indices: Vec<usize>| indices.into_iter().map(|bit| i64::try_from(bit).expect("binary coordinate fits i64")).collect::<Vec<_>>()
+);
+
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
     vec![
+        crate::example_db::specs::ModelExampleSpec {
+            id: "decision_ilp",
+            instance: Box::new(canonical_decision_example()),
+            optimal_config: serde_json::json!([0, 0, 1]),
+            optimal_value: serde_json::json!(true),
+        },
         crate::example_db::specs::ModelExampleSpec {
             id: "ilp",
             instance: Box::new(
@@ -733,3 +765,17 @@ pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::M
 #[cfg(test)]
 #[path = "../../unit_tests/models/algebraic/ilp.rs"]
 mod tests;
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_decision_example() -> crate::models::Decision<ILP<bool>> {
+    crate::models::Decision::new(
+        ILP::new(
+            3,
+            vec![LinearConstraint::eq(vec![(0, 1), (1, 1), (2, 1)], 1)],
+            vec![(0, 3), (1, 2), (2, 1)],
+            ObjectiveSense::Minimize,
+        )
+        .unwrap(),
+        1,
+    )
+}

src/models/algebraic/ilp.rs

@@ -31,9 +31,16 @@ macro_rules! decision_problem_meta {
 /// variant's construction fields and decoder without adding another schema or default.
 /// Both decision/optimization edges derive their identity parameter transforms directly
 /// from the inner problem's canonical parameter schema.
+/// Prefix with `without_turing;` to omit the reverse optimization-to-decision Turing edge.
 #[macro_export]
 macro_rules! register_decision_variant {
-    (
+    (without_turing; $($body:tt)*) => {
+        $crate::register_decision_variant!(@register witness_edge; $($body)*);
+    };
+    ($inner:ty, $($body:tt)*) => {
+        $crate::register_decision_variant!(@register edges; $inner, $($body)*);
+    };
+    (@register $edges:ident;
         $inner:ty,
         $name:literal,
         $complexity:literal,
@@ -61,16 +68,16 @@ macro_rules! register_decision_variant {
             }
         }
 
-        $crate::register_decision_variant!(@edges $inner, $name);
+        $crate::register_decision_variant!(@$edges $inner, $name);
         $($(
             $crate::register_brute_force! {
                 $crate::models::decision::Decision<$additional> decode $decoder,
             }
-            $crate::register_decision_variant!(@edges $additional, $name);
+            $crate::register_decision_variant!(@$edges $additional, $name);
         )*)?
     };
 
-    (@edges $inner:ty, $name:literal) => {
+    (@witness_edge $inner:ty, $name:literal) => {
         // Decision<P> → P: both witness (identity config) and aggregate (solve + compare)
         $crate::inventory::submit! {
             $crate::rules::ReductionEntry {
@@ -114,7 +121,10 @@ macro_rules! register_decision_variant {
                 turing: false,
             }
         }
+    };
 
+    (@edges $inner:ty, $name:literal) => {
+        $crate::register_decision_variant!(@witness_edge $inner, $name);
         // Reverse edge: P → Decision<P> (Turing/multi-query reduction via binary search)
         $crate::inventory::submit! {
             $crate::rules::ReductionEntry {