Fix #1102: [Rule] MaxCut/One to Maximum2Satisfiability

docs/paper/reductions.typ

@@ -20048,6 +20048,70 @@ The following table shows concrete target-variable counts for example instances,
   _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction keeps the original vertices' bits and drops the auxiliary ones. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip.
 ]
 
+// MaxCut → Maximum2Satisfiability (#1102, Gramm et al. 2003)
+#let mc_m2s = load-example(
+  "MaxCut",
+  "Maximum2Satisfiability",
+  source-variant: (graph: "SimpleGraph", weight: "One"),
+)
+#let mc_m2s_sol = mc_m2s.solutions.at(0)
+#let mc_m2s_n = mc_m2s.source.instance.graph.num_vertices
+#let mc_m2s_edges = mc_m2s.source.instance.graph.edges
+#let mc_m2s_m = mc_m2s_edges.len()
+#let mc_m2s_clauses = mc_m2s.target.instance.clauses
+#let mc_m2s_cut(x) = mc_m2s_edges.filter(e => x.at(e.at(0)) != x.at(e.at(1))).len()
+#let mc_m2s_true(l, x) = if l > 0 { x.at(l - 1) } else { not x.at(-l - 1) }
+#let mc_m2s_sat(x) = mc_m2s_clauses.filter(c => c.literals.any(l => mc_m2s_true(l, x))).len()
+#let mc_m2s_pair(j, x) = range(2 * j, 2 * j + 2).filter(i => mc_m2s_clauses.at(i).literals.any(l => mc_m2s_true(l, x))).len()
+#let mc_m2s_all = range(calc.pow(2, mc_m2s_n)).map(mask => range(mc_m2s_n).map(i => calc.rem(calc.quo(mask, calc.pow(2, i)), 2) == 1))
+#let mc_m2s_opt_cut = calc.max(..mc_m2s_all.map(mc_m2s_cut))
+#let mc_m2s_opt_sat = calc.max(..mc_m2s_all.map(mc_m2s_sat))
+#let mc_m2s_x = mc_m2s_sol.target_config
+#let mc_m2s_side = range(mc_m2s_n).map(_ => false)
+#let mc_m2s_lit(l) = if l > 0 { $x_#(l - 1)$ } else { $not x_#(-l - 1)$ }
+#let mc_m2s_clause(c) = $(#mc_m2s_lit(c.literals.at(0)) or #mc_m2s_lit(c.literals.at(1)))$
+#let mc_m2s_edge(e) = $(#e.at(0), #e.at(1))$
+#reduction-rule("MaxCut", "Maximum2Satisfiability",
+  example: true,
+  example-source-variant: (graph: "SimpleGraph", weight: "One"),
+  example-caption: [$n = #mc_m2s_n$ vertices and $m = #mc_m2s_m$ edges become $#mc_m2s.target.instance.num_vars$ variables and $#mc_m2s_clauses.len()$ clauses],
+  extra: [
+    #pred-commands(
+      "pred create --example " + rule-spec(mc_m2s) + " -o maxcut.json",
+      "pred reduce maxcut.json --via route.json -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate maxcut.json --config " + cli-config(mc_m2s_sol.source_config),
+    )
+
+    *Step 1 -- Source instance.* The unweighted graph has $n = #mc_m2s_n$ vertices and the $m = #mc_m2s_m$ edges #mc_m2s_edges.map(mc_m2s_edge).join(", ").
+
+    *Step 2 -- Build the formula.* One variable per vertex and two clauses per edge, in edge order, give #mc_m2s.target.instance.num_vars variables and the #mc_m2s_clauses.len() clauses #mc_m2s_clauses.map(mc_m2s_clause).join(", ").
+
+    *Step 3 -- Verify the witness.* The canonical assignment $bold(x) = (#fmt-values(mc_m2s_x))$ cuts #mc_m2s_cut(mc_m2s_x) of the #mc_m2s_m edges. The clause pairs of the edges satisfy #range(mc_m2s_m).map(j => str(mc_m2s_pair(j, mc_m2s_x))).join(", ") clauses respectively: 2 for each cut edge and 1 for the uncut ones, #mc_m2s_sat(mc_m2s_x) $= #mc_m2s_m + #mc_m2s_cut(mc_m2s_x)$ in total. Placing every vertex on one side cuts nothing and satisfies exactly the #mc_m2s_sat(mc_m2s_side) $= m$ negative clauses. Enumerating all #mc_m2s_all.len() assignments gives the optima $"OPT"(G) = #mc_m2s_opt_cut$ and $"OPT"(phi) = #mc_m2s_opt_sat = m + "OPT"(G)$, so the witness is optimal on both sides and extracts to the cut $(#fmt-values(mc_m2s_sol.source_config))$ #sym.checkmark.
+
+    *Threshold (NO) check.* For $k = #(mc_m2s_opt_cut + 1)$ no cut of this graph has value at least $k$, and correspondingly no assignment satisfies $m + k = #(mc_m2s_m + mc_m2s_opt_cut + 1)$ clauses, since the target maximum is $#mc_m2s_opt_sat$. Both decision versions answer NO.
+
+    *Multiplicity:* The fixture stores one canonical witness. Complementing every variable leaves both objectives unchanged, so the complementary assignment is equally optimal.
+  ],
+)[
+  This $O(n + m)$ reduction @gramm2003 (Section 5) encodes an unweighted graph $G = (V, E)$ with $n$ vertices and $m$ edges as a 2-CNF formula $phi(G)$ with one variable per vertex and two clauses per edge. Every assignment satisfies exactly $m + "cut"$ clauses, so the target has $n$ variables and $2m$ clauses and maximum cuts are optimal assignments.
+][
+  _Construction._ Let $V = {0, dots, n-1}$ and let $E = (e_0, dots, e_(m-1))$ list the edges, $e_j = (u_j, v_j)$. Create a Boolean variable $x_v$ for each vertex $v$; $x_v = 1$ places $v$ on side 1 of the cut and $x_v = 0$ on side 0. For each $j$ in order, add the clauses $P_j = (x_(u_j) or x_(v_j))$ and $Q_j = (not x_(u_j) or not x_(v_j))$. No other clause is created. The source graph is simple: self-loops and repeated edges are rejected when the graph is constructed. Isolated vertices yield variables occurring in no clause, and an edgeless graph yields $n$ variables and no clause.
+
+  _Correctness._ Write $"cut"(bold(x)) = |{j : x_(u_j) != x_(v_j)}|$ and $"sat"(bold(x))$ for the number of satisfied clauses. For a single edge with $a = x_(u_j)$ and $b = x_(v_j)$: if $a != b$, one of them is 1 and one is 0, so both $P_j$ and $Q_j$ hold; if $a = b = 1$, only $P_j$ holds; if $a = b = 0$, only $Q_j$ holds. The pair therefore contributes $1 + [x_(u_j) != x_(v_j)]$, and summing over the $m$ disjoint pairs gives
+  $
+    "sat"(bold(x)) = m + "cut"(bold(x)) quad "for every" bold(x) in {0, 1}^n.
+  $
+
+  ($arrow.r.double$) If a configuration $bold(x)$ has $"cut"(bold(x)) >= k$, the same vector as an assignment satisfies $m + "cut"(bold(x)) >= m + k$ clauses.
+
+  ($arrow.l.double$) If an assignment $bold(y)$ satisfies at least $m + k$ clauses, the configuration $bold(x) = bold(y)$ (both have length $n$) has $"cut"(bold(x)) = "sat"(bold(y)) - m >= k$.
+
+  The identity map is a bijection between configurations and assignments that adds the constant $m$ to the objective, so $"OPT"(phi(G)) = m + "OPT"(G)$ and the optimal assignments are exactly the maximum cuts.
+
+  _Solution extraction._ Return the assignment unchanged: vertex $v$ goes to side 1 exactly when $x_v$ is true. Its cut value is $"sat"(bold(y)) - m$, so an optimal assignment extracts to a maximum cut. Assignments of the wrong length are rejected.
+]
+
 // 14. HamiltonianPath → IsomorphicSpanningTree (#912)
 #let hp_ist = load-example("HamiltonianPath", "IsomorphicSpanningTree")
 #let hp_ist_sol = hp_ist.solutions.at(0)

