Fix #1100: SetSplitting to NAESatisfiability

docs/paper/reductions.typ

@@ -18775,6 +18775,49 @@ The following table shows concrete variable overhead for example instances, take
   _Solution extraction._ Set $alpha(x_(i+1)) = chi(2i)$ for $i = 0, dots, n-1$.
 ]
 
+// 8a. SetSplitting → NAESatisfiability
+#let ss_nae = load-example("SetSplitting", "NAESatisfiability")
+#let ss_nae_sol = ss_nae.solutions.at(0)
+#reduction-rule("SetSplitting", "NAESatisfiability",
+  example: true,
+  example-caption: [$|U| = #ss_nae.source.instance.universe_size$, $#ss_nae.source.instance.subsets.len()$ subsets, and $#ss_nae.target.instance.clauses.len()$ NAE clauses],
+  extra: [
+    #pred-commands(
+      "pred create --example " + problem-spec(ss_nae.source) + " -o set-splitting.json",
+      "pred reduce set-splitting.json --to " + target-spec(ss_nae) + " -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate set-splitting.json --config " + ss_nae_sol.source_config.map(str).join(","),
+    )
+
+    #{
+      let source = ss_nae.source.instance
+      let target = ss_nae.target.instance
+      let colors = ss_nae_sol.source_config
+      [
+        *Step 1 -- Start from the set family.* The universe is $U = {0, dots, #(source.universe_size - 1)}$, with subsets $S_1 = {#source.subsets.at(0).map(str).join(", ")}$, $S_2 = {#source.subsets.at(1).map(str).join(", ")}$, and $S_3 = {#source.subsets.at(2).map(str).join(", ")}$. The fixture's splitting is $(#colors.map(str).join(", "))$.
+
+        *Step 2 -- Turn elements into variables and subsets into clauses.* The target has $#target.num_vars$ variables, one for each universe element. In signed one-indexed storage, the three canonicalized subsets become the positive-literal clauses $(#target.clauses.at(0).literals.map(str).join(", "))$, $(#target.clauses.at(1).literals.map(str).join(", "))$, and $(#target.clauses.at(2).literals.map(str).join(", "))$. Thus this fixture has $#target.clauses.len()$ clauses and $#target.clauses.map(c => c.literals.len()).sum()$ literal occurrences.
+
+        *Step 3 -- Verify the NAE assignment.* Under the source colors, the three subsets have truth patterns $(#source.subsets.at(0).map(u => colors.at(u)).map(str).join(", "))$, $(#source.subsets.at(1).map(u => colors.at(u)).map(str).join(", "))$, and $(#source.subsets.at(2).map(u => colors.at(u)).map(str).join(", "))$. Every pattern contains both 0 and 1, so the identical target assignment $(#ss_nae_sol.target_config.map(str).join(", "))$ NAE-satisfies every clause. Extracting it unchanged recovers the source splitting $(#colors.map(str).join(", "))$ #sym.checkmark.
+
+        *Multiplicity:* The fixture stores one canonical witness. Because construction and extraction leave the configuration vector unchanged, every valid splitting corresponds to exactly one satisfying target assignment and conversely.
+      ]
+    }
+  ],
+)[
+  This $O(n + sum_(j=1)^m |S_j|)$ reduction @garey1979 @schaefer1978 identifies a two-way split with a Boolean assignment. It creates one variable for each of the $n$ universe elements and one positive-literal NAE clause for each of the $m$ source subset vectors. The target has exactly $n$ variables and $m$ clauses; its literal count is at most $(n + 1)m$.
+][
+  _Construction._ Let the Set Splitting instance have universe $U = {0, dots, n - 1}$ and subset vectors $S_1, dots, S_m$. Introduce a Boolean variable $x_u$ for each $u in U$, with its truth value denoting the side assigned to $u$. For each $S_j$, scan its entries from left to right and retain only the first occurrence of each distinct element, obtaining the canonical sequence $D_j$. If $|D_j| >= 2$, emit the NAE clause $C_j = (x_u : u in D_j)$, using only positive literals. If $D_j = (u)$, emit $C_j = (x_u, x_u)$. The implementation stores positive literal $x_u$ as the signed one-indexed integer $u + 1$.
+
+  Duplicate removal preserves the first-seen order for deterministic output and does not affect which colors occur in a subset. The exact literal count is $sum_j max(2, |D_j|)$, bounded by $(n + 1)m$; the variable and clause counts are exactly $n$ and $m$.
+
+  _Correctness._ ($arrow.r.double$) Let $chi: U -> {0, 1}$ split every source subset, and assign $x_u = chi(u)$. Removing duplicates does not remove either color from a split subset, so every $D_j$ contains elements of both colors and $C_j$ has both truth values. Hence every target clause satisfies NAE. ($arrow.l.double$) Let $bold(x)$ NAE-satisfy every target clause and color element $u$ by $chi(u) = x_u$. A repeated-literal clause $(x_u, x_u)$ can never satisfy NAE, so no all-repeated source subset can occur in a satisfiable target instance. Every other clause contains both truth values; therefore its canonical sequence $D_j$, and hence the original subset vector $S_j$, contains elements on both sides of the split. Thus $chi$ splits every source subset.
+
+  An all-repeated vector such as $(u, u, dots, u)$ is therefore preserved as a NO constraint: canonicalization finds only $u$, and the emitted $(x_u, x_u)$ is false under both possible values of $x_u$.
+
+  _Solution extraction._ Return the target assignment unchanged: the source color of universe element $u$ is $x_u$.
+]
+
 // 6b. NAESatisfiability → PartitionIntoPerfectMatchings (#845)
 #let nae_ppm = load-example("NAESatisfiability", "PartitionIntoPerfectMatchings")
 #let nae_ppm_sol = nae_ppm.solutions.at(0)

