diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 8e0462b7a..d0fc74dc2 100644 --- a/docs/paper/reductions.typ +++ b/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) diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 0dda81fd2..276b9199d 100644 --- a/docs/paper/references.bib +++ b/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} +} diff --git a/src/rules/maxcut_maximum2satisfiability.rs b/src/rules/maxcut_maximum2satisfiability.rs new file mode 100644 index 000000000..3f00c7ef3 --- /dev/null +++ b/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; + +/// 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: &::Solution, + ) -> crate::rules::ExtractionResult<::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 { + vertex + .checked_add(1) + .and_then(|literal| i64::try_from(literal).ok()) + .ok_or_else(|| { + ReductionError::integer_overflow::( + "encoding a vertex as a CNF literal", + ) + }) +} + +/// The number of target clauses, two per edge. +fn clause_count(num_edges: usize) -> Result { + num_edges.checked_mul(2).ok_or_else(|| { + ReductionError::integer_overflow::( + "counting two clauses per edge", + ) + }) +} + +#[reduction( + transform = exact { + num_vars = "num_vertices", + num_clauses = "2 * num_edges", + } +)] +impl ReduceTo for MaxCut { + type Result = ReductionMaxCutToMaximum2Satisfiability; + + fn reduce_to(&self) -> Result { + 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(>::target_construction)?; + Ok(ReductionMaxCutToMaximum2Satisfiability { target }) + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + 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; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 7606f4923..5e63007ce 100644 --- a/src/rules/mod.rs +++ b/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) -> Source { + Source::unweighted(SimpleGraph::new(n, edges)) +} + +fn reduce(source: &Source) -> ReductionMaxCutToMaximum2Satisfiability { + ReduceTo::::reduce_to(source).expect("reduction should succeed") +} + +/// The 4-cycle 0-1-2-3-0 plus the diagonal {0, 2}. +fn issue_example() -> Source { + maxcut(4, vec![(0, 1), (1, 2), (2, 3), (3, 0), (0, 2)]) +} + +fn assignments(n: usize) -> impl Iterator> { + (0..1usize << n).map(move |mask| (0..n).map(|bit| (mask >> bit) & 1 == 1).collect()) +} + +fn value>>(problem: &P, config: &P::Solution) -> i64 { + problem.evaluate(config).unwrap().0.unwrap() +} + +fn optimum

