Add NAESatisfiability → Satisfiability clause-doubling reduction (#1101)

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",

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<crate::example_db::specs::Ru
     specs.extend(rootedtreearrangement_rootedtreestorageassignment::canonical_rule_example_specs());
     specs.extend(naesatisfiability_maxcut::canonical_rule_example_specs());
     specs.extend(naesatisfiability_partitionintoperfectmatchings::canonical_rule_example_specs());
+    specs.extend(naesatisfiability_satisfiability::canonical_rule_example_specs());
     specs.extend(satisfiability_maximum2satisfiability::canonical_rule_example_specs());
     specs.extend(ensemblecomputation_ilp::canonical_rule_example_specs());
     specs.extend(exactcoverby3sets_maximumsetpacking::canonical_rule_example_specs());

src/rules/naesatisfiability_satisfiability.rs

@@ -0,0 +1,102 @@
+//! Reduction from NAE-Satisfiability to Satisfiability.
+//!
+//! A not-all-equal clause `(l_1, ..., l_r)` holds exactly when at least one
+//! literal is true and at least one literal is false. Each NAE clause therefore
+//! becomes two CNF clauses over the same variables: `(l_1 ∨ ... ∨ l_r)` excludes
+//! the all-false assignment and `(¬l_1 ∨ ... ∨ ¬l_r)` excludes the all-true one.
+
+use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability};
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+
+/// Result of reducing NAE-Satisfiability to Satisfiability.
+#[derive(Debug, Clone)]
+pub struct ReductionNAESATToSAT {
+    /// The target SAT problem.
+    target: Satisfiability,
+}
+
+impl ReductionResult for ReductionNAESATToSAT {
+    type Source = NAESatisfiability;
+    type Target = Satisfiability;
+
+    fn target_problem(&self) -> &Self::Target {
+        &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 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<Satisfiability> for NAESatisfiability {
+    type Result = ReductionNAESATToSAT;
+
+    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
+        let clauses: Vec<CNFClause> = 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::<NAESatisfiability, Satisfiability>,
+        )?;
+
+        Ok(ReductionNAESATToSAT { target })
+    }
+}
+
+#[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: "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;

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]

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::<Satisfiability>::reduce_to(source).expect("reduction should succeed")
+}
+
+fn assignments(num_vars: usize) -> impl Iterator<Item = Vec<bool>> {
+    (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<Vec<i64>> = 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<Vec<bool>> = 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<Vec<i64>> = 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",
+    );
+}