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] 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]) + ); +}