From 43fb5e0d629d6724b975ff07e8ac6e806d3a6e22 Mon Sep 17 00:00:00 2001 From: pasitnusso Date: Sun, 18 Oct 2026 22:23:03 +0700 Subject: [PATCH] feat(rules): add NAESatisfiability to Satisfiability reduction (#1101) --- docs/paper/reductions.typ | 10 + src/rules/mod.rs | 2 + src/rules/naesatisfiability_satisfiability.rs | 102 +++++++++ src/unit_tests/example_db.rs | 15 ++ .../rules/naesatisfiability_satisfiability.rs | 200 ++++++++++++++++++ 5 files changed, 329 insertions(+) create mode 100644 src/rules/naesatisfiability_satisfiability.rs create mode 100644 src/unit_tests/rules/naesatisfiability_satisfiability.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 44256b45b..6005324af 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -12983,6 +12983,16 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ If the sentinel $s = 0$, return the first $n$ variables. If $s = 1$, return the complement of the first $n$ variables. ] +#reduction-rule("NAESatisfiability", "Satisfiability")[ + A not-all-equal clause holds exactly when it has a true literal and a false literal @schaefer1978. Each NAE clause therefore becomes two CNF clauses over the same variables, one forbidding the all-false assignment and one forbidding the all-true assignment. +][ + _Construction._ Given an NAE-SAT instance with $n$ variables and $m$ clauses, keep the same $n$ variables. For each clause $C_j = (ell_1, dots, ell_r)$ with $r >= 2$, emit the CNF clauses $(ell_1 or dots or ell_r)$ and $(not ell_1 or dots or not ell_r)$. The target has $n$ variables, $2m$ clauses, and $2L$ literal occurrences, where $L$ is the number of source literal occurrences. Repeated and complementary literals are copied unchanged. + + _Correctness._ For any assignment, the first clause is false exactly when every $ell_i$ is false, and the second is false exactly when every $ell_i$ is true. Both hold exactly when $C_j$ contains a true and a false literal, which is the NAE condition. Hence an assignment satisfies the target iff it satisfies the source. + + _Solution extraction._ Return the target assignment unchanged. +] + #let cs_sat = load-example("CircuitSAT", "Satisfiability") #let cs_sat_sol = cs_sat.solutions.at(0) #reduction-rule("CircuitSAT", "Satisfiability", diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 3baa44186..c31c70e10 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -115,6 +115,7 @@ pub(crate) mod minimumvertexcover_minimumsetcovering; pub(crate) mod minimumvertexcover_minimumweightandorgraph; pub(crate) mod naesatisfiability_maxcut; pub(crate) mod naesatisfiability_partitionintoperfectmatchings; +pub(crate) mod naesatisfiability_satisfiability; pub(crate) mod naesatisfiability_setsplitting; pub(crate) mod numerical3dimensionalmatching_numericalmatchingwithtargetsums; pub(crate) mod optimallineararrangement_consecutiveonesmatrixaugmentation; @@ -411,6 +412,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec &Self::Target { + &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 assignment does not satisfy CNF clauses", + )?; + + Ok(target_solution.clone()) + } +} + +#[crate::aggregate_reduction(identity)] +impl crate::rules::AggregateReductionResult for ReductionNAESATToSAT {} + +#[reduction(transform = exact { + num_vars = "num_vars", + num_clauses = "2 * num_clauses", + num_literals = "2 * num_literals", +})] +impl ReduceTo for NAESatisfiability { + type Result = ReductionNAESATToSAT; + + fn reduce_to(&self) -> Result { + let clauses: Vec = self + .clauses() + .iter() + .flat_map(|clause| { + let negated = clause.literals.iter().map(|&lit| -lit).collect(); + [ + CNFClause::new(clause.literals.clone()), + CNFClause::new(negated), + ] + }) + .collect(); + + let target = Satisfiability::try_new(self.num_vars(), clauses).map_err( + crate::rules::ReductionError::construction::, + )?; + + Ok(ReductionNAESATToSAT { target }) + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "naesatisfiability_to_satisfiability", + build: || { + let source = NAESatisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, 2]), + CNFClause::new(vec![1, -2, -3]), + ], + ); + crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>( + source, + SolutionPair { + source_config: serde_json::json!(vec![false, false, true]), + target_config: serde_json::json!(vec![false, false, true]), + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/naesatisfiability_satisfiability.rs"] +mod tests; diff --git a/src/unit_tests/example_db.rs b/src/unit_tests/example_db.rs index 3bc887a26..71707cb36 100644 --- a/src/unit_tests/example_db.rs +++ b/src/unit_tests/example_db.rs @@ -938,6 +938,21 @@ fn test_find_rule_example_satisfiability_to_naesatisfiability() { assert_eq!(example.target.problem, "NAESatisfiability"); } +#[test] +fn test_find_rule_example_naesatisfiability_to_satisfiability() { + let source = ProblemRef { + name: "NAESatisfiability".to_string(), + variant: BTreeMap::new(), + }; + let target = ProblemRef { + name: "Satisfiability".to_string(), + variant: BTreeMap::new(), + }; + let example = find_rule_example(&source, &target).unwrap(); + assert_eq!(example.source.problem, "NAESatisfiability"); + assert_eq!(example.target.problem, "Satisfiability"); +} + // PR #779 rules #[test] diff --git a/src/unit_tests/rules/naesatisfiability_satisfiability.rs b/src/unit_tests/rules/naesatisfiability_satisfiability.rs new file mode 100644 index 000000000..0b8150584 --- /dev/null +++ b/src/unit_tests/rules/naesatisfiability_satisfiability.rs @@ -0,0 +1,200 @@ +use super::*; +use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target; +use crate::solvers::BruteForce; +use crate::traits::Problem; + +fn reduce(source: &NAESatisfiability) -> ReductionNAESATToSAT { + ReduceTo::::reduce_to(source).expect("reduction should succeed") +} + +fn assignments(num_vars: usize) -> impl Iterator> { + (0..1usize << num_vars).map(move |mask| (0..num_vars).map(|i| (mask >> i) & 1 == 1).collect()) +} + +/// Checks that source and target agree on every assignment, that satisfying +/// assignments extract unchanged, and that all others are rejected. +fn assert_equivalent_on_all_assignments(source: &NAESatisfiability) { + let reduction = reduce(source); + let target = reduction.target_problem(); + assert_eq!(target.num_vars(), source.num_vars()); + for assignment in assignments(source.num_vars()) { + let source_ok = source.evaluate(&assignment).unwrap().0; + assert_eq!( + source_ok, + target.evaluate(&assignment).unwrap().0, + "disagreement on {assignment:?}" + ); + match reduction.extract_solution(&assignment) { + Ok(extracted) => { + assert!(source_ok, "accepted non-witness {assignment:?}"); + assert_eq!(extracted, assignment); + } + Err(_) => assert!(!source_ok, "rejected witness {assignment:?}"), + } + } +} + +fn canonical_source() -> NAESatisfiability { + NAESatisfiability::new( + 3, + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, 2]), + CNFClause::new(vec![1, -2, -3]), + ], + ) +} + +#[test] +fn test_naesatisfiability_to_satisfiability_closed_loop() { + let source = canonical_source(); + let reduction = reduce(&source); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "NAE-SAT->SAT closed loop", + ); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_structure() { + let source = canonical_source(); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 3); + assert_eq!(target.num_clauses(), 2 * source.num_clauses()); + assert_eq!(target.num_literals(), 2 * source.num_literals()); + let literals: Vec> = target + .clauses() + .iter() + .map(|clause| clause.literals.clone()) + .collect(); + assert_eq!( + literals, + vec![ + vec![1, 2, 3], + vec![-1, -2, -3], + vec![-1, 2], + vec![1, -2], + vec![1, -2, -3], + vec![-1, 2, 3], + ] + ); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_canonical_all_assignments() { + let source = canonical_source(); + assert_equivalent_on_all_assignments(&source); + + let witnesses: Vec> = assignments(3) + .filter(|assignment| source.evaluate(assignment).unwrap().0) + .collect(); + assert_eq!( + witnesses, + vec![vec![true, true, false], vec![false, false, true]] + ); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_witness_and_near_witness() { + let reduction = reduce(&canonical_source()); + + assert_eq!( + reduction.extract_solution(&vec![false, false, true]).unwrap(), + vec![false, false, true] + ); + // [0,1,0] makes (¬x1, x2) all true, so the excluded all-true CNF clause fails. + let error = reduction + .extract_solution(&vec![false, true, false]) + .unwrap_err(); + assert!(error + .to_string() + .contains("target assignment does not satisfy CNF clauses")); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_rejects_malformed_assignment() { + let reduction = reduce(&canonical_source()); + assert!(reduction.extract_solution(&vec![false, false]).is_err()); + assert!(reduction + .extract_solution(&vec![false, false, true, false]) + .is_err()); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_empty_conjunction() { + for num_vars in [0, 2] { + let source = NAESatisfiability::new(num_vars, vec![]); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!(target.num_vars(), num_vars); + assert_eq!(target.num_clauses(), 0); + assert_eq!(target.num_literals(), 0); + assert_equivalent_on_all_assignments(&source); + } +} + +#[test] +fn test_naesatisfiability_to_satisfiability_unsatisfiable_repeated_variable() { + let source = NAESatisfiability::new(1, vec![CNFClause::new(vec![1, 1])]); + let reduction = reduce(&source); + let literals: Vec> = reduction + .target_problem() + .clauses() + .iter() + .map(|clause| clause.literals.clone()) + .collect(); + assert_eq!(literals, vec![vec![1, 1], vec![-1, -1]]); + + let solver = BruteForce::new(); + assert!(solver.solve(&source).unwrap().is_none()); + assert!(solver.solve(reduction.target_problem()).unwrap().is_none()); + assert_equivalent_on_all_assignments(&source); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_repeated_literals() { + // NAE(x1, x1, x2) holds exactly when x1 != x2. + let source = NAESatisfiability::new(2, vec![CNFClause::new(vec![1, 1, 2])]); + assert_equivalent_on_all_assignments(&source); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_tautological_clauses() { + // (x1, ¬x1) always has one true and one false literal. + let source = NAESatisfiability::new( + 2, + vec![CNFClause::new(vec![1, -1]), CNFClause::new(vec![2, -2, 1])], + ); + let reduction = reduce(&source); + assert_eq!( + reduction.target_problem().clauses()[1].literals, + vec![-1, 1] + ); + assert_equivalent_on_all_assignments(&source); +} + +#[test] +fn test_naesatisfiability_to_satisfiability_arbitrary_clause_lengths() { + let source = NAESatisfiability::new( + 5, + vec![ + CNFClause::new(vec![1, -2]), + CNFClause::new(vec![2, 3, -4]), + CNFClause::new(vec![-1, 3, 4, 5]), + CNFClause::new(vec![1, 2, -3, -4, 5]), + ], + ); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!(target.num_clauses(), 8); + assert_eq!(target.num_literals(), 2 * 14); + assert_equivalent_on_all_assignments(&source); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "NAE-SAT->SAT mixed clause lengths", + ); +}