From c64351278faac0768e3d0a145465094fa5a9bccd Mon Sep 17 00:00:00 2001 From: zazabap Date: Sun, 29 Mar 2026 16:03:55 +0000 Subject: [PATCH] feat: add NAESatisfiability to MaxCut reduction (#166) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implement the classic NAE-3-SAT → MaxCut reduction via variable gadgets (complementary vertex pairs with weight M = 2m+1) and clause triangles. Each NAE-satisfied clause contributes exactly 2 cut edges, giving a tight threshold of nM + 2m. Includes reduction rule, unit tests (7 tests), canonical example_db entry, paper entry, and updated dominated-rules allow-list. Co-Authored-By: Claude Opus 4.6 --- docs/paper/reductions.typ | 12 ++ src/rules/mod.rs | 2 + src/rules/naesatisfiability_maxcut.rs | 144 ++++++++++++++++ src/unit_tests/rules/analysis.rs | 4 +- .../rules/naesatisfiability_maxcut.rs | 155 ++++++++++++++++++ 5 files changed, 316 insertions(+), 1 deletion(-) create mode 100644 src/rules/naesatisfiability_maxcut.rs create mode 100644 src/unit_tests/rules/naesatisfiability_maxcut.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 15c431e52..4d65cb772 100644 --- a/docs/paper/reductions.typ +++ b/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. ][ diff --git a/src/rules/mod.rs b/src/rules/mod.rs index f1e51cf8e..0fd594239 100644 --- a/src/rules/mod.rs +++ b/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, + /// Number of variables in the source NAE-SAT instance. + num_vars: usize, +} + +impl ReductionResult for ReductionNAESATToMaxCut { + type Source = NAESatisfiability; + type Target = MaxCut; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + // 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> 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 = 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 { + 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>( + 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; diff --git a/src/unit_tests/rules/analysis.rs b/src/unit_tests/rules/analysis.rs index 020b89b66..6e40684f1 100644 --- a/src/unit_tests/rules/analysis.rs +++ b/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\"}"), diff --git a/src/unit_tests/rules/naesatisfiability_maxcut.rs b/src/unit_tests/rules/naesatisfiability_maxcut.rs new file mode 100644 index 000000000..585116d35 --- /dev/null +++ b/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::>::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::>::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::>::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::>::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::>::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::>::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::>::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", + ); +}