feat: add 1 Tier 1a/1b corrected reduction rules (#770)

docs/paper/reductions.typ

@@ -8250,6 +8250,18 @@ The following reductions to Integer Linear Programming are straightforward formu
   _Solution extraction._ Direct: $x_i = 1$ iff variable $i$ is true.
 ]
 
+#reduction-rule("NAESatisfiability", "MaxCut",
+  example: false,
+)[
+  @gareyJohnsonStockmeyer1976 This $O(n + m)$ reduction constructs a weighted graph with $2n$ vertices and at most $n + 3m$ edges. Variable gadgets force complementary literal vertices to opposite sides; clause triangles contribute exactly 2 cut edges per NAE-satisfied clause.
+][
+  _Construction._ Given a NAE-3-SAT instance with $n$ variables and $m$ clauses, let $M = 2m + 1$. For each variable $x_i$, create two vertices $v_i$ (positive literal) and $v_i'$ (negative literal) connected by an edge of weight $M$. For each clause $C_j = (ell_a, ell_b, ell_c)$, add a triangle of weight-1 edges between the three literal vertices. If a clause edge coincides with a variable-gadget edge (when a clause contains both $x_i$ and $not x_i$), merge by summing weights.
+
+  _Correctness._ ($arrow.r.double$) If the instance is NAE-satisfiable, the assignment partitions literal vertices so that $v_i$ and $v_i'$ are on opposite sides (cutting all variable edges for $n M$). Each NAE-satisfied clause has a 1:2 or 2:1 split across the triangle, contributing exactly 2 edges. Total cut $= n M + 2m$. ($arrow.l.double$) Since $M > 2m$, any optimal partition must cut every variable edge (otherwise the loss of $M$ exceeds the maximum clause gain of $2m$). With all variable edges cut, each clause triangle contributes 0 (all-same side, violating NAE) or 2 (NAE-satisfied). If the instance is unsatisfiable, at least one clause contributes 0, so the cut $<= n M + 2(m-1) < n M + 2m$.
+
+  _Solution extraction._ For each variable $x_i$, set $x_i = 1$ if $v_i$ is in partition side 1, else $x_i = 0$.
+]
+
 #reduction-rule("KClique", "ILP")[
   A $k$-clique requires at least $k$ selected vertices with no non-edge between any pair.
 ][

src/rules/mod.rs

@@ -49,6 +49,7 @@ pub(crate) mod minimumvertexcover_maximumindependentset;
 pub(crate) mod minimumvertexcover_minimumfeedbackarcset;
 pub(crate) mod minimumvertexcover_minimumfeedbackvertexset;
 pub(crate) mod minimumvertexcover_minimumsetcovering;
+pub(crate) mod naesatisfiability_maxcut;
 pub(crate) mod partition_cosineproductintegration;
 pub(crate) mod partition_knapsack;
 pub(crate) mod partition_multiprocessorscheduling;
@@ -293,6 +294,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(minimumvertexcover_minimumfeedbackarcset::canonical_rule_example_specs());
     specs.extend(minimumvertexcover_minimumfeedbackvertexset::canonical_rule_example_specs());
     specs.extend(minimumvertexcover_minimumsetcovering::canonical_rule_example_specs());
+    specs.extend(naesatisfiability_maxcut::canonical_rule_example_specs());
     specs.extend(satisfiability_naesatisfiability::canonical_rule_example_specs());
     specs.extend(sat_circuitsat::canonical_rule_example_specs());
     specs.extend(sat_coloring::canonical_rule_example_specs());

src/rules/naesatisfiability_maxcut.rs

@@ -0,0 +1,144 @@
+//! Reduction from NAESatisfiability to MaxCut.
+//!
+//! Given a NAE-3-SAT instance with n variables and m clauses (each with exactly
+//! 3 literals), we construct a weighted MaxCut instance. Variable gadgets
+//! (complementary vertex pairs with high-weight edges) force optimal solutions
+//! to encode truth assignments. Clause gadgets (triangles on literal vertices)
+//! ensure that NAE-satisfied clauses contribute exactly 2 edges to the cut.
+//!
+//! Reference: Garey, Johnson & Stockmeyer, "Some simplified NP-complete graph
+//! problems," Theoretical Computer Science 1(3), 237–267 (1976).
+
+use crate::models::formula::NAESatisfiability;
+use crate::models::graph::MaxCut;
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+use crate::topology::SimpleGraph;
+use std::collections::BTreeMap;
+
+/// Result of reducing NAESatisfiability to MaxCut.
+#[derive(Debug, Clone)]
+pub struct ReductionNAESATToMaxCut {
+    target: MaxCut<SimpleGraph, i32>,
+    /// Number of variables in the source NAE-SAT instance.
+    num_vars: usize,
+}
+
+impl ReductionResult for ReductionNAESATToMaxCut {
+    type Source = NAESatisfiability;
+    type Target = MaxCut<SimpleGraph, i32>;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+        // Variable x_i corresponds to vertex 2*i (positive literal vertex).
+        // The partition side of v_i directly encodes the truth value of x_i.
+        (0..self.num_vars).map(|i| target_solution[2 * i]).collect()
+    }
+}
+
+/// Map a 1-indexed signed literal to its vertex index.
+///
+/// Positive literal j → vertex 2*(j-1) (positive literal vertex).
+/// Negative literal -j → vertex 2*(j-1)+1 (negative literal vertex).
+fn literal_vertex(lit: i32) -> usize {
+    let var_idx = (lit.unsigned_abs() as usize) - 1;
+    if lit > 0 {
+        2 * var_idx
+    } else {
+        2 * var_idx + 1
+    }
+}
+
+#[reduction(overhead = {
+    num_vertices = "2 * num_vars",
+    num_edges = "num_vars + 3 * num_clauses",
+})]
+impl ReduceTo<MaxCut<SimpleGraph, i32>> for NAESatisfiability {
+    type Result = ReductionNAESATToMaxCut;
+
+    fn reduce_to(&self) -> Self::Result {
+        let n = self.num_vars();
+        let m = self.num_clauses();
+
+        for (idx, clause) in self.clauses().iter().enumerate() {
+            assert_eq!(
+                clause.len(),
+                3,
+                "Clause {idx} has {} literals; NAE-3-SAT to MaxCut requires exactly 3",
+                clause.len()
+            );
+        }
+
+        // Forcing weight: M > max total clause contribution (2m), so all
+        // variable-gadget edges are always cut in an optimal partition.
+        let big_m: i32 = 2 * (m as i32) + 1;
+
+        // Accumulate edges with merged weights (parallel edges sum).
+        let mut edge_weights: BTreeMap<(usize, usize), i32> = BTreeMap::new();
+
+        // Variable gadget edges: (v_i, v_i') with weight M.
+        for i in 0..n {
+            let key = (2 * i, 2 * i + 1);
+            *edge_weights.entry(key).or_insert(0) += big_m;
+        }
+
+        // Clause triangle edges: for each 3-literal clause, add weight-1
+        // edges between all pairs of literal vertices.
+        for clause in self.clauses() {
+            let lits = &clause.literals;
+            for a in 0..lits.len() {
+                for b in (a + 1)..lits.len() {
+                    let u = literal_vertex(lits[a]);
+                    let v = literal_vertex(lits[b]);
+                    let key = if u < v { (u, v) } else { (v, u) };
+                    *edge_weights.entry(key).or_insert(0) += 1;
+                }
+            }
+        }
+
+        let edges: Vec<(usize, usize)> = edge_weights.keys().copied().collect();
+        let weights: Vec<i32> = edge_weights.values().copied().collect();
+
+        let target = MaxCut::new(SimpleGraph::new(2 * n, edges), weights);
+
+        ReductionNAESATToMaxCut {
+            target,
+            num_vars: n,
+        }
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+    use crate::models::formula::CNFClause;
+
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "naesatisfiability_to_maxcut",
+        build: || {
+            // NAE-3-SAT: n=3, m=2
+            // C1 = (x1, x2, x3), C2 = (¬x1, ¬x2, ¬x3)
+            let source = NAESatisfiability::new(
+                3,
+                vec![
+                    CNFClause::new(vec![1, 2, 3]),
+                    CNFClause::new(vec![-1, -2, -3]),
+                ],
+            );
+            crate::example_db::specs::rule_example_with_witness::<_, MaxCut<SimpleGraph, i32>>(
+                source,
+                SolutionPair {
+                    source_config: vec![1, 0, 0],
+                    target_config: vec![1, 0, 0, 1, 0, 1],
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/naesatisfiability_maxcut.rs"]
+mod tests;

src/unit_tests/rules/analysis.rs

@@ -243,7 +243,9 @@ fn test_find_dominated_rules_returns_known_set() {
     let allowed: std::collections::HashSet<(&str, &str)> = [
         // Composite through CircuitSAT → ILP is better
         ("Factoring", "ILP {variable: \"i32\"}"),
-        // K3-SAT → QUBO via SAT → CircuitSAT → SpinGlass chain
+        // K2-SAT → QUBO via SAT → NAE-SAT → MaxCut → SpinGlass chain
+        ("KSatisfiability {k: \"K2\"}", "QUBO {weight: \"f64\"}"),
+        // K3-SAT → QUBO via MVC → MIS → MaxSetPacking chain
         ("KSatisfiability {k: \"K3\"}", "QUBO {weight: \"f64\"}"),
         // Knapsack -> ILP -> QUBO is better than the direct penalty reduction
         ("Knapsack", "QUBO {weight: \"f64\"}"),

src/unit_tests/rules/naesatisfiability_maxcut.rs

@@ -0,0 +1,155 @@
+use super::*;
+use crate::models::formula::CNFClause;
+use crate::rules::test_helpers::assert_satisfaction_round_trip_from_optimization_target;
+use crate::solvers::BruteForce;
+use crate::traits::Problem;
+use crate::types::Max;
+
+#[test]
+fn test_naesatisfiability_to_maxcut_closed_loop() {
+    // NAE-3-SAT: C1 = (x1, x2, x3), C2 = (¬x1, ¬x2, ¬x3)
+    let naesat = NAESatisfiability::new(
+        3,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![-1, -2, -3]),
+        ],
+    );
+
+    let reduction = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&naesat);
+
+    assert_satisfaction_round_trip_from_optimization_target(
+        &naesat,
+        &reduction,
+        "NAE-SAT->MaxCut closed loop",
+    );
+}
+
+#[test]
+fn test_reduction_structure() {
+    // n=3, m=2: expect 6 vertices, up to 9 edges
+    let naesat = NAESatisfiability::new(
+        3,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![-1, -2, -3]),
+        ],
+    );
+
+    let reduction = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&naesat);
+    let maxcut = reduction.target_problem();
+
+    assert_eq!(maxcut.num_vertices(), 6); // 2n
+                                          // 3 variable edges + 3 triangle edges for C1 + 3 triangle edges for C2
+                                          // No overlap since C1 uses positive literal vertices and C2 uses negative
+    assert_eq!(maxcut.num_edges(), 9); // n + 3m = 3 + 6
+}
+
+#[test]
+fn test_variable_gadget_weights() {
+    // Verify variable-gadget edges have weight M = 2m + 1
+    let naesat = NAESatisfiability::new(
+        2,
+        vec![
+            CNFClause::new(vec![1, 2, -1]),
+            CNFClause::new(vec![-1, -2, 1]),
+        ],
+    );
+
+    let reduction = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&naesat);
+    let maxcut = reduction.target_problem();
+
+    // M = 2*2 + 1 = 5
+    // Variable gadget edge (v0, v0') = (0, 1) should have weight >= 5
+    let w01 = maxcut.edge_weight(0, 1).copied().unwrap();
+    assert!(
+        w01 >= 5,
+        "Variable gadget edge weight should be at least M=5, got {w01}"
+    );
+}
+
+#[test]
+fn test_optimal_cut_value() {
+    // For a satisfiable NAE-3-SAT instance, optimal cut = n*M + 2m
+    let naesat = NAESatisfiability::new(
+        3,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![-1, -2, -3]),
+        ],
+    );
+
+    let reduction = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&naesat);
+    let maxcut = reduction.target_problem();
+
+    let solver = BruteForce::new();
+    let witness = solver.find_witness(maxcut).unwrap();
+    let value = maxcut.evaluate(&witness);
+
+    // n=3, m=2, M=5: threshold = 3*5 + 2*2 = 19
+    assert_eq!(value, Max(Some(19)));
+}
+
+#[test]
+fn test_solution_extraction() {
+    let naesat = NAESatisfiability::new(
+        3,
+        vec![
+            CNFClause::new(vec![1, 2, 3]),
+            CNFClause::new(vec![-1, -2, -3]),
+        ],
+    );
+
+    let reduction = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&naesat);
+
+    // Target config: v0=1, v0'=0, v1=0, v1'=1, v2=0, v2'=1
+    // → x1=1, x2=0, x3=0
+    let source_sol = reduction.extract_solution(&[1, 0, 0, 1, 0, 1]);
+    assert_eq!(source_sol, vec![1, 0, 0]);
+    assert!(naesat.is_valid_solution(&source_sol));
+}
+
+#[test]
+fn test_larger_instance() {
+    // 4 variables, 3 clauses
+    let naesat = NAESatisfiability::new(
+        4,
+        vec![
+            CNFClause::new(vec![1, 2, -3]),
+            CNFClause::new(vec![-2, 3, 4]),
+            CNFClause::new(vec![1, -3, -4]),
+        ],
+    );
+
+    let reduction = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&naesat);
+    let maxcut = reduction.target_problem();
+
+    assert_eq!(maxcut.num_vertices(), 8); // 2*4
+
+    assert_satisfaction_round_trip_from_optimization_target(
+        &naesat,
+        &reduction,
+        "NAE-SAT->MaxCut larger instance",
+    );
+}
+
+#[test]
+fn test_edge_merging() {
+    // Clause contains both x1 and ¬x1: the triangle edge (v1, v1') overlaps
+    // with the variable gadget edge and weights should merge.
+    let naesat = NAESatisfiability::new(2, vec![CNFClause::new(vec![1, -1, 2])]);
+
+    let reduction = ReduceTo::<MaxCut<SimpleGraph, i32>>::reduce_to(&naesat);
+    let maxcut = reduction.target_problem();
+
+    // Variable edge (0,1) should have weight M + 1 = 3 + 1 = 4
+    // (M = 2*1 + 1 = 3, plus 1 from the triangle edge)
+    let w01 = maxcut.edge_weight(0, 1).copied().unwrap();
+    assert_eq!(w01, 4);
+
+    assert_satisfaction_round_trip_from_optimization_target(
+        &naesat,
+        &reduction,
+        "NAE-SAT->MaxCut edge merging",
+    );
+}