Fix #1102: MaxCut/One to Maximum2Satisfiability

docs/paper/reductions.typ

@@ -11437,6 +11437,87 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
 Each reduction is presented as a *Rule* (with linked problem names and overhead from the graph data), followed by a *Proof* (construction, correctness, variable mapping, solution extraction), and optionally a *Concrete Example* (a small instance with verified solution). Problem names in the rule title link back to their definitions in @sec:problems.
 
 
+#let mc_max2sat = load-example("MaxCut", "Maximum2Satisfiability")
+#let mc_max2sat_sol = mc_max2sat.solutions.at(0)
+#let mc_max2sat_cut = mc_max2sat.source.instance.graph.edges.filter(edge =>
+  mc_max2sat_sol.source_config.at(edge.at(0)) != mc_max2sat_sol.source_config.at(edge.at(1))
+).len()
+#let mc_max2sat_satisfied = mc_max2sat.target.instance.clauses.filter(clause =>
+  clause.literals.any(lit => {
+    let bit = mc_max2sat_sol.target_config.at(calc.abs(lit) - 1)
+    if lit > 0 { bit == 1 } else { bit == 0 }
+  })
+).len()
+#reduction-rule("MaxCut", "Maximum2Satisfiability",
+  example: true,
+  example-caption: [Four-cycle with one diagonal ($n = #mc_max2sat.source.instance.graph.num_vertices$, $|E| = #mc_max2sat.source.instance.graph.edges.len()$, ten target clauses)],
+  extra: [
+    #pred-commands(
+      "pred create --example " + problem-spec(mc_max2sat.source) + " --to " + target-spec(mc_max2sat) + " -o maxcut.json",
+      "pred reduce maxcut.json --to " + target-spec(mc_max2sat) + " -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate maxcut.json --config " + mc_max2sat_sol.source_config.map(str).join(","),
+    )
+
+    #{
+      let positions = ((0, 0), (1, 0), (1, 1), (0, 1))
+      let fills = mc_max2sat_sol.source_config.map(bit => graph-colors.at(bit))
+      align(center, canvas(length: 0.75cm, {
+        for (u, v) in mc_max2sat.source.instance.graph.edges {
+          g-edge(positions.at(u), positions.at(v))
+        }
+        for (v, pos) in positions.enumerate() {
+          g-node(pos, name: str(v), fill: fills.at(v), label: str(v))
+        }
+      }))
+    }
+
+    *Step 1 -- Read the cut instance.* The fixture has #mc_max2sat.source.instance.graph.num_vertices vertices and the five edge occurrences
+    #raw(mc_max2sat.source.instance.graph.edges.map(edge => "(" + edge.map(str).join(",") + ")").join(", ")).
+    Its canonical cut assignment is $(#mc_max2sat_sol.source_config.map(str).join(", "))$: vertices colored differently lie on opposite sides.
+
+    *Step 2 -- Replace each edge by two clauses.* For every displayed edge occurrence $(u,v)$, introduce $(x_u or x_v)$ and $(not x_u or not x_v)$. Thus the five edges produce #mc_max2sat.target.instance.clauses.len() clauses. In the fixture's one-based literal encoding, their literal pairs are
+    #raw(mc_max2sat.target.instance.clauses.map(clause => "[" + clause.literals.map(str).join(",") + "]").join(", ")).
+
+    *Step 3 -- Verify the objectives.* Under the identical target assignment $(#mc_max2sat_sol.target_config.map(str).join(", "))$, exactly #mc_max2sat_cut of the five edges cross. The two clauses belonging to each crossing edge are both true, while each noncrossing edge contributes one true clause. Hence the target value is $5 + #mc_max2sat_cut = #mc_max2sat_satisfied$. The source value is #mc_max2sat_cut and the target value is #mc_max2sat_satisfied, so the direct extraction recovers the optimal cut #sym.checkmark.
+
+    *Multiplicity:* The fixture stores one canonical optimum. Complementing all four bits gives the other orientation of the same cut and also satisfies nine clauses; this second optimum follows from the construction rather than from the fixture's solution count.
+  ],
+)[
+  This $O(n + m)$ reduction @gramm2003max2sat maps an unweighted graph $G = (V,E)$ to a 2-CNF formula with $n = |V|$ variables and $2m$ clauses. Every edge occurrence $(u,v)$ contributes the pair $(x_u or x_v)$ and $(not x_u or not x_v)$, so maximizing satisfied clauses is equivalent to maximizing cut edges.
+][
+  _Construction._ Given an unweighted MaxCut instance $G = (V,E)$, introduce one Boolean variable $x_v$ for every $v in V$. The value $x_v$ denotes the side of the cut containing $v$. For every edge occurrence $e = (u,v)$, append two clauses
+  $
+    C_e^+ = (x_u or x_v), quad C_e^- = (not x_u or not x_v).
+  $
+  Edge occurrences are processed independently, so the target has exactly $n$ variables and $2m$ clauses.
+
+  _Per-edge identity._ The complete truth table is
+  #table(
+    columns: (auto, auto, auto, auto, auto),
+    inset: 4pt,
+    align: center,
+    table.header([$x_u$], [$x_v$], [$C_e^+$], [$C_e^-$], [satisfied / cut]),
+    [$0$], [$0$], [true], [false], [$1 = 1 + 0$],
+    [$0$], [$1$], [true], [true], [$2 = 1 + 1$],
+    [$1$], [$0$], [true], [true], [$2 = 1 + 1$],
+    [$1$], [$1$], [false], [true], [$1 = 1 + 0$],
+  )
+  Therefore each edge occurrence contributes exactly $1 + bold(1)[x_u != x_v]$ satisfied clauses. Summing over all occurrences gives
+  $
+    "sat"(bold(x)) = m + "cut"_G(bold(x)).
+  $
+
+  _Correctness._ ($arrow.r.double$) Let $bold(x)$ be a maximum cut. The per-edge truth table shows that its target assignment satisfies $m + "cut"_G(bold(x))$ clauses. If another assignment satisfied more clauses, subtracting the fixed $m$ in the identity would give a larger cut, contradicting maximality.
+
+  ($arrow.l.double$) Let $bold(x)$ maximize the number of satisfied target clauses. If some cut crossed more edges, using its side bits as a truth assignment would, by the same truth table, satisfy more than $m + "cut"_G(bold(x))$ clauses. This contradicts target optimality, so $bold(x)$ is a maximum cut.
+
+  _Loops and parallel edges._ If $u = v$, the pair becomes $(x_u or x_u)$ and $(not x_u or not x_u)$: exactly one clause is true, matching the fact that a loop never crosses the cut. Parallel edge occurrences generate repeated clause pairs. Each copy contributes independently on both sides of the identity, so multiplicity is preserved.
+
+  _Solution extraction._ Return the target assignment unchanged. Variable $x_v$ already records the source cut side of vertex $v$, so this is a direct canonical witness mapping.
+]
+
+
 #let max2sat_mc = load-example("Maximum2Satisfiability", "MaxCut")
 #let max2sat_mc_sol = max2sat_mc.solutions.at(0)
 #reduction-rule("Maximum2Satisfiability", "MaxCut",