(problem: &P) -> i64 +where + P: Problem> + crate::solvers::BruteForceProblem + 'static, +{ + let best = BruteForce::new().solve(problem).unwrap().unwrap(); + value(problem, &best) +} + +/// `satisfied(x) = m + cut(x)` for every assignment, and extraction is the identity. +fn assert_pointwise_identity(source: &Source) { + let reduction = reduce(source); + let target = reduction.target_problem(); + let m = i64::try_from(source.num_edges()).unwrap(); + for x in assignments(source.num_vertices()) { + assert_eq!(value(target, &x), m + value(source, &x), "assignment {x:?}"); + assert_eq!(reduction.extract_solution(&x).unwrap(), x); + } +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_closed_loop() { + let source = issue_example(); + let reduction = reduce(&source); + assert_optimization_round_trip_from_optimization_target( + &source, + &reduction, + "MaxCut -> Maximum2Satisfiability closed loop", + ); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_structure() { + let source = issue_example(); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 4); + assert_eq!(target.num_clauses(), 10); + let literals: Vec> = target + .clauses() + .iter() + .map(|c| c.literals.clone()) + .collect(); + assert_eq!( + literals, + vec![ + vec![1, 2], + vec![-1, -2], + vec![2, 3], + vec![-2, -3], + vec![3, 4], + vec![-3, -4], + vec![4, 1], + vec![-4, -1], + vec![1, 3], + vec![-1, -3], + ] + ); + assert_parameter_predictions(&source, &reduction); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_issue_example_values() { + let source = issue_example(); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + let witness = vec![false, true, false, true]; + assert_eq!(value(&source, &witness), 4); + assert_eq!(value(target, &witness), 9); + assert_eq!(value(target, &[false; 4].to_vec()), 5); + assert_eq!(value(target, &[true; 4].to_vec()), 5); + assert_eq!(optimum(&source), 4); + assert_eq!(optimum(target), 9); + assert_eq!( + BruteForce::new().find_all_witnesses(target).unwrap().len(), + 2, + "the witness and its complement" + ); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_pointwise_identity_on_all_small_graphs() { + for n in 0..=5usize { + let pairs: Vec<(usize, usize)> = (0..n) + .flat_map(|u| (u + 1..n).map(move |v| (u, v))) + .collect(); + for mask in 0..1usize << pairs.len() { + let edges = (0..pairs.len()) + .filter(|&i| (mask >> i) & 1 == 1) + .map(|i| pairs[i]) + .collect(); + assert_pointwise_identity(&maxcut(n, edges)); + } + } +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_preserves_edge_orientation() { + let source = maxcut(3, vec![(2, 0), (1, 2)]); + let reduction = reduce(&source); + let literals: Vec> = reduction + .target_problem() + .clauses() + .iter() + .map(|c| c.literals.clone()) + .collect(); + assert_eq!( + literals, + vec![vec![3, 1], vec![-3, -1], vec![2, 3], vec![-2, -3]] + ); + assert_pointwise_identity(&source); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_empty_graph() { + let source = maxcut(0, vec![]); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!(target.num_vars(), 0); + assert_eq!(target.num_clauses(), 0); + assert_eq!(value(target, &vec![]), 0); + assert_eq!( + reduction.extract_solution(&vec![]).unwrap(), + Vec::::new() + ); + assert_optimization_round_trip_from_optimization_target(&source, &reduction, "empty graph"); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_edgeless_graph() { + let source = maxcut(3, vec![]); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!(target.num_vars(), 3); + assert_eq!(target.num_clauses(), 0); + for x in assignments(3) { + assert_eq!(value(target, &x), 0); + assert_eq!(value(&source, &x), 0); + } +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_isolated_vertex() { + // Vertex 2 is isolated; the objectives need not be zero. + let source = maxcut(3, vec![(0, 1)]); + let reduction = reduce(&source); + let target = reduction.target_problem(); + assert_eq!(value(&source, &vec![false, true, false]), 1); + assert_eq!(value(target, &vec![false, true, false]), 2); + for x in assignments(3) { + let mut flipped = x.clone(); + flipped[2] = !flipped[2]; + assert_eq!(value(&source, &flipped), value(&source, &x)); + assert_eq!(value(target, &flipped), value(target, &x)); + } + assert_pointwise_identity(&source); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_disconnected_graph() { + let source = maxcut(5, vec![(0, 1), (1, 2), (3, 4)]); + let reduction = reduce(&source); + assert_pointwise_identity(&source); + assert_eq!(optimum(&source), 3); + assert_eq!(optimum(reduction.target_problem()), 6); + assert_optimization_round_trip_from_optimization_target(&source, &reduction, "disconnected"); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_thresholds_unattainable_on_both_sides() { + // Single edge: no cut reaches 2, so no assignment satisfies m + 2 = 3 clauses. + let edge = maxcut(2, vec![(0, 1)]); + let edge_target = reduce(&edge).target_problem().clone(); + assert!(assignments(2).all(|x| value(&edge, &x) < 2)); + assert!(assignments(2).all(|x| value(&edge_target, &x) < 3)); + assert_eq!(optimum(&edge_target), 2); + + // Triangle: no cut reaches 3, so no assignment satisfies m + 3 = 6 clauses. + let triangle = maxcut(3, vec![(0, 1), (1, 2), (0, 2)]); + let triangle_target = reduce(&triangle).target_problem().clone(); + assert!(assignments(3).all(|x| value(&triangle, &x) < 3)); + assert!(assignments(3).all(|x| value(&triangle_target, &x) < 6)); + assert_eq!(optimum(&triangle), 2); + assert_eq!(optimum(&triangle_target), 5); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_source_rejects_loops_and_parallel_edges() { + assert!(SimpleGraph::try_new(2, vec![(1, 1)]).is_err()); + assert!(SimpleGraph::try_new(2, vec![(0, 1), (1, 0)]).is_err()); + assert!(SimpleGraph::try_new(2, vec![(0, 1), (0, 1)]).is_err()); + let looped = serde_json::json!({ + "graph": {"num_vertices": 2, "edges": [[1, 1]]}, + "edge_weights": [1], + }); + assert!(serde_json::from_value::(looped).is_err()); + let parallel = serde_json::json!({ + "graph": {"num_vertices": 2, "edges": [[0, 1], [1, 0]]}, + "edge_weights": [1, 1], + }); + assert!(serde_json::from_value::(parallel).is_err()); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_extraction_rejects_wrong_lengths() { + let reduction = reduce(&issue_example()); + assert!(reduction.extract_solution(&vec![false; 3]).is_err()); + assert!(reduction.extract_solution(&vec![false; 5]).is_err()); + assert!(reduction.extract_solution(&vec![]).is_err()); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_literal_boundary() { + let largest = usize::try_from(i64::MAX).unwrap(); + assert_eq!(vertex_literal(0).unwrap(), 1); + assert_eq!(vertex_literal(largest - 1).unwrap(), i64::MAX); + assert!(matches!( + vertex_literal(largest), + Err(ReductionError::IntegerOverflow { .. }) + )); + assert!(matches!( + vertex_literal(usize::MAX), + Err(ReductionError::IntegerOverflow { .. }) + )); +} + +#[test] +fn test_maxcut_to_maximum2satisfiability_clause_count_boundary() { + let half = usize::MAX / 2; + assert_eq!(clause_count(0).unwrap(), 0); + assert_eq!(clause_count(half).unwrap(), usize::MAX - 1); + assert!(matches!( + clause_count(half + 1), + Err(ReductionError::IntegerOverflow { .. }) + )); +}