src/rules/mod.rs

@@ -138,6 +138,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;
@@ -557,6 +558,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,89 @@
+//! Reduction from Set Splitting to NAE-Satisfiability.
+//!
+//! Create one Boolean variable for each universe element and one positive-literal
+//! NAE clause for each subset. Repeated members are removed in first-occurrence
+//! order. An all-repeated subset becomes `(x_u, x_u)`, which is unsatisfiable.
+
+use std::collections::HashSet;
+
+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 ReductionSetSplittingToNAESatisfiability {
+    target: NAESatisfiability,
+}
+
+impl ReductionResult for ReductionSetSplittingToNAESatisfiability {
+    type Source = SetSplitting;
+    type Target = NAESatisfiability;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+        target_solution.to_vec()
+    }
+}
+
+#[reduction(
+    overhead = {
+        num_vars = "universe_size",
+        num_clauses = "num_subsets",
+        num_literals = "(universe_size + 1) * num_subsets",
+    }
+)]
+impl ReduceTo<NAESatisfiability> for SetSplitting {
+    type Result = ReductionSetSplittingToNAESatisfiability;
+
+    fn reduce_to(&self) -> Self::Result {
+        let clauses = self
+            .subsets()
+            .iter()
+            .map(|subset| {
+                let mut seen = HashSet::new();
+                let mut literals: Vec<_> = subset
+                    .iter()
+                    .copied()
+                    .filter(|element| seen.insert(*element))
+                    .map(|element| (element + 1) as i32)
+                    .collect();
+
+                if literals.len() == 1 {
+                    literals.push(literals[0]);
+                }
+
+                CNFClause::new(literals)
+            })
+            .collect();
+
+        ReductionSetSplittingToNAESatisfiability {
+            target: NAESatisfiability::new(self.universe_size(), clauses),
+        }
+    }
+}
+
+#[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: vec![0, 1, 0, 1],
+                    target_config: vec![0, 1, 0, 1],
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/setsplitting_naesatisfiability.rs"]
+mod tests;

src/unit_tests/rules/analysis.rs

@@ -322,6 +322,8 @@ fn test_find_dominated_rules_returns_known_set() {
             "PartitionIntoPathsOfLength2 {graph: \"SimpleGraph\"}",
             "ILP {variable: \"bool\"}",
         ),
+        // SetSplitting → NAE-SAT → ILP is better than direct SetSplitting → ILP
+        ("SetSplitting", "ILP {variable: \"bool\"}"),
     ]
     .into_iter()
     .collect();

src/unit_tests/rules/setsplitting_naesatisfiability.rs

