From be3b45a19fde6535348365c3692c37377994f350 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:13:53 +0800 Subject: [PATCH 1/5] Add plan for #1102: MaxCut to Maximum2Satisfiability --- ...-08-02-maxcut-to-maximum2satisfiability.md | 85 +++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md diff --git a/docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md b/docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md new file mode 100644 index 000000000..ed01bcf85 --- /dev/null +++ b/docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md @@ -0,0 +1,85 @@ +# MaxCut/One to Maximum2Satisfiability + +Implement issue #1102 as a witness-preserving reduction from +`MaxCut` to `Maximum2Satisfiability`. The branch is stacked on +commit `a9067297`, where the exact source variant is introduced. + +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, DOI `10.1016/S0166-218X(02)00402-X`; open preprint ECCC +TR00-037, Section 5. + +## Batch 1: verify and implement the reduction + +Follow `.agents/skills/add-rule/SKILL.md` Steps 0–5 and 7, using the repository +copy of that skill from the parent checkout when the stacked worktree does not +contain `.agents/`. + +1. Run the full `verify-reduction` workflow before editing Rust code. Verify the + pointwise identity + + `satisfied_clauses(x) = num_edges + cut_edges(x)` + + with a standalone Typst proof, an independent constructor validator, and an + adversary validator. Cover all graphs through five vertices, direct witness + extraction, exact overhead, empty and isolated graphs, self-loops, parallel + edges, the five-edge worked example, and a three-or-more-vertex negative + threshold example. Keep all verification artifacts outside the repository. + +2. Add `src/rules/maxcut_maximum2satisfiability.rs`. Implement + `ReduceTo` specifically for + `MaxCut`. For each edge occurrence `(u, v)`, append + `CNFClause::new(vec![(u + 1) as i32, (v + 1) as i32])` and + `CNFClause::new(vec![-((u + 1) as i32), -((v + 1) as i32)])`. Preserve the + target assignment directly in `extract_solution`. Register exact overhead + `num_vars = num_vertices` and `num_clauses = 2 * num_edges`. + +3. Register the module directly in `src/rules/mod.rs`. Do not add adapters, + alternate variants, or compatibility paths. + +4. Add `src/unit_tests/rules/maxcut_maximum2satisfiability.rs` with focused + semantic tests: + + - `test_maxcut_to_maximum2satisfiability_closed_loop` checks both optima and + every extracted optimum on the four-cycle-plus-diagonal example. + - A structure/pointwise test checks all ten clauses, exact metrics, direct + extraction, and `target_value = 5 + source_value` for every assignment. + - Boundary tests cover empty, isolated, disconnected, self-loop, and + parallel-edge inputs, including repeated literals and repeated clause + pairs. + - An exhaustive small-graph test checks the affine identity and round trip + without introducing a golden fixture. + +5. Add the canonical four-cycle-plus-diagonal example to + `canonical_rule_example_specs()` in the new rule module. Use source config + `[0, 1, 0, 1]` and the identical target config, with source optimum `4` and + target optimum `9`. + +6. Regenerate the reduction graph, schemas, and example fixtures. Run focused + tests, `make test`, `make clippy`, `make fmt-check`, and `make coverage`. + Keep tracked generated data required by the rule; do not commit ignored + exports or temporary verification artifacts. + +## Batch 2: document the rule with fresh context + +After Batch 1 and fixture regeneration, follow `.agents/skills/add-rule/SKILL.md` +Step 6. + +1. Add the BibTeX entry for Gramm et al. if it is not already present. +2. Add a `MaxCut` to `Maximum2Satisfiability` `reduction-rule` entry in + `docs/paper/reductions.typ`, loading the canonical rule fixture and deriving + the source-side `pred create --example` command from the loaded variant. +3. State the construction, prove both directions independently via the + per-edge truth table, state direct witness extraction, and explain why loops + and parallel edges preserve the identity. +4. Include a tutorial-style walkthrough of the four-cycle-plus-diagonal + fixture: five edges, ten clauses, cut witness `[0,1,0,1]`, cut value `4`, and + target value `9`. State that the fixture stores one canonical optimum. +5. Run `make paper`, then rerun formatting, linting, tests, and coverage after + all documentation and fixture changes. + +## Completion + +Commit the implementation and documentation in coherent commits, remove this +plan file, post a PR implementation summary including any deviations, push the +stacked branch, and leave the issue ready for the review pipeline. From 379b795405dc748e8d8113b23ff090921b355d64 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:27:35 +0800 Subject: [PATCH 2/5] Implement #1102: MaxCut to Maximum2Satisfiability --- src/rules/maxcut_maximum2satisfiability.rs | 80 +++++++++ src/rules/mod.rs | 2 + .../rules/maxcut_maximum2satisfiability.rs | 156 ++++++++++++++++++ 3 files changed, 238 insertions(+) create mode 100644 src/rules/maxcut_maximum2satisfiability.rs create mode 100644 src/unit_tests/rules/maxcut_maximum2satisfiability.rs diff --git a/src/rules/maxcut_maximum2satisfiability.rs b/src/rules/maxcut_maximum2satisfiability.rs new file mode 100644 index 000000000..76743d614 --- /dev/null +++ b/src/rules/maxcut_maximum2satisfiability.rs @@ -0,0 +1,80 @@ +//! 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, +} + +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 = (u + 1) as i32; + let v = (v + 1) as i32; + [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] +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], + }] + ); +} From d004a5139e2cc538a0dee706c2b90781420bf3a8 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:49:18 +0800 Subject: [PATCH 3/5] Document MaxCut to Maximum2Satisfiability --- docs/paper/reductions.typ | 81 +++++++++++++++++++++++++++++++++++++++ docs/paper/references.bib | 11 ++++++ 2 files changed, 92 insertions(+) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 88cd07556..d5cd3c043 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) + " -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}, From 56f7d30474e5a7baf3ea63737b95e580c5940be5 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 14:49:27 +0800 Subject: [PATCH 4/5] chore: remove plan file after implementation --- ...-08-02-maxcut-to-maximum2satisfiability.md | 85 ------------------- 1 file changed, 85 deletions(-) delete mode 100644 docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md diff --git a/docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md b/docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md deleted file mode 100644 index ed01bcf85..000000000 --- a/docs/plans/2026-08-02-maxcut-to-maximum2satisfiability.md +++ /dev/null @@ -1,85 +0,0 @@ -# MaxCut/One to Maximum2Satisfiability - -Implement issue #1102 as a witness-preserving reduction from -`MaxCut` to `Maximum2Satisfiability`. The branch is stacked on -commit `a9067297`, where the exact source variant is introduced. - -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, DOI `10.1016/S0166-218X(02)00402-X`; open preprint ECCC -TR00-037, Section 5. - -## Batch 1: verify and implement the reduction - -Follow `.agents/skills/add-rule/SKILL.md` Steps 0–5 and 7, using the repository -copy of that skill from the parent checkout when the stacked worktree does not -contain `.agents/`. - -1. Run the full `verify-reduction` workflow before editing Rust code. Verify the - pointwise identity - - `satisfied_clauses(x) = num_edges + cut_edges(x)` - - with a standalone Typst proof, an independent constructor validator, and an - adversary validator. Cover all graphs through five vertices, direct witness - extraction, exact overhead, empty and isolated graphs, self-loops, parallel - edges, the five-edge worked example, and a three-or-more-vertex negative - threshold example. Keep all verification artifacts outside the repository. - -2. Add `src/rules/maxcut_maximum2satisfiability.rs`. Implement - `ReduceTo` specifically for - `MaxCut`. For each edge occurrence `(u, v)`, append - `CNFClause::new(vec![(u + 1) as i32, (v + 1) as i32])` and - `CNFClause::new(vec![-((u + 1) as i32), -((v + 1) as i32)])`. Preserve the - target assignment directly in `extract_solution`. Register exact overhead - `num_vars = num_vertices` and `num_clauses = 2 * num_edges`. - -3. Register the module directly in `src/rules/mod.rs`. Do not add adapters, - alternate variants, or compatibility paths. - -4. Add `src/unit_tests/rules/maxcut_maximum2satisfiability.rs` with focused - semantic tests: - - - `test_maxcut_to_maximum2satisfiability_closed_loop` checks both optima and - every extracted optimum on the four-cycle-plus-diagonal example. - - A structure/pointwise test checks all ten clauses, exact metrics, direct - extraction, and `target_value = 5 + source_value` for every assignment. - - Boundary tests cover empty, isolated, disconnected, self-loop, and - parallel-edge inputs, including repeated literals and repeated clause - pairs. - - An exhaustive small-graph test checks the affine identity and round trip - without introducing a golden fixture. - -5. Add the canonical four-cycle-plus-diagonal example to - `canonical_rule_example_specs()` in the new rule module. Use source config - `[0, 1, 0, 1]` and the identical target config, with source optimum `4` and - target optimum `9`. - -6. Regenerate the reduction graph, schemas, and example fixtures. Run focused - tests, `make test`, `make clippy`, `make fmt-check`, and `make coverage`. - Keep tracked generated data required by the rule; do not commit ignored - exports or temporary verification artifacts. - -## Batch 2: document the rule with fresh context - -After Batch 1 and fixture regeneration, follow `.agents/skills/add-rule/SKILL.md` -Step 6. - -1. Add the BibTeX entry for Gramm et al. if it is not already present. -2. Add a `MaxCut` to `Maximum2Satisfiability` `reduction-rule` entry in - `docs/paper/reductions.typ`, loading the canonical rule fixture and deriving - the source-side `pred create --example` command from the loaded variant. -3. State the construction, prove both directions independently via the - per-edge truth table, state direct witness extraction, and explain why loops - and parallel edges preserve the identity. -4. Include a tutorial-style walkthrough of the four-cycle-plus-diagonal - fixture: five edges, ten clauses, cut witness `[0,1,0,1]`, cut value `4`, and - target value `9`. State that the fixture stores one canonical optimum. -5. Run `make paper`, then rerun formatting, linting, tests, and coverage after - all documentation and fixture changes. - -## Completion - -Commit the implementation and documentation in coherent commits, remove this -plan file, post a PR implementation summary including any deviations, push the -stacked branch, and leave the issue ready for the review pipeline. From d679590f047cc7aa7868f3477655ab919109541c Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 15:28:37 +0800 Subject: [PATCH 5/5] fix: address PR #1111 review comments - reject vertex indices outside the signed CNF literal range\n- make the paper command select the canonical rule fixture --- docs/paper/reductions.typ | 2 +- src/rules/maxcut_maximum2satisfiability.rs | 9 +++++++-- src/unit_tests/rules/maxcut_maximum2satisfiability.rs | 6 ++++++ 3 files changed, 14 insertions(+), 3 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index d5cd3c043..0dbf3006d 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -11453,7 +11453,7 @@ Each reduction is presented as a *Rule* (with linked problem names and overhead 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) + " -o maxcut.json", + "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(","), diff --git a/src/rules/maxcut_maximum2satisfiability.rs b/src/rules/maxcut_maximum2satisfiability.rs index 76743d614..083750fdc 100644 --- a/src/rules/maxcut_maximum2satisfiability.rs +++ b/src/rules/maxcut_maximum2satisfiability.rs @@ -13,6 +13,11 @@ 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; @@ -41,8 +46,8 @@ impl ReduceTo for MaxCut { .edges() .into_iter() .flat_map(|(u, v)| { - let u = (u + 1) as i32; - let v = (v + 1) as i32; + let u = vertex_literal(u); + let v = vertex_literal(v); [CNFClause::new(vec![u, v]), CNFClause::new(vec![-u, -v])] }) .collect(); diff --git a/src/unit_tests/rules/maxcut_maximum2satisfiability.rs b/src/unit_tests/rules/maxcut_maximum2satisfiability.rs index 0058a88a3..961324033 100644 --- a/src/unit_tests/rules/maxcut_maximum2satisfiability.rs +++ b/src/unit_tests/rules/maxcut_maximum2satisfiability.rs @@ -101,6 +101,12 @@ fn test_maxcut_to_maximum2satisfiability_boundaries() { 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 {