From 309c562e4f3fe964d47e18fa43dba1086d062369 Mon Sep 17 00:00:00 2001 From: Pedro Monteiro <83892026+peda-cos@users.noreply.github.com> Date: Mon, 12 Oct 2026 13:36:31 -0300 Subject: [PATCH 1/2] feat: SetSplitting to NAE-SAT clause-per-subset reduction (#1100) Fixes #1100 --- src/rules/mod.rs | 2 + src/rules/setsplitting_naesatisfiability.rs | 120 ++++++++++++++++++ .../rules/setsplitting_naesatisfiability.rs | 104 +++++++++++++++ 3 files changed, 226 insertions(+) create mode 100644 src/rules/setsplitting_naesatisfiability.rs create mode 100644 src/unit_tests/rules/setsplitting_naesatisfiability.rs diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 3baa44186..d224900c7 100644 --- a/src/rules/mod.rs +++ b/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 &NAESatisfiability { + &self.target + } + + fn extract_solution( + &self, + target_solution: &::Solution, + ) -> crate::rules::ExtractionResult<::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 for SetSplitting { + type Result = ReductionSetSplittingToNAESAT; + + fn reduce_to(&self) -> Result { + let universe_size = self.universe_size(); + let mut clauses = Vec::with_capacity(self.num_subsets()); + + for subset in self.subsets() { + let mut distinct: Vec = Vec::new(); + for &element in subset { + if element >= universe_size { + return Err(>::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(>::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 { + 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; diff --git a/src/unit_tests/rules/setsplitting_naesatisfiability.rs b/src/unit_tests/rules/setsplitting_naesatisfiability.rs new file mode 100644 index 000000000..97cccc23d --- /dev/null +++ b/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::::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::::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![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::::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::::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::::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]) + ); +} From 40a445d6162f25995042bd50365f31ff55a92464 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Thu, 29 Oct 2026 12:17:38 +0800 Subject: [PATCH 2/2] Fix SetSplitting NAE bounds and checked construction --- docs/paper/reductions.typ | 59 ++++++++++ src/rules/setsplitting_naesatisfiability.rs | 36 +++---- .../rules/setsplitting_naesatisfiability.rs | 102 ++++++++++++++++++ 3 files changed, 176 insertions(+), 21 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 413ed4790..bd827a828 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -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. ][ diff --git a/src/rules/setsplitting_naesatisfiability.rs b/src/rules/setsplitting_naesatisfiability.rs index 20606f8d6..2feb08050 100644 --- a/src/rules/setsplitting_naesatisfiability.rs +++ b/src/rules/setsplitting_naesatisfiability.rs @@ -48,7 +48,7 @@ impl crate::rules::AggregateReductionResult for ReductionSetSplittingToNAESAT {} num_clauses = "num_subsets", }, upper_bound { - num_clause_variables = "universe_size * (universe_size + 1)", + 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)", }, @@ -58,38 +58,32 @@ impl ReduceTo for SetSplitting { fn reduce_to(&self) -> Result { let universe_size = self.universe_size(); + crate::rules::sat_helpers::SatVariableAllocator::new( + "SetSplitting -> NAESatisfiability", + universe_size, + ) + .map_err(>::target_construction)?; let mut clauses = Vec::with_capacity(self.num_subsets()); for subset in self.subsets() { let mut distinct: Vec = Vec::new(); for &element in subset { - if element >= universe_size { - return Err(>::target_construction( - format!( - "subset element {element} is outside universe of size {universe_size}" - ) - .into(), - )); - } - let literal = (element + 1) as i64; + // 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); } } - match distinct.len() { - 1 => distinct.push(distinct[0]), - 0 => { - return Err(>::target_construction( - crate::registry::ConstructionError::from( - "empty subset cannot be split".to_string(), - ), - )) - } - _ => {} + // 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::new(universe_size, clauses); + let target = NAESatisfiability::try_new(universe_size, clauses) + .map_err(>::target_construction)?; Ok(ReductionSetSplittingToNAESAT { target, source_universe_size: universe_size, diff --git a/src/unit_tests/rules/setsplitting_naesatisfiability.rs b/src/unit_tests/rules/setsplitting_naesatisfiability.rs index 97cccc23d..1a3fbfd68 100644 --- a/src/unit_tests/rules/setsplitting_naesatisfiability.rs +++ b/src/unit_tests/rules/setsplitting_naesatisfiability.rs @@ -81,6 +81,108 @@ fn test_setsplitting_to_naesatisfiability_target_witness_extracts_to_satisfying_ assert!(source.evaluate(&source_solution).unwrap()); } +#[test] +fn test_setsplitting_to_naesatisfiability_rejects_invalid_witnesses() { + let reduction = ReduceTo::::reduce_to(&rule_example_problem()).unwrap(); + for witness in [vec![], vec![true; 3], vec![true; 5], vec![false; 4]] { + assert!(reduction.extract_solution(&witness).is_err()); + } +} + +#[test] +fn test_setsplitting_to_naesatisfiability_all_small_assignments() { + // Every pair of nonempty subsets on up to four elements, with zero + // standing for an omitted subset. Duplicate occurrences exercise the + // set semantics, including subsets with only one distinct member. + for n in 0..=4 { + for first in 0..(1 << n) { + for second in 0..(1 << n) { + let subsets = [first, second] + .into_iter() + .filter(|&mask| mask != 0) + .map(|mask| { + let mut subset: Vec<_> = (0..n).filter(|&i| mask & (1 << i) != 0).collect(); + subset.push(subset[0]); + subset + }) + .collect(); + let source = SetSplitting::new(n, subsets); + let reduction = ReduceTo::::reduce_to(&source).unwrap(); + for mask in 0..(1 << n) { + let witness: Vec<_> = (0..n).map(|i| mask & (1 << i) != 0).collect(); + let feasible = source.evaluate(&witness).unwrap().0; + assert_eq!( + reduction.target_problem().evaluate(&witness).unwrap().0, + feasible, + "n={n}, subsets={:?}, witness={witness:?}", + source.subsets() + ); + if feasible { + assert_eq!(reduction.extract_solution(&witness).unwrap(), witness); + } else { + assert!(reduction.extract_solution(&witness).is_err()); + } + } + } + } + } +} + +#[test] +fn test_setsplitting_to_naesatisfiability_parameter_bounds() { + use crate::parameters::ParameterRelation; + + let entries = crate::rules::registry::reduction_entries(); + let entry = entries + .iter() + .find(|e| e.source_name == "SetSplitting" && e.target_name == "NAESatisfiability") + .unwrap(); + let contract = entry.parameter_contract().unwrap(); + let transform = contract.transform().unwrap(); + for source in [ + SetSplitting::new(0, vec![]), + SetSplitting::new(4, vec![]), + SetSplitting::new(1, vec![vec![0, 0, 0]; 4]), + SetSplitting::new(2, vec![vec![0, 1]; 4]), + SetSplitting::new(5, vec![vec![3, 1, 0, 2, 3, 1]]), + ] { + let reduction = ReduceTo::::reduce_to(&source).unwrap(); + let actual = reduction.target_problem().parameters(); + let predicted = transform.evaluate(&source.parameters()).unwrap(); + for (field, _) in transform.expressions() { + let measured = actual.get(field).unwrap(); + let bound = predicted.get(field).unwrap(); + match transform.relation(field).unwrap() { + ParameterRelation::Exact => assert_eq!(measured, bound, "{field}"), + ParameterRelation::UpperBound => assert!(measured <= bound, "{field}"), + } + } + } +} + +#[cfg(target_pointer_width = "64")] +#[test] +fn test_setsplitting_to_naesatisfiability_literal_domain_boundary() { + let largest = usize::try_from(i64::MAX).unwrap(); + // Empty families exercise the universe limit without huge allocations. + let source = SetSplitting::new(largest, vec![]); + let reduction = ReduceTo::::reduce_to(&source).unwrap(); + assert_eq!(reduction.target_problem().num_vars(), largest); + for n in [largest + 1, usize::MAX] { + let source = SetSplitting::new(n, vec![]); + assert!(matches!( + ReduceTo::::reduce_to(&source), + Err(crate::rules::ReductionError::Construction { .. }) + )); + } + let source = SetSplitting::new(largest, vec![vec![largest - 1, largest - 1]]); + let reduction = ReduceTo::::reduce_to(&source).unwrap(); + assert_eq!( + reduction.target_problem().clauses()[0].literals, + [i64::MAX; 2] + ); +} + #[cfg(feature = "example-db")] #[test] fn test_setsplitting_to_naesatisfiability_canonical_example_spec() {