@@ -0,0 +1,143 @@
+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;
+
+fn issue_example() -> 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 = issue_example();
+    let reduction = ReduceTo::<NAESatisfiability>::reduce_to(&source);
+
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &reduction,
+        "SetSplitting -> NAE-SAT",
+    );
+    assert_eq!(reduction.extract_solution(&[0, 1, 0, 1]), vec![0, 1, 0, 1]);
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_five_element_closed_loop() {
+    let source = SetSplitting::new(5, vec![vec![0, 1], vec![1, 2, 3], vec![0, 2, 3, 4]]);
+    let reduction = ReduceTo::<NAESatisfiability>::reduce_to(&source);
+
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &reduction,
+        "five-element SetSplitting -> NAE-SAT",
+    );
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_odd_cycle_is_infeasible() {
+    let source = SetSplitting::new(3, vec![vec![0, 1], vec![1, 2], vec![0, 2]]);
+    let reduction = ReduceTo::<NAESatisfiability>::reduce_to(&source);
+    let solver = BruteForce::new();
+
+    assert!(solver.find_witness(&source).is_none());
+    assert!(solver.find_witness(reduction.target_problem()).is_none());
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_structure_and_overhead() {
+    let source = issue_example();
+    let reduction = ReduceTo::<NAESatisfiability>::reduce_to(&source);
+    let target = reduction.target_problem();
+
+    assert_eq!(target.num_vars(), 4);
+    assert_eq!(target.num_clauses(), 3);
+    assert_eq!(target.num_literals(), 8);
+    assert_eq!(
+        target
+            .clauses()
+            .iter()
+            .map(|clause| clause.literals.clone())
+            .collect::<Vec<_>>(),
+        vec![vec![1, 2], vec![2, 3, 4], vec![1, 3, 4]],
+    );
+
+    let entry = inventory::iter::<crate::rules::ReductionEntry>()
+        .find(|entry| {
+            entry.source_name == "SetSplitting" && entry.target_name == "NAESatisfiability"
+        })
+        .expect("SetSplitting -> NAESatisfiability reduction should be registered");
+    let overhead = (entry.overhead_eval_fn)(&source as &dyn std::any::Any);
+
+    assert_eq!(overhead.get("num_vars"), Some(target.num_vars()));
+    assert_eq!(overhead.get("num_clauses"), Some(target.num_clauses()));
+    assert_eq!(overhead.get("num_literals"), Some(15));
+    assert!(target.num_literals() <= overhead.get("num_literals").unwrap());
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_deduplicates_in_first_occurrence_order() {
+    let source = SetSplitting::new(4, vec![vec![2, 0, 2, 1, 0]]);
+    let reduction = ReduceTo::<NAESatisfiability>::reduce_to(&source);
+
+    assert_eq!(
+        reduction.target_problem().clauses()[0].literals,
+        vec![3, 1, 2]
+    );
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_all_repeated_subset_is_infeasible() {
+    let source = SetSplitting::new(1, vec![vec![0, 0]]);
+    let reduction = ReduceTo::<NAESatisfiability>::reduce_to(&source);
+
+    assert_eq!(reduction.target_problem().clauses()[0].literals, vec![1, 1]);
+    assert!(BruteForce::new().find_witness(&source).is_none());
+    assert!(BruteForce::new()
+        .find_witness(reduction.target_problem())
+        .is_none());
+}
+
+#[test]
+fn test_setsplitting_to_naesatisfiability_empty_family_and_unused_element() {
+    let empty_source = SetSplitting::new(3, vec![]);
+    let empty_reduction = ReduceTo::<NAESatisfiability>::reduce_to(&empty_source);
+    assert_eq!(empty_reduction.target_problem().num_vars(), 3);
+    assert!(empty_reduction.target_problem().clauses().is_empty());
+
+    let source = SetSplitting::new(5, vec![vec![0, 1], vec![0, 1, 2], vec![0, 1, 2, 3, 1]]);
+    let reduction = ReduceTo::<NAESatisfiability>::reduce_to(&source);
+    assert_eq!(reduction.target_problem().num_vars(), 5);
+    assert_eq!(
+        reduction
+            .target_problem()
+            .clauses()
+            .iter()
+            .map(|clause| clause.literals.clone())
+            .collect::<Vec<_>>(),
+        vec![vec![1, 2], vec![1, 2, 3], vec![1, 2, 3, 4]],
+    );
+}
+
+#[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.source.instance["universe_size"], 4);
+    assert_eq!(
+        example.target.instance["clauses"],
+        serde_json::json!([
+            { "literals": [1, 2] },
+            { "literals": [2, 3, 4] },
+            { "literals": [1, 3, 4] },
+        ]),
+    );
+
+    let pair = &example.solutions[0];
+    assert_eq!(pair.source_config, vec![0, 1, 0, 1]);
+    assert_eq!(pair.target_config, vec![0, 1, 0, 1]);
+}