@@ -14486,6 +14486,65 @@ The following reductions to Integer Linear Programming are straightforward formu
   _Solution extraction._ Direct: $x_i = 1$ iff variable $i$ is true.
 ]
 
+#let ss_nae = load-example("SetSplitting", "NAESatisfiability")
+#let ss_nae_sol = ss_nae.solutions.at(0)
+#reduction-rule("SetSplitting", "NAESatisfiability",
+  example: true,
+  example-caption: [One NAE clause per subset],
+  extra: [
+    #pred-commands(
+      "pred create --example " + rule-spec(ss_nae) + " -o set-splitting.json",
+      "pred reduce set-splitting.json --via route.json -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate set-splitting.json --config " + cli-config(ss_nae_sol.source_config),
+    )
+
+    The canonical source has $#ss_nae.source.instance.universe_size$ elements and
+    subsets #{ss_nae.source.instance.subsets.map(s => [${#s.map(str).join(", ")}$]).join(", ")}.
+    It produces $#ss_nae.target.instance.num_vars$ Boolean variables and
+    $#ss_nae.target.instance.clauses.len()$ NAE clauses.
+    Under the stored target witness $(#fmt-values(ss_nae_sol.target_config))$,
+    the subsets have truth values
+    #{ss_nae.source.instance.subsets.map(s => [$(#fmt-values(s.map(u => ss_nae_sol.target_config.at(u))))$]).join(", ")}.
+    Each contains both values, so the same vector
+    $(#fmt-values(ss_nae_sol.source_config))$ is a valid splitting.
+  ],
+)[
+  Encode each universe element by a Boolean variable and each subset by its
+  not-all-equal constraint @schaefer1978. The target has exactly $n$ variables
+  and $m$ clauses for a source universe of size $n$ with $m$ subset vectors.
+][
+  _Construction._ For $U = {0, dots, n-1}$, introduce $x_u$ for each $u in U$.
+  In each subset vector, retain the first occurrence of each distinct element.
+  If the resulting list is $(u_1, dots, u_k)$ with $k >= 2$, emit the NAE clause
+  $(x_(u_1), dots, x_(u_k))$. If only one distinct element $u$ remains, emit
+  $(x_u, x_u)$. Source construction excludes empty subset vectors; an empty
+  family of subsets produces an empty formula. Unused elements retain their
+  variables. Positive literal $x_u$ is represented by the signed integer $u+1$;
+  universes outside the target literal domain return a construction error.
+
+  _Correctness._ ($arrow.r.double$) In a valid splitting, every subset contains
+  both colors. Removing repeated occurrences preserves these colors, so assigning
+  each $x_u$ its element's color satisfies every emitted NAE clause.
+  ($arrow.l.double$) In any satisfying target assignment, every clause has both
+  truth values. Giving each element its variable's value therefore splits every
+  source subset. A subset containing only one distinct element is unsplittable;
+  its repeated-literal clause is unsatisfiable, preserving the equivalence.
+
+  _Parameter bounds._ Each clause uses at most $n$ distinct variables, so the
+  sum of clause-variable counts is at most $n m$. A clause has at most $2n$
+  literal occurrences, including the repeated-literal case. Thus the total
+  literal count $L$ is at most $2 n m$, and the sum of within-clause literal-pair
+  counts is at most $L(L-1)/2 <= 2 n m (2 n m + 1)$. For an empty universe, the
+  accepted family is empty and all these counts are zero. Deduplication by
+  scanning previously retained elements takes polynomial time in the source
+  representation length.
+
+  _Solution extraction._ Validate the target witness and return it unchanged.
+  The assignment to every original element is preserved, with no auxiliary
+  variables to discard.
+]
+
 #reduction-rule("SetSplitting", "ILP")[
   Each subset must contain at least one element of each color, encoded as a pair of linear inequalities per subset.
 ][
 
@@ -166,6 +166,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;
@@ -471,6 +472,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());
 
@@ -0,0 +1,114 @@
+//! 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 * num_subsets",
+        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();
+        crate::rules::sat_helpers::SatVariableAllocator::new(
+            "SetSplitting -> NAESatisfiability",
+            universe_size,
+        )
+        .map_err(<Self as ReduceTo<NAESatisfiability>>::target_construction)?;
+        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 {
+                // SetSplitting validates element < universe_size; the allocator
+                // above checks that every resulting SAT variable fits i64.
+                let literal = i64::try_from(element + 1).expect("validated SAT variable");
+                if !distinct.contains(&literal) {
+                    distinct.push(literal);
+                }
+            }
+            // Source construction rejects empty subsets, but permits repeated
+            // occurrences of a single element. Such a subset is unsplittable.
+            if distinct.len() == 1 {
+                distinct.push(distinct[0]);
+            }
+            clauses.push(CNFClause::new(distinct));
+        }
+        let target = NAESatisfiability::try_new(universe_size, clauses)
+            .map_err(<Self as ReduceTo<NAESatisfiability>>::target_construction)?;
+        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;