Add SetSplitting → NAE-SAT clause-per-subset reduction

src/rules/mod.rs

@@ -146,6 +146,7 @@ pub(crate) mod satisfiability_maximum2satisfiability;
 pub(crate) mod satisfiability_naesatisfiability;
 pub(crate) mod satisfiability_nontautology;
 pub(crate) mod setsplitting_betweenness;
+pub(crate) mod setsplitting_naesatisfiability;
 mod spinglass_casts;
 pub(crate) mod spinglass_maxcut;
 pub(crate) mod spinglass_qubo;
@@ -449,6 +450,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
         optimallineararrangement_sequencingtominimizeweightedcompletiontime::canonical_rule_example_specs(),
     );
     specs.extend(setsplitting_betweenness::canonical_rule_example_specs());
+    specs.extend(setsplitting_naesatisfiability::canonical_rule_example_specs());
     specs.extend(satisfiability_integralflowhomologousarcs::canonical_rule_example_specs());
     specs.extend(satisfiability_naesatisfiability::canonical_rule_example_specs());
     specs.extend(sat_circuitsat::canonical_rule_example_specs());

src/rules/setsplitting_naesatisfiability.rs

@@ -0,0 +1,120 @@
+//! Reduction from Set Splitting to NAE-Satisfiability.
+//!
+//! Create one Boolean variable for each universe element. Each source subset
+//! becomes one NAE clause over the distinct elements it contains. A subset
+//! whose entries all equal a single element cannot be split, so emitting the
+//! clause `(x_u, x_u)` makes the target an exact mirror of the source.
+
+use crate::models::formula::{CNFClause, NAESatisfiability};
+use crate::models::set::SetSplitting;
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+
+#[derive(Debug, Clone)]
+pub struct ReductionSetSplittingToNAESAT {
+    target: NAESatisfiability,
+    source_universe_size: usize,
+}
+
+impl ReductionResult for ReductionSetSplittingToNAESAT {
+    type Source = SetSplitting;
+    type Target = NAESatisfiability;
+
+    fn target_problem(&self) -> &NAESatisfiability {
+        &self.target
+    }
+
+    fn extract_solution(
+        &self,
+        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
+    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
+        crate::rules::traits::validate_target_witness(
+            self.target_problem(),
+            target_solution,
+            |value| value.0,
+            "target witness does not satisfy the target problem",
+        )?;
+
+        Ok(target_solution[..self.source_universe_size].to_vec())
+    }
+}
+
+#[crate::aggregate_reduction(identity)]
+impl crate::rules::AggregateReductionResult for ReductionSetSplittingToNAESAT {}
+
+#[reduction(transform = {
+    exact {
+        num_vars = "universe_size",
+        num_clauses = "num_subsets",
+    },
+    upper_bound {
+        num_clause_variables = "universe_size * (universe_size + 1)",
+        num_literals = "2 * universe_size * num_subsets",
+        num_literal_pairs = "2 * universe_size * num_subsets * (2 * universe_size * num_subsets + 1)",
+    },
+})]
+impl ReduceTo<NAESatisfiability> for SetSplitting {
+    type Result = ReductionSetSplittingToNAESAT;
+
+    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
+        let universe_size = self.universe_size();
+        let mut clauses = Vec::with_capacity(self.num_subsets());
+
+        for subset in self.subsets() {
+            let mut distinct: Vec<i64> = Vec::new();
+            for &element in subset {
+                if element >= universe_size {
+                    return Err(<Self as ReduceTo<NAESatisfiability>>::target_construction(
+                        format!(
+                            "subset element {element} is outside universe of size {universe_size}"
+                        )
+                        .into(),
+                    ));
+                }
+                let literal = (element + 1) as i64;
+                if !distinct.contains(&literal) {
+                    distinct.push(literal);
+                }
+            }
+            match distinct.len() {
+                1 => distinct.push(distinct[0]),
+                0 => {
+                    return Err(<Self as ReduceTo<NAESatisfiability>>::target_construction(
+                        crate::registry::ConstructionError::from(
+                            "empty subset cannot be split".to_string(),
+                        ),
+                    ))
+                }
+                _ => {}
+            }
+            clauses.push(CNFClause::new(distinct));
+        }
+        let target = NAESatisfiability::new(universe_size, clauses);
+        Ok(ReductionSetSplittingToNAESAT {
+            target,
+            source_universe_size: universe_size,
+        })
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "setsplitting_to_naesatisfiability",
+        build: || {
+            crate::example_db::specs::rule_example_with_witness::<_, NAESatisfiability>(
+                SetSplitting::new(4, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3]]),
+                SolutionPair {
+                    source_config: serde_json::json!(vec![true, false, true, false]),
+                    target_config: serde_json::json!(vec![true, false, true, false]),
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/setsplitting_naesatisfiability.rs"]
+mod tests;

src/unit_tests/rules/setsplitting_naesatisfiability.rs

@@ -0,0 +1,104 @@
+use crate::models::formula::NAESatisfiability;
+use crate::models::set::SetSplitting;
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target;
+use crate::rules::{ReduceTo, ReductionResult};
+use crate::solvers::BruteForce;
+use crate::traits::Problem;
+
+fn rule_example_problem() -> SetSplitting {
+    SetSplitting::new(4, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3]])
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_closed_loop() {
+    let source = rule_example_problem();
+    let reduction =
+        ReduceTo::<NAESatisfiability>::reduce_to(&source).expect("reduction should succeed");
+
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &reduction,
+        "SetSplitting -> NAE-SAT",
+    );
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_structure() {
+    let source = rule_example_problem();
+    let reduction =
+        ReduceTo::<NAESatisfiability>::reduce_to(&source).expect("reduction should succeed");
+    let target = reduction.target_problem();
+
+    assert_eq!(target.num_vars(), 4);
+    assert_eq!(target.num_clauses(), 3);
+    assert_eq!(
+        target
+            .clauses()
+            .iter()
+            .map(|clause| clause.literals.clone())
+            .collect::<Vec<_>>(),
+        vec![vec![1, 2], vec![2, 3, 4], vec![1, 3, 4]],
+    );
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_repeated_members() {
+    let source = SetSplitting::new(1, vec![vec![0, 0]]);
+    let reduction =
+        ReduceTo::<NAESatisfiability>::reduce_to(&source).expect("reduction should succeed");
+
+    assert_eq!(reduction.target_problem().clauses()[0].literals, [1, 1]);
+    assert!(BruteForce::new()
+        .solve(reduction.target_problem())
+        .unwrap()
+        .is_none());
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_extract_solution() {
+    let source = rule_example_problem();
+    let reduction =
+        ReduceTo::<NAESatisfiability>::reduce_to(&source).expect("reduction should succeed");
+
+    assert_eq!(
+        reduction
+            .extract_solution(&vec![true, false, true, false])
+            .unwrap(),
+        vec![true, false, true, false]
+    );
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_target_witness_extracts_to_satisfying_assignment() {
+    let source = rule_example_problem();
+    let reduction =
+        ReduceTo::<NAESatisfiability>::reduce_to(&source).expect("reduction should succeed");
+    let solver = BruteForce::new();
+
+    let target_solution = solver.solve(reduction.target_problem()).unwrap().unwrap();
+    let source_solution = reduction.extract_solution(&target_solution).unwrap();
+
+    assert!(source.evaluate(&source_solution).unwrap());
+}
+
+#[cfg(feature = "example-db")]
+#[test]
+fn test_setsplitting_to_naesatisfiability_canonical_example_spec() {
+    let specs = crate::rules::setsplitting_naesatisfiability::canonical_rule_example_specs();
+    assert_eq!(specs.len(), 1);
+
+    let example = (specs[0].build)();
+    assert_eq!(example.source.problem, "SetSplitting");
+    assert_eq!(example.target.problem, "NAESatisfiability");
+    assert_eq!(example.solutions.len(), 1);
+
+    let pair = &example.solutions[0];
+    assert_eq!(
+        pair.source_config,
+        serde_json::json!([true, false, true, false])
+    );
+    assert_eq!(
+        pair.target_config,
+        serde_json::json!([true, false, true, false])
+    );
+}