feat: add NAESatisfiability → SetSplitting reduction (#841) [full pipeline v2]

src/rules/mod.rs

@@ -59,6 +59,7 @@ pub(crate) mod minimumvertexcover_minimumfeedbackvertexset;
 pub(crate) mod minimumvertexcover_minimumhittingset;
 pub(crate) mod minimumvertexcover_minimumsetcovering;
 pub(crate) mod naesatisfiability_maxcut;
+pub(crate) mod naesatisfiability_setsplitting;
 pub(crate) mod paintshop_qubo;
 pub(crate) mod partition_binpacking;
 pub(crate) mod partition_cosineproductintegration;
@@ -341,6 +342,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(partition_subsetsum::canonical_rule_example_specs());
     specs.extend(rootedtreearrangement_rootedtreestorageassignment::canonical_rule_example_specs());
     specs.extend(naesatisfiability_maxcut::canonical_rule_example_specs());
+    specs.extend(naesatisfiability_setsplitting::canonical_rule_example_specs());
     specs.extend(exactcoverby3sets_maximumsetpacking::canonical_rule_example_specs());
     specs.extend(maxcut_minimumcutintoboundedsets::canonical_rule_example_specs());
     specs.extend(partition_binpacking::canonical_rule_example_specs());

src/rules/naesatisfiability_setsplitting.rs

@@ -0,0 +1,134 @@
+//! Reduction from NAE-Satisfiability to Set Splitting.
+//!
+//! Given an NAE-SAT instance with n variables and m clauses, we construct a
+//! Set Splitting instance on universe {0, ..., 2n-1} where element 2i
+//! represents variable x_{i+1} being true and element 2i+1 represents it
+//! being false.
+//!
+//! The reduction adds two kinds of subsets:
+//! - Complementarity subsets {2i, 2i+1} for each variable i, ensuring that
+//!   each variable and its complement are assigned different colors.
+//! - Clause subsets mapping each NAE clause via literal_to_element, ensuring
+//!   the NAE condition (not all equal) maps to the set splitting condition
+//!   (non-monochromatic).
+
+use crate::models::formula::NAESatisfiability;
+use crate::models::set::SetSplitting;
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+
+/// Result of reducing NAE-Satisfiability to Set Splitting.
+#[derive(Debug, Clone)]
+pub struct ReductionNAESATToSetSplitting {
+    /// Number of variables in the source problem.
+    num_vars: usize,
+    /// The target Set Splitting problem.
+    target: SetSplitting,
+}
+
+impl ReductionResult for ReductionNAESATToSetSplitting {
+    type Source = NAESatisfiability;
+    type Target = SetSplitting;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+        // Variable i is true iff element 2i is in part 0 (color 0).
+        // So assignment[i] = 1 - target_solution[2*i].
+        (0..self.num_vars)
+            .map(|i| 1 - target_solution[2 * i])
+            .collect()
+    }
+}
+
+/// Convert a 1-indexed signed literal to a 0-indexed universe element.
+///
+/// Positive literal i -> element 2*(i-1).
+/// Negative literal -i -> element 2*(i-1)+1.
+fn literal_to_element(lit: i32) -> usize {
+    let var_idx = (lit.unsigned_abs() as usize) - 1;
+    if lit > 0 {
+        2 * var_idx
+    } else {
+        2 * var_idx + 1
+    }
+}
+
+#[reduction(overhead = {
+    universe_size = "2 * num_vars",
+    num_subsets = "num_clauses + num_vars",
+})]
+impl ReduceTo<SetSplitting> for NAESatisfiability {
+    type Result = ReductionNAESATToSetSplitting;
+
+    fn reduce_to(&self) -> Self::Result {
+        let n = self.num_vars();
+        let universe_size = 2 * n;
+
+        let mut subsets = Vec::with_capacity(n + self.num_clauses());
+
+        // Complementarity subsets: {2i, 2i+1} for each variable i
+        for i in 0..n {
+            subsets.push(vec![2 * i, 2 * i + 1]);
+        }
+
+        // Clause subsets: map each literal to its universe element
+        for clause in self.clauses() {
+            let subset: Vec<usize> = clause
+                .literals
+                .iter()
+                .map(|&lit| literal_to_element(lit))
+                .collect();
+            subsets.push(subset);
+        }
+
+        let target = SetSplitting::new(universe_size, subsets);
+
+        ReductionNAESATToSetSplitting {
+            num_vars: n,
+            target,
+        }
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+    use crate::models::formula::CNFClause;
+
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "naesatisfiability_to_setsplitting",
+        build: || {
+            // YES instance from test vectors: n=4,
+            // clauses=[[1,2,3],[-1,3,4],[2,-3,-4],[1,-2,4]]
+            let source = NAESatisfiability::new(
+                4,
+                vec![
+                    CNFClause::new(vec![1, 2, 3]),
+                    CNFClause::new(vec![-1, 3, 4]),
+                    CNFClause::new(vec![2, -3, -4]),
+                    CNFClause::new(vec![1, -2, 4]),
+                ],
+            );
+            // source_solution: [1,0,1,0] means x1=T, x2=F, x3=T, x4=F
+            // target_config: element 2i = 1 - assignment[i]
+            //   x1=T -> config[0]=0, config[1]=1
+            //   x2=F -> config[2]=1, config[3]=0
+            //   x3=T -> config[4]=0, config[5]=1
+            //   x4=F -> config[6]=1, config[7]=0
+            crate::example_db::specs::rule_example_with_witness::<_, SetSplitting>(
+                source,
+                SolutionPair {
+                    source_config: vec![1, 0, 1, 0],
+                    target_config: vec![0, 1, 1, 0, 0, 1, 1, 0],
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/naesatisfiability_setsplitting.rs"]
+mod tests;

src/unit_tests/rules/naesatisfiability_setsplitting.rs

@@ -0,0 +1,188 @@
+use super::*;
+use crate::models::formula::CNFClause;
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target;
+use crate::solvers::BruteForce;
+use crate::traits::Problem;
+
+#[test]
+fn test_naesatisfiability_to_setsplitting_closed_loop() {
+    // YES instance from test vectors: n=4
+    // clauses: (x1,x2,x3), (-x1,x3,x4), (x2,-x3,-x4), (x1,-x2,x4)
+    let naesat = NAESatisfiability::new(
+        4,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![-1, 3, 4]),
+            CNFClause::new(vec![2, -3, -4]),
+            CNFClause::new(vec![1, -2, 4]),
+        ],
+    );
+
+    let reduction = ReduceTo::<SetSplitting>::reduce_to(&naesat);
+
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &naesat,
+        &reduction,
+        "NAESAT->SetSplitting closed loop",
+    );
+}
+
+#[test]
+fn test_naesatisfiability_to_setsplitting_infeasible() {
+    // NO instance from test vectors: n=3
+    // clauses: (x1,x2,x3), (x1,x2,-x3), (x1,-x2,x3), (x1,-x2,-x3)
+    // This is infeasible because x1 must be both true and false.
+    let naesat = NAESatisfiability::new(
+        3,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![1, 2, -3]),
+            CNFClause::new(vec![1, -2, 3]),
+            CNFClause::new(vec![1, -2, -3]),
+        ],
+    );
+
+    let reduction = ReduceTo::<SetSplitting>::reduce_to(&naesat);
+    let target = reduction.target_problem();
+
+    let solver = BruteForce::new();
+    let naesat_solutions = solver.find_all_witnesses(&naesat);
+    let splitting_solutions = solver.find_all_witnesses(target);
+
+    assert!(naesat_solutions.is_empty(), "NAESAT should be infeasible");
+    assert!(
+        splitting_solutions.is_empty(),
+        "SetSplitting should also be infeasible"
+    );
+}
+
+#[test]
+fn test_reduction_structure() {
+    let naesat = NAESatisfiability::new(
+        4,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![-1, 3, 4]),
+            CNFClause::new(vec![2, -3, -4]),
+            CNFClause::new(vec![1, -2, 4]),
+        ],
+    );
+
+    let reduction = ReduceTo::<SetSplitting>::reduce_to(&naesat);
+    let target = reduction.target_problem();
+
+    // universe_size = 2 * num_vars = 8
+    assert_eq!(target.universe_size(), 8);
+    // num_subsets = num_vars + num_clauses = 4 + 4 = 8
+    assert_eq!(target.num_subsets(), 8);
+
+    // First 4 subsets are complementarity: {0,1}, {2,3}, {4,5}, {6,7}
+    let subsets = target.subsets();
+    for (i, subset) in subsets.iter().enumerate().take(4) {
+        assert_eq!(*subset, vec![2 * i, 2 * i + 1]);
+    }
+
+    // Clause subsets follow the literal mapping
+    // Clause [1,2,3] -> [0,2,4]
+    assert_eq!(subsets[4], vec![0, 2, 4]);
+    // Clause [-1,3,4] -> [1,4,6]
+    assert_eq!(subsets[5], vec![1, 4, 6]);
+    // Clause [2,-3,-4] -> [2,5,7]
+    assert_eq!(subsets[6], vec![2, 5, 7]);
+    // Clause [1,-2,4] -> [0,3,6]
+    assert_eq!(subsets[7], vec![0, 3, 6]);
+}
+
+#[test]
+fn test_solution_extraction() {
+    let naesat = NAESatisfiability::new(
+        4,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![-1, 3, 4]),
+        ],
+    );
+
+    let reduction = ReduceTo::<SetSplitting>::reduce_to(&naesat);
+
+    // target_solution: [0, 1, 1, 0, 0, 1, 1, 0]
+    // assignment[i] = 1 - target_solution[2*i]
+    // x1 = 1-0 = 1 (true), x2 = 1-1 = 0 (false), x3 = 1-0 = 1 (true), x4 = 1-1 = 0 (false)
+    let extracted = reduction.extract_solution(&[0, 1, 1, 0, 0, 1, 1, 0]);
+    assert_eq!(extracted, vec![1, 0, 1, 0]);
+}
+
+#[test]
+fn test_all_satisfying_assignments_map_back() {
+    // Small instance: verify every SetSplitting solution maps to a valid NAESAT solution
+    let naesat = NAESatisfiability::new(
+        3,
+        vec![
+            CNFClause::new(vec![1, 2, -3]),
+            CNFClause::new(vec![-1, 3]),
+        ],
+    );
+
+    let reduction = ReduceTo::<SetSplitting>::reduce_to(&naesat);
+    let target = reduction.target_problem();
+
+    let solver = BruteForce::new();
+    let splitting_solutions = solver.find_all_witnesses(target);
+
+    assert!(
+        !splitting_solutions.is_empty(),
+        "SetSplitting should have solutions"
+    );
+
+    for sol in &splitting_solutions {
+        let naesat_sol = reduction.extract_solution(sol);
+        assert_eq!(naesat_sol.len(), 3);
+        assert!(
+            naesat.evaluate(&naesat_sol).0,
+            "Extracted solution {:?} from splitting solution {:?} does not satisfy NAESAT",
+            naesat_sol,
+            sol
+        );
+    }
+}
+
+#[test]
+fn test_larger_instance_closed_loop() {
+    let naesat = NAESatisfiability::new(
+        5,
+        vec![
+            CNFClause::new(vec![1, 2, -3]),
+            CNFClause::new(vec![-1, 3, 4]),
+            CNFClause::new(vec![2, -4, 5]),
+            CNFClause::new(vec![-2, 3, -5]),
+            CNFClause::new(vec![1, -3, 5]),
+        ],
+    );
+
+    let reduction = ReduceTo::<SetSplitting>::reduce_to(&naesat);
+
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &naesat,
+        &reduction,
+        "NAESAT->SetSplitting larger instance",
+    );
+}
+
+#[test]
+fn test_two_variable_instance() {
+    // Minimal instance with 2 variables
+    let naesat = NAESatisfiability::new(2, vec![CNFClause::new(vec![1, -2])]);
+
+    let reduction = ReduceTo::<SetSplitting>::reduce_to(&naesat);
+    let target = reduction.target_problem();
+
+    assert_eq!(target.universe_size(), 4);
+    // 2 complementarity + 1 clause = 3 subsets
+    assert_eq!(target.num_subsets(), 3);
+
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &naesat,
+        &reduction,
+        "NAESAT->SetSplitting two-variable",
+    );
+}