diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 88cd07556..0dbf3006d 100644 --- a/docs/paper/reductions.typ +++ b/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", diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 186f70de2..aa6f11a13 100644 --- a/docs/paper/references.bib +++ b/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}, diff --git a/src/rules/maxcut_maximum2satisfiability.rs b/src/rules/maxcut_maximum2satisfiability.rs new file mode 100644 index 000000000..083750fdc --- /dev/null +++ b/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; + type Target = Maximum2Satisfiability; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution.to_vec() + } +} + +#[reduction( + overhead = { + num_vars = "num_vertices", + num_clauses = "2 * num_edges", + } +)] +impl ReduceTo for MaxCut { + 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 { + 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; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 95eb5f477..58bd1254a 100644 --- a/src/rules/mod.rs +++ b/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 MaxCut { + 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) { + let reduction = ReduceTo::::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 = (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::::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::::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::::new()); + assert_affine_identity(&empty); + + let isolated = MaxCut::new(SimpleGraph::empty(3), Vec::::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::::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::::reduce_to(¶llel); + 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(¶llel); +} + +#[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], + }] + ); +}