problemreductions/rules/
maximum2satisfiability_maxcut.rs

1//! Reduction from Maximum 2-Satisfiability (MAX-2-SAT) to MaxCut.
2//!
3//! The reduction uses one reference vertex `s` plus one vertex per Boolean
4//! variable. For a partition of the target graph, a variable is interpreted as
5//! true exactly when its vertex lies on the same side of the cut as `s`.
6//!
7//! For each 2-literal clause `(l_1 \/ l_2)`, we add the doubled affine form of
8//! its satisfaction indicator:
9//! `2 * sat(C) = K_C + w(s,a) cut(s,a) + w(s,b) cut(s,b) + w(a,b) cut(a,b)`.
10//! Summing over clauses yields
11//! `2 * satisfied(phi, x) = C_0 + cut_value(G_phi, partition)`, so every
12//! optimal cut extracts to an optimal MAX-2-SAT assignment.
13
14use crate::models::formula::Maximum2Satisfiability;
15use crate::models::graph::MaxCut;
16use crate::reduction;
17use crate::rules::traits::{ReduceTo, ReductionResult};
18use crate::topology::SimpleGraph;
19use std::collections::BTreeMap;
20
21/// Result of reducing Maximum2Satisfiability to MaxCut.
22#[derive(Debug, Clone)]
23pub struct ReductionMaximum2SatisfiabilityToMaxCut {
24    target: MaxCut<SimpleGraph, i32>,
25    source_num_vars: usize,
26}
27
28impl ReductionResult for ReductionMaximum2SatisfiabilityToMaxCut {
29    type Source = Maximum2Satisfiability;
30    type Target = MaxCut<SimpleGraph, i32>;
31
32    fn target_problem(&self) -> &Self::Target {
33        &self.target
34    }
35
36    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
37        let reference_side = target_solution[0];
38        (0..self.source_num_vars)
39            .map(|i| usize::from(target_solution[i + 1] == reference_side))
40            .collect()
41    }
42}
43
44fn add_edge_weight(weights: &mut BTreeMap<(usize, usize), i32>, u: usize, v: usize, delta: i32) {
45    let edge = if u < v { (u, v) } else { (v, u) };
46    *weights.entry(edge).or_insert(0) += delta;
47}
48
49fn literal_polarity(lit: i32) -> i32 {
50    if lit > 0 {
51        1
52    } else {
53        -1
54    }
55}
56
57#[reduction(
58    overhead = {
59        num_vertices = "num_vars + 1",
60        num_edges = "num_vars + num_clauses",
61    }
62)]
63impl ReduceTo<MaxCut<SimpleGraph, i32>> for Maximum2Satisfiability {
64    type Result = ReductionMaximum2SatisfiabilityToMaxCut;
65
66    fn reduce_to(&self) -> Self::Result {
67        let mut accumulated = BTreeMap::new();
68
69        for clause in self.clauses() {
70            let literals = &clause.literals;
71            let (lit_a, lit_b) = (literals[0], literals[1]);
72            let var_a = lit_a.unsigned_abs() as usize;
73            let var_b = lit_b.unsigned_abs() as usize;
74            let sigma_a = literal_polarity(lit_a);
75            let sigma_b = literal_polarity(lit_b);
76
77            add_edge_weight(&mut accumulated, 0, var_a, -sigma_a);
78            add_edge_weight(&mut accumulated, 0, var_b, -sigma_b);
79            if var_a != var_b {
80                add_edge_weight(&mut accumulated, var_a, var_b, sigma_a * sigma_b);
81            }
82        }
83
84        let (edges, weights): (Vec<_>, Vec<_>) = accumulated
85            .into_iter()
86            .filter(|(_, weight)| *weight != 0)
87            .unzip();
88
89        let target = MaxCut::new(SimpleGraph::new(self.num_vars() + 1, edges), weights);
90
91        ReductionMaximum2SatisfiabilityToMaxCut {
92            target,
93            source_num_vars: self.num_vars(),
94        }
95    }
96}
97
98#[cfg(feature = "example-db")]
99pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
100    use crate::export::SolutionPair;
101    use crate::models::formula::CNFClause;
102
103    vec![crate::example_db::specs::RuleExampleSpec {
104        id: "maximum2satisfiability_to_maxcut",
105        build: || {
106            let source = Maximum2Satisfiability::new(
107                3,
108                vec![
109                    CNFClause::new(vec![1, 2]),
110                    CNFClause::new(vec![-1, 3]),
111                    CNFClause::new(vec![2, -3]),
112                    CNFClause::new(vec![-1, -2]),
113                    CNFClause::new(vec![1, 3]),
114                ],
115            );
116            crate::example_db::specs::rule_example_with_witness::<_, MaxCut<SimpleGraph, i32>>(
117                source,
118                SolutionPair {
119                    // x1=F, x2=T, x3=T satisfies all five clauses.
120                    source_config: vec![0, 1, 1],
121                    // Vertex 0 is the reference vertex s. Variables are true
122                    // exactly when they share s's side of the cut.
123                    target_config: vec![0, 1, 0, 0],
124                },
125            )
126        },
127    }]
128}
129
130#[cfg(test)]
131#[path = "../unit_tests/rules/maximum2satisfiability_maxcut.rs"]
132mod tests;
problemreductions/rules/maximum2satisfiability_maxcut.rs

problemreductions/rules/
maximum2satisfiability_maxcut.rs
