Fix #1101: NAESatisfiability to Satisfiability

docs/paper/reductions.typ

@@ -13066,6 +13066,59 @@ 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.
 ]
 
+#let nae_sat = load-example("NAESatisfiability", "Satisfiability")
+#let nae_sat_sol = nae_sat.solutions.at(0)
+#reduction-rule("NAESatisfiability", "Satisfiability",
+  example: true,
+  example-caption: [$n = #nae_sat.source.instance.num_vars$ variables, $m = #sat-num-clauses(nae_sat.source.instance)$ NAE clauses, and $#sat-num-clauses(nae_sat.target.instance)$ SAT clauses],
+  extra: [
+    #pred-commands(
+      "pred create --example " + problem-spec(nae_sat.source) + " -o naesat.json",
+      "pred reduce naesat.json --to " + target-spec(nae_sat) + " -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate naesat.json --config " + nae_sat_sol.source_config.map(str).join(","),
+    )
+
+    #{
+      let fmt-lit(l) = if l > 0 { $x_#l$ } else { $overline(x)_#calc.abs(l)$ }
+      let fmt-clause(c) = $paren.l #c.literals.map(fmt-lit).join($or$) paren.r$
+      let lit-value(l, config) = if l > 0 { config.at(l - 1) } else { 1 - config.at(-l - 1) }
+      let truth-pattern(c, config) = c.literals.map(l => lit-value(l, config))
+      let clause-value(c, config) = if truth-pattern(c, config).any(v => v == 1) { 1 } else { 0 }
+      [
+        *Step 1 -- Read the NAE instance.* The fixture has $#nae_sat.source.instance.num_vars$ variables and $#sat-num-clauses(nae_sat.source.instance)$ clauses:
+        $#nae_sat.source.instance.clauses.enumerate().map(((j, c)) => $C_#(j + 1) = #fmt-clause(c)$).join($comma quad$)$.
+
+        *Step 2 -- Double the clauses.* For each $C_j$, emit $C_j$ followed by its literalwise complement $overline(C_j)$. The target therefore retains $#nae_sat.target.instance.num_vars$ variables and contains $#sat-num-clauses(nae_sat.target.instance)$ clauses:
+        $#nae_sat.target.instance.clauses.enumerate().map(((j, c)) => $D_#(j + 1) = #fmt-clause(c)$).join($comma quad$)$.
+        The source has $#nae_sat.source.instance.clauses.map(c => c.literals.len()).sum()$ literal occurrences, while the target has $#nae_sat.target.instance.clauses.map(c => c.literals.len()).sum()$.
+
+        *Step 3 -- Verify the canonical witness.* For $(#range(nae_sat.source.instance.num_vars).map(i => $x_#(i + 1)$).join(", ")) = (#nae_sat_sol.source_config.map(str).join(", "))$, the source clauses have literal-value patterns
+        $#nae_sat.source.instance.clauses.enumerate().map(((j, c)) => $C_#(j + 1): #truth-pattern(c, nae_sat_sol.source_config).map(str).join(",")$).join([; ])$.
+        Every pattern contains both $0$ and $1$, so every NAE clause is satisfied. Under the identical target configuration $(#nae_sat_sol.target_config.map(str).join(", "))$, the target clauses evaluate to $(#nae_sat.target.instance.clauses.map(c => str(clause-value(c, nae_sat_sol.target_config))).join(", "))$ #sym.checkmark.
+
+        *Step 4 -- Extract the source witness.* Identity extraction returns $(#nae_sat_sol.target_config.map(str).join(", "))$, exactly the stored source configuration $(#nae_sat_sol.source_config.map(str).join(", "))$.
+
+        *Multiplicity:* The fixture stores one canonical witness. Since the reduction introduces no variables and preserves every assignment pointwise, each NAE witness corresponds to exactly one SAT witness and conversely; this conclusion follows from the construction, not from the number of stored fixture solutions.
+      ]
+    }
+  ],
+)[
+  Let $L = sum_(j=1)^m |C_j|$ be the number of literal occurrences. This $O(L)$ negation-closure construction @Gurumukhani2025, also implicit in the classical ternary NAE relation @schaefer1978, keeps all $n$ variables and replaces every NAE clause $C_j$ by two SAT clauses, $C_j$ and its literalwise complement $overline(C_j)$. The target has $n$ variables, $2m$ clauses, and $2L$ literal occurrences.
+][
+  _Construction._ Let $Phi = and.big_(j=1)^m "NAE"(C_j)$ be an NAE-CNF formula on variables $x_1, dots, x_n$, where $C_j = (ell_(j,1), dots, ell_(j,r_j))$ and each $ell_(j,k)$ is a literal. For a literal $ell$, let $overline(ell)$ denote its Boolean complement, and define $overline(C_j) = (overline(ell_(j,1)) or dots or overline(ell_(j,r_j)))$. Construct the ordinary CNF formula
+  $
+    Psi = and.big_(j=1)^m (C_j and overline(C_j)),
+  $
+  interpreting $C_j$ itself as the disjunction $(ell_(j,1) or dots or ell_(j,r_j))$. No variables are added or reordered. The construction copies and complements each literal once, so it takes $O(L)$ time. When $m = 0$, both source and target are the empty conjunction.
+
+  _Correctness._ ($arrow.r.double$) Suppose an assignment satisfies $Phi$. In each $C_j$, the NAE condition supplies a true literal $ell_(j,p)$ and a false literal $ell_(j,q)$. The true literal satisfies the target clause $C_j$, while $overline(ell_(j,q))$ is true and satisfies $overline(C_j)$. Hence every pair $C_j and overline(C_j)$ is satisfied, so the assignment satisfies $Psi$.
+
+  ($arrow.l.double$) Conversely, suppose an assignment satisfies $Psi$. For every $j$, satisfaction of $C_j$ supplies at least one true source literal. Satisfaction of $overline(C_j)$ supplies a true complemented literal $overline(ell_(j,q))$, so the corresponding source literal $ell_(j,q)$ is false. Thus $C_j$ contains both truth values and satisfies NAE. Therefore the same assignment satisfies $Phi$.
+
+  _Solution extraction._ Return the target Boolean configuration unchanged. Because the target uses exactly the source variables in the same order, this identity map is valid for every satisfying assignment, including the unique empty configuration when $n = 0$.
+]
+
 #let cs_sat = load-example("CircuitSAT", "Satisfiability")
 #let cs_sat_sol = cs_sat.solutions.at(0)
 #reduction-rule("CircuitSAT", "Satisfiability",

docs/paper/references.bib

@@ -1580,6 +1580,17 @@ @book{papadimitriou-steiglitz1982
   year      = {1982}
 }
 
+@inproceedings{Gurumukhani2025,
+  author    = {Mohit Gurumukhani and Ramamohan Paturi and Michael Saks and Navid Talebanfard},
+  title     = {Local Enumeration: The Not-All-Equal Case},
+  booktitle = {42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
+  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
+  volume    = {327},
+  pages     = {42:1--42:19},
+  year      = {2025},
+  doi       = {10.4230/LIPIcs.STACS.2025.42}
+}
+
 @article{schaefer1978,
   author  = {Thomas J. Schaefer},
   title   = {The Complexity of Satisfiability Problems},
@@ -2142,4 +2153,3 @@ @article{berlekampMcElieceTilborg1978
   year    = {1978},
   doi     = {10.1109/TIT.1978.1055873}
 }
-

src/rules/mod.rs

@@ -109,6 +109,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;
@@ -517,6 +518,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(exactcoverby3sets_maximumsetpacking::canonical_rule_example_specs());
     specs.extend(maxcut_minimumcutintoboundedsets::canonical_rule_example_specs());

src/rules/naesatisfiability_satisfiability.rs

@@ -0,0 +1,84 @@
+//! Reduction from Not-All-Equal Satisfiability to Satisfiability.
+
+use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability};
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+
+/// Result of reducing NAE-SAT to SAT.
+#[derive(Debug, Clone)]
+pub struct ReductionNAESATToSAT {
+    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: &[usize]) -> Vec<usize> {
+        target_solution.to_vec()
+    }
+}
+
+#[reduction(overhead = {
+    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) -> Self::Result {
+        let clauses = self
+            .clauses()
+            .iter()
+            .flat_map(|clause| {
+                [
+                    clause.clone(),
+                    CNFClause::new(clause.literals.iter().map(|literal| -literal).collect()),
+                ]
+            })
+            .collect();
+
+        ReductionNAESATToSAT {
+            target: Satisfiability::new(self.num_vars(), clauses),
+        }
+    }
+}
+
+#[cfg(any(test, feature = "example-db"))]
+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]),
+        ],
+    )
+}
+
+#[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: || {
+            crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
+                canonical_source(),
+                SolutionPair {
+                    source_config: vec![0, 0, 1],
+                    target_config: vec![0, 0, 1],
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/naesatisfiability_satisfiability.rs"]
+mod tests;

src/unit_tests/rules/naesatisfiability_satisfiability.rs

@@ -0,0 +1,133 @@
+#[cfg(feature = "example-db")]
+use super::canonical_rule_example_specs;
+use super::*;
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_satisfaction_target;
+use crate::rules::{ReduceTo, ReductionGraph, ReductionResult};
+use crate::solvers::BruteForce;
+use crate::traits::Problem;
+
+#[test]
+fn test_naesatisfiability_to_satisfiability_closed_loop() {
+    let source = canonical_source();
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+
+    assert_satisfaction_round_trip_from_satisfaction_target(
+        &source,
+        &reduction,
+        "NAESatisfiability -> Satisfiability closed loop",
+    );
+    assert_eq!(reduction.extract_solution(&[0, 0, 1]), vec![0, 0, 1]);
+    assert!(source.evaluate(&[0, 0, 1]).0);
+    assert!(reduction.target_problem().evaluate(&[0, 0, 1]).0);
+}
+
+#[test]
+fn test_naesatisfiability_to_satisfiability_repeated_literal_infeasible() {
+    let source = NAESatisfiability::new(1, vec![CNFClause::new(vec![1, 1])]);
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+
+    assert_eq!(BruteForce::new().find_witness(&source), None);
+    assert_eq!(
+        BruteForce::new().find_witness(reduction.target_problem()),
+        None
+    );
+}
+
+#[test]
+fn test_naesatisfiability_to_satisfiability_structure_and_overhead() {
+    let source = NAESatisfiability::new(
+        4,
+        vec![
+            CNFClause::new(vec![1, -2]),
+            CNFClause::new(vec![2, 3, -4, 1]),
+            CNFClause::new(vec![-1, -1, 4]),
+        ],
+    );
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+    let target = reduction.target_problem();
+
+    assert_eq!(target.num_vars(), source.num_vars());
+    assert_eq!(target.num_clauses(), 2 * source.num_clauses());
+    assert_eq!(target.num_literals(), 2 * source.num_literals());
+    assert_eq!(
+        target.clauses(),
+        &[
+            CNFClause::new(vec![1, -2]),
+            CNFClause::new(vec![-1, 2]),
+            CNFClause::new(vec![2, 3, -4, 1]),
+            CNFClause::new(vec![-2, -3, 4, -1]),
+            CNFClause::new(vec![-1, -1, 4]),
+            CNFClause::new(vec![1, 1, -4]),
+        ]
+    );
+
+    let entry = inventory::iter::<crate::rules::ReductionEntry>()
+        .find(|entry| {
+            entry.source_name == "NAESatisfiability" && entry.target_name == "Satisfiability"
+        })
+        .expect("NAESatisfiability -> Satisfiability reduction should be registered");
+    let overhead = (entry.overhead_eval_fn)(&source as &dyn std::any::Any);
+    assert_eq!(overhead.get("num_vars"), Some(target.num_vars()));
+    assert_eq!(overhead.get("num_clauses"), Some(target.num_clauses()));
+    assert_eq!(overhead.get("num_literals"), Some(target.num_literals()));
+}
+
+#[test]
+fn test_naesatisfiability_to_satisfiability_edge_case_semantics() {
+    let formulas = [
+        NAESatisfiability::new(0, vec![]),
+        NAESatisfiability::new(5, vec![CNFClause::new(vec![1, 2, -3, 4, -5])]),
+        NAESatisfiability::new(2, vec![CNFClause::new(vec![1, 1, -2])]),
+        NAESatisfiability::new(2, vec![CNFClause::new(vec![1, -1, 2])]),
+    ];
+
+    for source in formulas {
+        let reduction = ReduceTo::<Satisfiability>::reduce_to(&source);
+        for mask in 0..(1usize << source.num_vars()) {
+            let config = (0..source.num_vars())
+                .map(|bit| (mask >> bit) & 1)
+                .collect::<Vec<_>>();
+            assert_eq!(
+                source.evaluate(&config),
+                reduction.target_problem().evaluate(&config),
+                "evaluation differs for config {config:?}",
+            );
+            assert_eq!(reduction.extract_solution(&config), config);
+        }
+    }
+}
+
+#[test]
+fn test_reduction_graph_registers_naesatisfiability_to_satisfiability() {
+    assert!(
+        ReductionGraph::new().has_direct_reduction_by_name("NAESatisfiability", "Satisfiability")
+    );
+}
+
+#[cfg(feature = "example-db")]
+#[test]
+fn test_naesatisfiability_to_satisfiability_canonical_example_spec() {
+    let example = (canonical_rule_example_specs()
+        .into_iter()
+        .find(|spec| spec.id == "naesatisfiability_to_satisfiability")
+        .expect("missing canonical NAESatisfiability -> Satisfiability example spec")
+        .build)();
+
+    assert_eq!(example.source.problem, "NAESatisfiability");
+    assert_eq!(example.target.problem, "Satisfiability");
+    assert_eq!(example.source.instance["num_vars"], serde_json::json!(3));
+    assert_eq!(
+        example.target.instance["clauses"].as_array().unwrap().len(),
+        6
+    );
+    assert_eq!(example.solutions.len(), 1);
+    assert_eq!(example.solutions[0].source_config, vec![0, 0, 1]);
+    assert_eq!(example.solutions[0].target_config, vec![0, 0, 1]);
+
+    let source: NAESatisfiability = serde_json::from_value(example.source.instance.clone())
+        .expect("source example deserializes");
+    let target: Satisfiability = serde_json::from_value(example.target.instance.clone())
+        .expect("target example deserializes");
+    assert!(source.evaluate(&example.solutions[0].source_config).0);
+    assert!(target.evaluate(&example.solutions[0].target_config).0);
+}