docs/paper/references.bib

@@ -2352,3 +2352,14 @@ @article{een2006
   pages = {1--26},
   doi = {10.3233/SAT190014},
 }
+
+@article{gramm2003,
+  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}
+}

src/rules/maxcut_maximum2satisfiability.rs

@@ -0,0 +1,121 @@
+//! Reduction from unit-weight MaxCut to Maximum 2-Satisfiability (MAX-2-SAT).
+//!
+//! Each vertex `v` becomes the Boolean variable `x_v` (CNF literal `v + 1`);
+//! its truth value is the side of the cut. Each edge `(u, v)`, in edge order,
+//! becomes the two clauses `(x_u OR x_v)` and `(NOT x_u OR NOT x_v)`.
+//!
+//! When the endpoints are on different sides both clauses hold; when they are
+//! on the same side exactly one does. Summing over the `m` edges gives, for
+//! every assignment `x`,
+//!     `satisfied(x) = m + cut(x)`,
+//! so the maximizers coincide and an assignment is extracted unchanged.
+//!
+//! Reference: Gramm, Hirsch, Niedermeier and Rossmanith, "Worst-case upper
+//! bounds for MAX-2-SAT with an application to MAX-CUT", Discrete Applied
+//! Mathematics 130(2), 2003, Section 5.
+
+use crate::models::formula::{CNFClause, Maximum2Satisfiability};
+use crate::models::graph::MaxCut;
+use crate::reduction;
+use crate::rules::ReductionError;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+use crate::topology::{Graph, SimpleGraph};
+use crate::types::One;
+
+type Source = MaxCut<SimpleGraph, One>;
+
+/// Result of reducing unit-weight MaxCut to Maximum2Satisfiability.
+#[derive(Debug, Clone)]
+pub struct ReductionMaxCutToMaximum2Satisfiability {
+    target: Maximum2Satisfiability,
+}
+
+impl ReductionResult for ReductionMaxCutToMaximum2Satisfiability {
+    type Source = Source;
+    type Target = Maximum2Satisfiability;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    /// Solution extraction: variable `x_v` is the side of vertex `v`.
+    fn extract_solution(
+        &self,
+        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
+    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
+        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
+
+        Ok(target_solution.clone())
+    }
+}
+
+/// The positive CNF literal `v + 1` of vertex `v`.
+fn vertex_literal(vertex: usize) -> Result<i64, ReductionError> {
+    vertex
+        .checked_add(1)
+        .and_then(|literal| i64::try_from(literal).ok())
+        .ok_or_else(|| {
+            ReductionError::integer_overflow::<Source, Maximum2Satisfiability>(
+                "encoding a vertex as a CNF literal",
+            )
+        })
+}
+
+/// The number of target clauses, two per edge.
+fn clause_count(num_edges: usize) -> Result<usize, ReductionError> {
+    num_edges.checked_mul(2).ok_or_else(|| {
+        ReductionError::integer_overflow::<Source, Maximum2Satisfiability>(
+            "counting two clauses per edge",
+        )
+    })
+}
+
+#[reduction(
+    transform = exact {
+        num_vars = "num_vertices",
+        num_clauses = "2 * num_edges",
+    }
+)]
+impl ReduceTo<Maximum2Satisfiability> for MaxCut<SimpleGraph, One> {
+    type Result = ReductionMaxCutToMaximum2Satisfiability;
+
+    fn reduce_to(&self) -> Result<Self::Result, ReductionError> {
+        let edges = self.graph().edges();
+        let mut clauses = Vec::with_capacity(clause_count(edges.len())?);
+        for (u, v) in edges {
+            let (lu, lv) = (vertex_literal(u)?, vertex_literal(v)?);
+            clauses.push(CNFClause::new(vec![lu, lv]));
+            clauses.push(CNFClause::new(vec![-lu, -lv]));
+        }
+        let target = Maximum2Satisfiability::try_new(self.num_vertices(), clauses)
+            .map_err(<Self as ReduceTo<Maximum2Satisfiability>>::target_construction)?;
+        Ok(ReductionMaxCutToMaximum2Satisfiability { target })
+    }
+}
+
+#[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: || {
+            // The 4-cycle 0-1-2-3-0 plus the diagonal {0, 2}.
+            let source = Source::unweighted(SimpleGraph::new(
+                4,
+                vec![(0, 1), (1, 2), (2, 3), (3, 0), (0, 2)],
+            ));
+            crate::example_db::specs::rule_example_with_witness::<_, Maximum2Satisfiability>(
+                source,
+                SolutionPair {
+                    source_config: serde_json::json!(vec![false, true, false, true]),
+                    target_config: serde_json::json!(vec![false, true, false, true]),
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/maxcut_maximum2satisfiability.rs"]
+mod tests;

src/rules/mod.rs

@@ -94,6 +94,7 @@ pub(crate) mod ksatisfiability_timetabledesign;
 pub(crate) mod longestcommonsubsequence_maximumindependentset;
 mod longestpath_casts;
 mod maxcut_casts;
+pub(crate) mod maxcut_maximum2satisfiability;
 pub(crate) mod maxcut_minimumcutintoboundedsets;
 pub(crate) mod maxcut_minimummatrixcover;
 pub(crate) mod maximum2satisfiability_maxcut;
@@ -428,6 +429,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(ksatisfiability_simultaneousincongruences::canonical_rule_example_specs());
     specs.extend(ksatisfiability_subsetsum::canonical_rule_example_specs());
     specs.extend(ksatisfiability_timetabledesign::canonical_rule_example_specs());
+    specs.extend(maxcut_maximum2satisfiability::canonical_rule_example_specs());
     specs.extend(maximum2satisfiability_maxcut::canonical_rule_example_specs());
     specs.extend(maximumclique_maximumindependentset::canonical_rule_example_specs());
     specs.extend(decisionmaximumindependentset_integralflowbundles::canonical_rule_example_specs());