docs/paper/references.bib

@@ -1869,6 +1869,17 @@ @article{gramm2009
   doi     = {10.1145/1412228.1412236}
 }
 
+@article{gramm2003max2sat,
+  author  = {Jens Gramm and Edward A. Hirsch and Rolf Niedermeier and Peter Rossmanith},
+  title   = {Worst-Case Upper Bounds for {MAX-2-SAT} with an Application to {MAX-CUT}},
+  journal = {Discrete Applied Mathematics},
+  volume  = {130},
+  number  = {2},
+  pages   = {139--155},
+  year    = {2003},
+  doi     = {10.1016/S0166-218X(02)00402-X}
+}
+
 @inproceedings{lovasz1973,
   author    = {László Lovász},
   title     = {Coverings and Colorings of Hypergraphs},

src/rules/maxcut_maximum2satisfiability.rs

@@ -0,0 +1,85 @@
+//! Reduction from unweighted MaxCut to Maximum 2-Satisfiability.
+
+use crate::models::formula::{CNFClause, Maximum2Satisfiability};
+use crate::models::graph::MaxCut;
+use crate::reduction;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+use crate::topology::{Graph, SimpleGraph};
+use crate::types::One;
+
+/// Result of reducing unweighted MaxCut to Maximum2Satisfiability.
+#[derive(Debug, Clone)]
+pub struct ReductionMaxCutToMaximum2Satisfiability {
+    target: Maximum2Satisfiability,
+}
+
+fn vertex_literal(vertex: usize) -> i32 {
+    i32::try_from(vertex + 1)
+        .expect("MaxCut vertex index exceeds Maximum2Satisfiability's i32 literal range")
+}
+
+impl ReductionResult for ReductionMaxCutToMaximum2Satisfiability {
+    type Source = MaxCut<SimpleGraph, One>;
+    type Target = Maximum2Satisfiability;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
+        target_solution.to_vec()
+    }
+}
+
+#[reduction(
+    overhead = {
+        num_vars = "num_vertices",
+        num_clauses = "2 * num_edges",
+    }
+)]
+impl ReduceTo<Maximum2Satisfiability> for MaxCut<SimpleGraph, One> {
+    type Result = ReductionMaxCutToMaximum2Satisfiability;
+
+    fn reduce_to(&self) -> Self::Result {
+        let clauses = self
+            .graph()
+            .edges()
+            .into_iter()
+            .flat_map(|(u, v)| {
+                let u = vertex_literal(u);
+                let v = vertex_literal(v);
+                [CNFClause::new(vec![u, v]), CNFClause::new(vec![-u, -v])]
+            })
+            .collect();
+
+        ReductionMaxCutToMaximum2Satisfiability {
+            target: Maximum2Satisfiability::new(self.num_vertices(), clauses),
+        }
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "maxcut_to_maximum2satisfiability",
+        build: || {
+            let source = MaxCut::new(
+                SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0), (0, 2)]),
+                vec![One; 5],
+            );
+            crate::example_db::specs::rule_example_with_witness::<_, Maximum2Satisfiability>(
+                source,
+                SolutionPair {
+                    source_config: vec![0, 1, 0, 1],
+                    target_config: vec![0, 1, 0, 1],
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/maxcut_maximum2satisfiability.rs"]
+mod tests;

src/rules/mod.rs

@@ -76,6 +76,7 @@ pub(crate) mod ksatisfiability_simultaneousincongruences;
 pub(crate) mod ksatisfiability_subsetsum;
 pub(crate) mod ksatisfiability_timetabledesign;
 pub(crate) mod longestcommonsubsequence_maximumindependentset;
+pub(crate) mod maxcut_maximum2satisfiability;
 pub(crate) mod maxcut_minimumcutintoboundedsets;
 pub(crate) mod maxcut_minimummatrixcover;
 pub(crate) mod maximum2satisfiability_maxcut;
@@ -487,6 +488,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(ksatisfiability_subsetsum::canonical_rule_example_specs());
     specs.extend(ksatisfiability_timetabledesign::canonical_rule_example_specs());
     specs.extend(maximum2satisfiability_maxcut::canonical_rule_example_specs());
+    specs.extend(maxcut_maximum2satisfiability::canonical_rule_example_specs());
     specs.extend(maximumclique_maximumindependentset::canonical_rule_example_specs());
     specs.extend(maximumindependentset_integralflowbundles::canonical_rule_example_specs());
     specs.extend(maximumindependentset_maximumclique::canonical_rule_example_specs());

src/unit_tests/rules/maxcut_maximum2satisfiability.rs

@@ -0,0 +1,162 @@
+use super::*;
+use crate::solvers::{BruteForce, Solver};
+use crate::traits::Problem;
+use crate::types::Max;
+
+fn four_cycle_with_diagonal() -> MaxCut<SimpleGraph, One> {
+    MaxCut::new(
+        SimpleGraph::new(4, vec![(0, 1), (1, 2), (2, 3), (3, 0), (0, 2)]),
+        vec![One; 5],
+    )
+}
+
+fn assert_affine_identity(source: &MaxCut<SimpleGraph, One>) {
+    let reduction = ReduceTo::<Maximum2Satisfiability>::reduce_to(source);
+    let target = reduction.target_problem();
+
+    assert_eq!(target.num_vars(), source.num_vertices());
+    assert_eq!(target.num_clauses(), 2 * source.num_edges());
+
+    for mask in 0..(1usize << source.num_vertices()) {
+        let config: Vec<usize> = (0..source.num_vertices())
+            .map(|bit| (mask >> bit) & 1)
+            .collect();
+        let source_value = source.evaluate(&config).unwrap();
+        let target_value = target.evaluate(&config).unwrap();
+        assert_eq!(target_value, source.num_edges() + source_value as usize);
+        assert_eq!(reduction.extract_solution(&config), config);
+    }
+}
+
+#[test]
+fn test_maxcut_to_maximum2satisfiability_closed_loop() {
+    let source = four_cycle_with_diagonal();
+    let reduction = ReduceTo::<Maximum2Satisfiability>::reduce_to(&source);
+    let solver = BruteForce::new();
+
+    assert_eq!(solver.solve(&source), Max(Some(4)));
+    assert_eq!(solver.solve(reduction.target_problem()), Max(Some(9)));
+    for target_solution in solver.find_all_witnesses(reduction.target_problem()) {
+        let source_solution = reduction.extract_solution(&target_solution);
+        assert_eq!(source.evaluate(&source_solution), Max(Some(4)));
+    }
+}
+
+#[test]
+fn test_maxcut_to_maximum2satisfiability_structure_and_pointwise_identity() {
+    let source = four_cycle_with_diagonal();
+    let reduction = ReduceTo::<Maximum2Satisfiability>::reduce_to(&source);
+    let target = reduction.target_problem();
+
+    assert_eq!(target.num_vars(), 4);
+    assert_eq!(target.num_clauses(), 10);
+    assert_eq!(
+        target.clauses(),
+        &[
+            CNFClause::new(vec![1, 2]),
+            CNFClause::new(vec![-1, -2]),
+            CNFClause::new(vec![2, 3]),
+            CNFClause::new(vec![-2, -3]),
+            CNFClause::new(vec![3, 4]),
+            CNFClause::new(vec![-3, -4]),
+            CNFClause::new(vec![4, 1]),
+            CNFClause::new(vec![-4, -1]),
+            CNFClause::new(vec![1, 3]),
+            CNFClause::new(vec![-1, -3]),
+        ]
+    );
+    assert_affine_identity(&source);
+}
+
+#[test]
+fn test_maxcut_to_maximum2satisfiability_boundaries() {
+    let empty = MaxCut::new(SimpleGraph::empty(0), Vec::<One>::new());
+    assert_affine_identity(&empty);
+
+    let isolated = MaxCut::new(SimpleGraph::empty(3), Vec::<One>::new());
+    assert_affine_identity(&isolated);
+
+    let disconnected = MaxCut::new(SimpleGraph::new(4, vec![(0, 1)]), vec![One]);
+    assert_affine_identity(&disconnected);
+
+    let loop_graph = MaxCut::new(SimpleGraph::new(2, vec![(1, 1)]), vec![One]);
+    let loop_reduction = ReduceTo::<Maximum2Satisfiability>::reduce_to(&loop_graph);
+    assert_eq!(
+        loop_reduction.target_problem().clauses(),
+        &[CNFClause::new(vec![2, 2]), CNFClause::new(vec![-2, -2]),]
+    );
+    assert_affine_identity(&loop_graph);
+
+    let parallel = MaxCut::new(SimpleGraph::new(2, vec![(0, 1), (0, 1)]), vec![One, One]);
+    let parallel_reduction = ReduceTo::<Maximum2Satisfiability>::reduce_to(&parallel);
+    assert_eq!(
+        parallel_reduction.target_problem().clauses(),
+        &[
+            CNFClause::new(vec![1, 2]),
+            CNFClause::new(vec![-1, -2]),
+            CNFClause::new(vec![1, 2]),
+            CNFClause::new(vec![-1, -2]),
+        ]
+    );
+    assert_affine_identity(&parallel);
+}
+
+#[test]
+#[should_panic(expected = "MaxCut vertex index exceeds Maximum2Satisfiability's i32 literal range")]
+fn test_maxcut_to_maximum2satisfiability_rejects_unrepresentable_vertex_literal() {
+    vertex_literal(i32::MAX as usize);
+}
+
+#[test]
+fn test_maxcut_to_maximum2satisfiability_exhaustive_small_graphs() {
+    for num_vertices in 0..=4 {
+        let possible_edges: Vec<_> = (0..num_vertices)
+            .flat_map(|u| ((u + 1)..num_vertices).map(move |v| (u, v)))
+            .collect();
+        for edge_mask in 0..(1usize << possible_edges.len()) {
+            let edges: Vec<_> = possible_edges
+                .iter()
+                .enumerate()
+                .filter_map(|(i, edge)| ((edge_mask >> i) & 1 == 1).then_some(*edge))
+                .collect();
+            let source = MaxCut::new(
+                SimpleGraph::new(num_vertices, edges.clone()),
+                vec![One; edges.len()],
+            );
+            assert_affine_identity(&source);
+        }
+    }
+}
+
+#[cfg(feature = "example-db")]
+#[test]
+fn test_maxcut_to_maximum2satisfiability_canonical_example_spec() {
+    let spec = canonical_rule_example_specs()
+        .into_iter()
+        .find(|spec| spec.id == "maxcut_to_maximum2satisfiability")
+        .expect("missing canonical MaxCut -> Maximum2Satisfiability example spec");
+    let example = (spec.build)();
+
+    assert_eq!(example.source.problem, "MaxCut");
+    assert_eq!(example.target.problem, "Maximum2Satisfiability");
+    assert_eq!(example.source.instance["graph"]["num_vertices"], 4);
+    assert_eq!(
+        example.source.instance["graph"]["edges"]
+            .as_array()
+            .unwrap()
+            .len(),
+        5
+    );
+    assert_eq!(example.target.instance["num_vars"], 4);
+    assert_eq!(
+        example.target.instance["clauses"].as_array().unwrap().len(),
+        10
+    );
+    assert_eq!(
+        example.solutions,
+        vec![crate::export::SolutionPair {
+            source_config: vec![0, 1, 0, 1],
+            target_config: vec![0, 1, 0, 1],
+        }]
+    );
+}