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, i64>,
25    source_num_vars: usize,
26}
27
28impl ReductionResult for ReductionMaximum2SatisfiabilityToMaxCut {
29    type Source = Maximum2Satisfiability;
30    type Target = MaxCut<SimpleGraph, i64>;
31
32    fn target_problem(&self) -> &Self::Target {
33        &self.target
34    }
35
36    fn extract_solution(
37        &self,
38        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
39    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
40        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
41
42        Ok({
43            let reference_side = target_solution[0];
44            (0..self.source_num_vars)
45                .map(|i| target_solution[i + 1] == reference_side)
46                .collect()
47        })
48    }
49}
50
51fn add_edge_weight(weights: &mut BTreeMap<(usize, usize), i64>, u: usize, v: usize, delta: i64) {
52    let edge = if u < v { (u, v) } else { (v, u) };
53    *weights.entry(edge).or_insert(0) += delta;
54}
55
56fn literal_polarity(lit: i64) -> i64 {
57    if lit > 0 {
58        1
59    } else {
60        -1
61    }
62}
63
64#[reduction(
65    transform = upper_bound {
66        num_vertices = "num_vars + 1",
67        num_edges = "(num_vars + 1)^2",
68    }
69)]
70impl ReduceTo<MaxCut<SimpleGraph, i64>> for Maximum2Satisfiability {
71    type Result = ReductionMaximum2SatisfiabilityToMaxCut;
72
73    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
74        let mut accumulated = BTreeMap::new();
75
76        for clause in self.clauses() {
77            let literals = &clause.literals;
78            let (lit_a, lit_b) = (literals[0], literals[1]);
79            let var_a = lit_a.unsigned_abs() as usize;
80            let var_b = lit_b.unsigned_abs() as usize;
81            let sigma_a = literal_polarity(lit_a);
82            let sigma_b = literal_polarity(lit_b);
83
84            add_edge_weight(&mut accumulated, 0, var_a, -sigma_a);
85            add_edge_weight(&mut accumulated, 0, var_b, -sigma_b);
86            if var_a != var_b {
87                add_edge_weight(&mut accumulated, var_a, var_b, sigma_a * sigma_b);
88            }
89        }
90
91        let (edges, weights): (Vec<_>, Vec<_>) = accumulated
92            .into_iter()
93            .filter(|(_, weight)| *weight != 0)
94            .unzip();
95
96        let target = MaxCut::new(SimpleGraph::new(self.num_vars() + 1, edges), weights);
97
98        Ok(ReductionMaximum2SatisfiabilityToMaxCut {
99            target,
100            source_num_vars: self.num_vars(),
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: "maximum2satisfiability_to_maxcut",
112        build: || {
113            let source = Maximum2Satisfiability::new(
114                3,
115                vec![
116                    CNFClause::new(vec![1, 2]),
117                    CNFClause::new(vec![-1, 3]),
118                    CNFClause::new(vec![2, -3]),
119                    CNFClause::new(vec![-1, -2]),
120                    CNFClause::new(vec![1, 3]),
121                ],
122            );
123            crate::example_db::specs::rule_example_with_witness::<_, MaxCut<SimpleGraph, i64>>(
124                source,
125                SolutionPair {
126                    // x1=F, x2=T, x3=T satisfies all five clauses.
127                    source_config: serde_json::json!(vec![false, true, true]),
128                    // Vertex 0 is the reference vertex s. Variables are true
129                    // exactly when they share s's side of the cut.
130                    target_config: serde_json::json!(vec![false, true, false, false]),
131                },
132            )
133        },
134    }]
135}
136
137#[cfg(test)]
138#[path = "../unit_tests/rules/maximum2satisfiability_maxcut.rs"]
139mod tests;
problemreductions/rules/maximum2satisfiability_maxcut.rs

problemreductions/rules/
maximum2satisfiability_maxcut.rs
