problemreductions/rules/
naesatisfiability_maxcut.rs

1//! Reduction from NAESatisfiability to MaxCut.
2//!
3//! Classical reduction from Not-All-Equal SAT to Maximum Cut (Karp 1972,
4//! Garey & Johnson ND16). For each variable x_i, create two vertices
5//! (positive literal 2i, negative literal 2i+1) connected by a heavy
6//! "variable edge" of weight M = m+1 where m is the number of clauses.
7//! For each clause, add weight-1 edges between all pairs of literal vertices
8//! in that clause. An optimal max-cut of value n*M + sum(k_j - 1) exists
9//! if and only if the NAE-SAT formula is satisfiable.
10//!
11//! Reference: Garey & Johnson, *Computers and Intractability*, ND16, p.210
12
13use crate::models::formula::NAESatisfiability;
14use crate::models::graph::MaxCut;
15use crate::reduction;
16use crate::rules::traits::{ReduceTo, ReductionResult};
17use crate::topology::SimpleGraph;
18
19/// Result of reducing NAESatisfiability to MaxCut.
20#[derive(Debug, Clone)]
21pub struct ReductionNAESATToMaxCut {
22    target: MaxCut<SimpleGraph, i32>,
23    source_num_vars: usize,
24}
25
26impl ReductionResult for ReductionNAESATToMaxCut {
27    type Source = NAESatisfiability;
28    type Target = MaxCut<SimpleGraph, i32>;
29
30    fn target_problem(&self) -> &Self::Target {
31        &self.target
32    }
33
34    /// Extract a NAE-SAT assignment from a MaxCut partition.
35    ///
36    /// Variable x_i is assigned based on vertex 2*i: if it is in set 0
37    /// (config[2*i] == 0), set x_i = false (config value 0); if in set 1,
38    /// set x_i = true (config value 1).
39    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
40        (0..self.source_num_vars)
41            .map(|i| target_solution[2 * i])
42            .collect()
43    }
44}
45
46/// Map a literal to its vertex index.
47///
48/// Positive literal l (l > 0): vertex 2*(l-1)
49/// Negative literal l (l < 0): vertex 2*((-l)-1) + 1
50fn literal_vertex(lit: i32) -> usize {
51    let var_idx = lit.unsigned_abs() as usize - 1;
52    if lit > 0 {
53        2 * var_idx
54    } else {
55        2 * var_idx + 1
56    }
57}
58
59#[reduction(
60    overhead = {
61        num_vertices = "2 * num_vars",
62        num_edges = "num_vars + num_literal_pairs",
63    }
64)]
65impl ReduceTo<MaxCut<SimpleGraph, i32>> for NAESatisfiability {
66    type Result = ReductionNAESATToMaxCut;
67
68    fn reduce_to(&self) -> Self::Result {
69        let n = self.num_vars();
70        let m = self.num_clauses();
71        let total_vertices = 2 * n;
72        let big_m = (m + 1) as i32;
73
74        let mut edges: Vec<(usize, usize)> = Vec::new();
75        let mut weights: Vec<i32> = Vec::new();
76
77        // Step 1: Variable edges — connect (2*i, 2*i+1) with weight M = m+1
78        for i in 0..n {
79            edges.push((2 * i, 2 * i + 1));
80            weights.push(big_m);
81        }
82
83        // Step 2: Clause edges — for each clause, add weight-1 edges between
84        // all pairs of literal vertices
85        for clause in self.clauses() {
86            let lits = &clause.literals;
87            for a in 0..lits.len() {
88                for b in (a + 1)..lits.len() {
89                    edges.push((literal_vertex(lits[a]), literal_vertex(lits[b])));
90                    weights.push(1);
91                }
92            }
93        }
94
95        let graph = SimpleGraph::new(total_vertices, edges);
96        let target = MaxCut::new(graph, weights);
97
98        ReductionNAESATToMaxCut {
99            target,
100            source_num_vars: n,
101        }
102    }
103}
104
105#[cfg(feature = "example-db")]
106pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
107    use crate::export::SolutionPair;
108    use crate::models::formula::CNFClause;
109
110    vec![crate::example_db::specs::RuleExampleSpec {
111        id: "naesatisfiability_to_maxcut",
112        build: || {
113            // 3 variables, 2 clauses:
114            //   C1 = (x1, x2, ~x3)
115            //   C2 = (~x1, x3, x2)
116            // NAE-satisfying: x1=T, x2=F, x3=T
117            let source = NAESatisfiability::new(
118                3,
119                vec![
120                    CNFClause::new(vec![1, 2, -3]),
121                    CNFClause::new(vec![-1, 3, 2]),
122                ],
123            );
124            crate::example_db::specs::rule_example_with_witness::<_, MaxCut<SimpleGraph, i32>>(
125                source,
126                SolutionPair {
127                    // x1=T(1), x2=F(0), x3=T(1)
128                    source_config: vec![1, 0, 1],
129                    // Vertices: x1(0)=1, ~x1(1)=0, x2(2)=0, ~x2(3)=1, x3(4)=1, ~x3(5)=0
130                    // All variable edges cross (weight M=3 each) -> 3*3=9
131                    // C1=(x1,x2,~x3): vertices 0,2,5 -> sides {1},{0,0} -> edges (0,2) crosses, (0,5) crosses, (2,5) doesn't -> +2
132                    // C2=(~x1,x3,x2): vertices 1,4,2 -> sides {0},{1,0} -> edges (1,4) crosses, (1,2) doesn't, (4,2) crosses -> +2
133                    // Total = 9 + 2 + 2 = 13
134                    target_config: vec![1, 0, 0, 1, 1, 0],
135                },
136            )
137        },
138    }]
139}
140
141#[cfg(test)]
142#[path = "../unit_tests/rules/naesatisfiability_maxcut.rs"]
143mod tests;
problemreductions/rules/naesatisfiability_maxcut.rs

problemreductions/rules/
naesatisfiability_maxcut.rs
