From b001ceb5665a378d31bf9e6b7790d9a5fcf2c630 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Fri, 20 Mar 2026 12:48:49 +0800 Subject: [PATCH 1/8] Add plan for #118: [Rule] GraphPartitioning to ILP --- .../2026-03-20-graphpartitioning-to-ilp.md | 210 ++++++++++++++++++ 1 file changed, 210 insertions(+) create mode 100644 docs/plans/2026-03-20-graphpartitioning-to-ilp.md diff --git a/docs/plans/2026-03-20-graphpartitioning-to-ilp.md b/docs/plans/2026-03-20-graphpartitioning-to-ilp.md new file mode 100644 index 000000000..fa944e42d --- /dev/null +++ b/docs/plans/2026-03-20-graphpartitioning-to-ilp.md @@ -0,0 +1,210 @@ +# GraphPartitioning to ILP Implementation Plan + +> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. + +**Goal:** Add a `GraphPartitioning -> ILP` reduction with closed-loop tests, canonical example data, and paper documentation for issue #118. + +**Architecture:** Implement a binary ILP reduction with one partition variable `x_v` per vertex and one crossing-indicator variable `y_e` per edge. Preserve GraphPartitioning's "odd number of vertices is invalid" semantics by encoding the balance equation as `sum x_v = n / 2` over reals, so odd `n` becomes infeasible automatically because the RHS is fractional. + +**Tech Stack:** Rust workspace, reduction registry macros, `good_lp`-backed ILP model, example-db exports, Typst paper. + +--- + +## Batch 1: Rule implementation and tests + +Aligned with `add-rule` Steps 1-4 and Step 6's code-side exports. + +### Task 1: Write failing rule tests first + +**Files:** +- Create: `src/unit_tests/rules/graphpartitioning_ilp.rs` +- Read for patterns: `src/unit_tests/rules/minimummultiwaycut_ilp.rs` +- Read for patterns: `src/unit_tests/rules/maximumclique_ilp.rs` + +**Step 1: Write the failing tests** + +Add focused tests for: +- ILP structure on the canonical 6-vertex example: `num_vars = n + m = 15`, `num_constraints = 2m + 1 = 19`, objective sense is minimize, objective coefficients are attached only to edge variables. +- Constraint shape on a tiny graph: balance equality plus two `>=` linking constraints per edge. +- Closed-loop solving on the canonical example: brute-force `GraphPartitioning` optimum is 3 and the ILP solution extracts to the same optimum. +- Odd-vertex behavior: a 3-vertex graph reduces to an infeasible ILP, so `ILPSolver::solve` returns `None`. +- Solution extraction: a hand-written ILP witness maps back to the expected partition config. +- `solve_reduced` path works end-to-end. + +**Step 2: Run the new test target and verify it fails** + +Run: +```bash +cargo test --features "ilp-highs example-db" graphpartitioning_ilp -- --include-ignored +``` + +Expected: compile failure because the rule module does not exist yet. + +### Task 2: Implement the reduction rule + +**Files:** +- Create: `src/rules/graphpartitioning_ilp.rs` +- Modify: `src/rules/mod.rs` +- Read for patterns: `src/models/graph/graph_partitioning.rs` +- Read for patterns: `src/models/algebraic/ilp.rs` + +**Step 1: Write the minimal implementation** + +Implement: +- `ReductionGraphPartitioningToILP { target: ILP, num_vertices: usize }` +- `ReductionResult` impl returning the target ILP and extracting the first `n` variables as the source partition assignment. +- `ReduceTo> for GraphPartitioning` with: + - variable layout: vertex variables first, then edge variables in source edge order + - balance equality `sum_v x_v = n as f64 / 2.0` + - two linking constraints per edge: + - `y_e - x_u + x_v >= 0` + - `y_e + x_u - x_v >= 0` + - objective `min sum_e y_e` + - overhead: + - `num_vars = "num_vertices + num_edges"` + - `num_constraints = "2 * num_edges + 1"` +- `#[cfg(feature = "example-db")] canonical_rule_example_specs()` with the issue's 6-vertex graph and a canonical witness: + - source config: `[0, 0, 0, 1, 1, 1]` + - target config: `[0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0]` +- Feature-gated registration in `src/rules/mod.rs` and inclusion in `canonical_rule_example_specs()`. + +**Step 2: Run the focused tests and verify they pass** + +Run: +```bash +cargo test --features "ilp-highs example-db" graphpartitioning_ilp -- --include-ignored +``` + +Expected: all `graphpartitioning_ilp` tests pass. + +**Step 3: Refactor only if needed** + +Keep only cleanup that preserves behavior: +- small helper for balance constraint construction +- comment documenting the variable ordering used by `extract_solution` + +### Task 3: Verify registry and example-db wiring + +**Files:** +- Modify: `src/rules/mod.rs` +- Read for patterns: `src/rules/minimummultiwaycut_ilp.rs` + +**Step 1: Run export commands that depend on rule registration** + +Run: +```bash +cargo run --example export_graph +cargo run --example export_schemas +cargo run --features "example-db" --example export_examples +``` + +Expected: +- `export_graph` includes a `GraphPartitioning -> ILP` edge. +- `export_examples` completes and writes `src/example_db/fixtures/examples.json`. + +**Step 2: If export output reveals missing wiring, fix only the missing registration and rerun the failing command** + +### Task 4: Run broader code verification for the implementation batch + +**Files:** +- No new files unless a verification failure requires a minimal follow-up fix + +**Step 1: Run the relevant batch verification** + +Run: +```bash +cargo test --features "ilp-highs example-db" graphpartitioning_ilp graph_partitioning -- --include-ignored +cargo clippy --all-targets --features ilp-highs -- -D warnings +``` + +Expected: tests pass and clippy reports no warnings. + +**Step 2: Commit the implementation batch** + +Run: +```bash +git add src/rules/graphpartitioning_ilp.rs src/rules/mod.rs src/unit_tests/rules/graphpartitioning_ilp.rs +git commit -m "Add GraphPartitioning to ILP reduction" +``` + +## Batch 2: Paper entry and fixture-backed documentation + +Aligned with `add-rule` Step 5. + +### Task 5: Add the paper reduction entry + +**Files:** +- Modify: `docs/paper/reductions.typ` +- Read for patterns: nearby `GraphPartitioning` problem definition +- Read for patterns: `#reduction-rule("MinimumMultiwayCut", "ILP")` +- Read for patterns: `#reduction-rule("TravelingSalesman", "ILP", example: true, ...)` + +**Step 1: Write the fixture-backed reduction-rule entry** + +Add a `GraphPartitioning -> ILP` theorem near the other ILP reductions that includes: +- theorem body summarizing the vertex/edge-indicator formulation and the `n + m` / `2m + 1` size +- proof body sections for construction, correctness, and solution extraction +- an `example: true` walkthrough backed by `load-rule-example("GraphPartitioning", "ILP")` +- explicit note that odd `n` produces an infeasible balance equality because `n / 2` is fractional + +The example should read the exported witness data rather than hardcoding a second copy of the solution. + +**Step 2: Build the paper and verify it passes** + +Run: +```bash +make paper +``` + +Expected: Typst builds successfully and the new reduction entry resolves its example data. + +### Task 6: Final verification for the branch state + +**Files:** +- Any generated tracked outputs from the export and paper build steps + +**Step 1: Run final verification commands** + +Run: +```bash +cargo test --features "ilp-highs example-db" graphpartitioning_ilp graph_partitioning -- --include-ignored +cargo clippy --all-targets --features ilp-highs -- -D warnings +make paper +git status --short +``` + +Expected: +- tests pass +- clippy passes +- paper builds +- `git status --short` shows only intended tracked changes plus ignored/generated files under ignored export paths + +**Step 2: Commit the documentation/export batch** + +Run: +```bash +git add docs/paper/reductions.typ src/example_db/fixtures/examples.json docs/paper/reductions.pdf docs/paper/graph.json docs/src/schema/problem_schemas.json +git commit -m "Document GraphPartitioning to ILP reduction" +``` + +If generated tracked file paths differ, stage the actual tracked outputs reported by `git status --short` instead of forcing this exact list. + +### Task 7: Remove the plan file after implementation + +**Files:** +- Delete: `docs/plans/2026-03-20-graphpartitioning-to-ilp.md` + +**Step 1: Remove the temporary plan artifact** + +Run: +```bash +git rm docs/plans/2026-03-20-graphpartitioning-to-ilp.md +git commit -m "chore: remove plan file after implementation" +``` + +## Notes for the executor + +- Stay inside the issue worktree branch `issue-118`. +- Do not touch the user's main checkout. +- Do not "fix" unrelated changes in the parent repository. +- Keep the implementation scoped to this one rule; do not add model changes. From 7eeeef81aec821e9258315c8f5712794d54718b3 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Fri, 20 Mar 2026 12:55:23 +0800 Subject: [PATCH 2/8] Add GraphPartitioning to ILP reduction --- src/rules/graphpartitioning_ilp.rs | 114 +++++++++++++++ src/rules/mod.rs | 3 + src/unit_tests/rules/graphpartitioning_ilp.rs | 132 ++++++++++++++++++ 3 files changed, 249 insertions(+) create mode 100644 src/rules/graphpartitioning_ilp.rs create mode 100644 src/unit_tests/rules/graphpartitioning_ilp.rs diff --git a/src/rules/graphpartitioning_ilp.rs b/src/rules/graphpartitioning_ilp.rs new file mode 100644 index 000000000..4d20d0f7d --- /dev/null +++ b/src/rules/graphpartitioning_ilp.rs @@ -0,0 +1,114 @@ +//! Reduction from GraphPartitioning to ILP (Integer Linear Programming). +//! +//! Uses the standard balanced-cut ILP formulation: +//! - Variables: `x_v` for vertex-side assignment and `y_e` for edge-crossing indicators +//! - Constraints: one balance equality plus two linking inequalities per edge +//! - Objective: minimize the number of crossing edges + +use crate::models::algebraic::{ILP, LinearConstraint, ObjectiveSense}; +use crate::models::graph::GraphPartitioning; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing GraphPartitioning to ILP. +/// +/// Variable layout (all binary): +/// - `x_v` for `v = 0..n-1`: vertex `v` belongs to side `B` +/// - `y_e` for `e = 0..m-1`: edge `e` crosses the partition +#[derive(Debug, Clone)] +pub struct ReductionGraphPartitioningToILP { + target: ILP, + num_vertices: usize, +} + +impl ReductionResult for ReductionGraphPartitioningToILP { + type Source = GraphPartitioning; + type Target = ILP; + + fn target_problem(&self) -> &ILP { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + target_solution[..self.num_vertices].to_vec() + } +} + +#[reduction( + overhead = { + num_vars = "num_vertices + num_edges", + num_constraints = "2 * num_edges + 1", + } +)] +impl ReduceTo> for GraphPartitioning { + type Result = ReductionGraphPartitioningToILP; + + fn reduce_to(&self) -> Self::Result { + let n = self.num_vertices(); + let edges = self.graph().edges(); + let m = edges.len(); + let num_vars = n + m; + + let mut constraints = Vec::with_capacity(2 * m + 1); + + let balance_terms: Vec<(usize, f64)> = (0..n).map(|v| (v, 1.0)).collect(); + constraints.push(LinearConstraint::eq(balance_terms, n as f64 / 2.0)); + + for (edge_idx, (u, v)) in edges.iter().enumerate() { + let y_var = n + edge_idx; + constraints.push(LinearConstraint::ge( + vec![(y_var, 1.0), (*u, -1.0), (*v, 1.0)], + 0.0, + )); + constraints.push(LinearConstraint::ge( + vec![(y_var, 1.0), (*u, 1.0), (*v, -1.0)], + 0.0, + )); + } + + let objective: Vec<(usize, f64)> = (0..m).map(|edge_idx| (n + edge_idx, 1.0)).collect(); + let target = ILP::new(num_vars, constraints, objective, ObjectiveSense::Minimize); + + ReductionGraphPartitioningToILP { + target, + num_vertices: n, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "graphpartitioning_to_ilp", + build: || { + let source = GraphPartitioning::new(SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + )); + crate::example_db::specs::rule_example_with_witness::<_, ILP>( + source, + SolutionPair { + source_config: vec![0, 0, 0, 1, 1, 1], + target_config: vec![0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/graphpartitioning_ilp.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 4740bd9bd..31521ece6 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -51,6 +51,8 @@ pub(crate) mod coloring_ilp; #[cfg(feature = "ilp-solver")] pub(crate) mod factoring_ilp; #[cfg(feature = "ilp-solver")] +pub(crate) mod graphpartitioning_ilp; +#[cfg(feature = "ilp-solver")] mod ilp_bool_ilp_i32; #[cfg(feature = "ilp-solver")] pub(crate) mod ilp_qubo; @@ -112,6 +114,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec GraphPartitioning { + let graph = SimpleGraph::new( + 6, + vec![ + (0, 1), + (0, 2), + (1, 2), + (1, 3), + (2, 3), + (2, 4), + (3, 4), + (3, 5), + (4, 5), + ], + ); + GraphPartitioning::new(graph) +} + +#[test] +fn test_reduction_creates_valid_ilp() { + let problem = canonical_instance(); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 15); + assert_eq!(ilp.constraints.len(), 19); + assert_eq!(ilp.sense, ObjectiveSense::Minimize); + assert_eq!( + ilp.objective, + vec![ + (6, 1.0), + (7, 1.0), + (8, 1.0), + (9, 1.0), + (10, 1.0), + (11, 1.0), + (12, 1.0), + (13, 1.0), + (14, 1.0), + ] + ); +} + +#[test] +fn test_reduction_constraint_shape() { + let problem = GraphPartitioning::new(SimpleGraph::new(2, vec![(0, 1)])); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.num_vars, 3); + assert_eq!(ilp.constraints.len(), 3); + + let balance = &ilp.constraints[0]; + assert_eq!(balance.cmp, Comparison::Eq); + assert_eq!(balance.terms, vec![(0, 1.0), (1, 1.0)]); + assert_eq!(balance.rhs, 1.0); + + let first_link = &ilp.constraints[1]; + assert_eq!(first_link.cmp, Comparison::Ge); + assert_eq!(first_link.terms, vec![(2, 1.0), (0, -1.0), (1, 1.0)]); + assert_eq!(first_link.rhs, 0.0); + + let second_link = &ilp.constraints[2]; + assert_eq!(second_link.cmp, Comparison::Ge); + assert_eq!(second_link.terms, vec![(2, 1.0), (0, 1.0), (1, -1.0)]); + assert_eq!(second_link.rhs, 0.0); +} + +#[test] +fn test_graphpartitioning_to_ilp_closed_loop() { + let problem = canonical_instance(); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + let bf = BruteForce::new(); + let ilp_solver = ILPSolver::new(); + + let bf_solutions = bf.find_all_best(&problem); + let bf_obj = problem.evaluate(&bf_solutions[0]); + + let ilp_solution = ilp_solver.solve(ilp).expect("ILP should be solvable"); + let extracted = reduction.extract_solution(&ilp_solution); + let ilp_obj = problem.evaluate(&extracted); + + assert_eq!(bf_obj, SolutionSize::Valid(3)); + assert_eq!(ilp_obj, SolutionSize::Valid(3)); +} + +#[test] +fn test_odd_vertices_reduce_to_infeasible_ilp() { + let problem = GraphPartitioning::new(SimpleGraph::new(3, vec![(0, 1), (1, 2)])); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + let ilp = reduction.target_problem(); + + assert_eq!(ilp.constraints[0].cmp, Comparison::Eq); + assert_eq!(ilp.constraints[0].rhs, 1.5); + + let solver = ILPSolver::new(); + assert_eq!(solver.solve(ilp), None); +} + +#[test] +fn test_solution_extraction() { + let problem = canonical_instance(); + let reduction: ReductionGraphPartitioningToILP = ReduceTo::>::reduce_to(&problem); + + let ilp_solution = vec![0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0]; + let extracted = reduction.extract_solution(&ilp_solution); + + assert_eq!(extracted, vec![0, 0, 0, 1, 1, 1]); + assert_eq!(problem.evaluate(&extracted), SolutionSize::Valid(3)); +} + +#[test] +fn test_solve_reduced() { + let problem = canonical_instance(); + + let ilp_solver = ILPSolver::new(); + let solution = ilp_solver + .solve_reduced(&problem) + .expect("solve_reduced should work"); + + assert_eq!(problem.evaluate(&solution), SolutionSize::Valid(3)); +} From 7989d0a91c718a83ae031c10266e1a8eeb7cfd04 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Fri, 20 Mar 2026 12:58:08 +0800 Subject: [PATCH 3/8] Document GraphPartitioning to ILP reduction --- docs/paper/reductions.typ | 35 +++++++++++++++++++++++++++++++++++ docs/paper/references.bib | 11 +++++++++++ 2 files changed, 46 insertions(+) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 09da8adb3..1a75b1914 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -4636,6 +4636,41 @@ The following reductions to Integer Linear Programming are straightforward formu _Solution extraction._ $K = {v : x_v = 1}$. ] +#let gp_ilp = load-example("GraphPartitioning", "ILP") +#let gp_ilp_sol = gp_ilp.solutions.at(0) +#let gp_n = graph-num-vertices(gp_ilp.source.instance) +#let gp_edges = gp_ilp.source.instance.graph.edges +#let gp_m = gp_edges.len() +#let gp_part_a = range(gp_n).filter(i => gp_ilp_sol.source_config.at(i) == 0) +#let gp_part_b = range(gp_n).filter(i => gp_ilp_sol.source_config.at(i) == 1) +#let gp_crossing = range(gp_m).filter(i => gp_ilp_sol.target_config.at(gp_n + i) == 1) +#let gp_crossing_edges = gp_crossing.map(i => gp_edges.at(i)) +#reduction-rule("GraphPartitioning", "ILP", + example: true, + example-caption: [Two triangles linked by three crossing edges encoded as a 15-variable ILP.], + extra: [ + *Step 1 -- Balanced partition variables.* Introduce $x_v in {0,1}$ for each vertex. In the canonical witness, $A = {#gp_part_a.map(str).join(", ")}$ and $B = {#gp_part_b.map(str).join(", ")}$, so $bold(x) = (#gp_ilp_sol.source_config.map(str).join(", "))$.\ + + *Step 2 -- Crossing indicators.* Add one binary variable per edge, so the target has $#gp_ilp.target.instance.num_vars$ binary variables and #gp_ilp.target.instance.constraints.len() constraints in total. The three active crossing indicators correspond to edges $\{#gp_crossing_edges.map(e => "(" + str(e.at(0)) + "," + str(e.at(1)) + ")").join(", ")\}$.\ + + *Step 3 -- Verify the objective.* The target witness $bold(z) = (#gp_ilp_sol.target_config.map(str).join(", "))$ sets exactly #gp_crossing.len() edge-indicator variables to 1, so the ILP objective equals the bisection width #gp_crossing.len() #sym.checkmark + ], +)[ + The node-and-edge integer-programming formulation of Chopra and Rao @chopra1993 models a balanced cut with one binary variable per vertex and one binary crossing indicator per edge. A single balance equality enforces the bisection, and two linear inequalities per edge linearize $|x_u - x_v|$ so that the objective can minimize the number of crossing edges directly. +][ + _Construction._ Given graph $G = (V, E)$ with $n = |V|$ and $m = |E|$: + + _Variables._ Binary $x_v in {0, 1}$ for each $v in V$, where $x_v = 1$ means vertex $v$ is placed in side $B$. For each edge $e = (u, v) in E$, binary $y_e in {0, 1}$ indicates whether $e$ crosses the partition. Total: $n + m$ variables. + + _Constraints._ (1) Balance: $sum_(v in V) x_v = n / 2$. If $n$ is odd, the right-hand side is fractional, so the ILP is infeasible exactly when Graph Partitioning has no valid balanced partition. (2) For each edge $e = (u, v)$: $y_e >= x_u - x_v$ and $y_e >= x_v - x_u$. Since $y_e$ is binary and the objective minimizes $sum_e y_e$, these inequalities force $y_e = 1$ exactly for crossing edges. Total: $2m + 1$ constraints. + + _Objective._ Minimize $sum_(e in E) y_e$. + + _Correctness._ ($arrow.r.double$) Given a balanced partition $(A, B)$, set $x_v = 1$ iff $v in B$, and set $y_e = 1$ iff edge $e$ has one endpoint in each side. The balance constraint holds because $|B| = n / 2$, and the linking inequalities hold because $|x_u - x_v| = 1$ exactly on crossing edges. The objective is therefore the cut size. ($arrow.l.double$) Any feasible ILP solution satisfies the balance equation, so exactly half the vertices have $x_v = 1$ when $n$ is even. For each edge, the linking inequalities imply $y_e >= |x_u - x_v|$; minimization therefore chooses $y_e = |x_u - x_v|$, making the objective count precisely the crossing edges of the extracted partition. + + _Solution extraction._ Return the first $n$ variables $(x_v)_(v in V)$ as the Graph Partitioning configuration; the edge-indicator variables are auxiliary. +] + #reduction-rule("MaximumClique", "MaximumIndependentSet", example: true, example-caption: [Path graph $P_4$: clique in $G$ maps to independent set in complement $overline(G)$.], diff --git a/docs/paper/references.bib b/docs/paper/references.bib index a4f203221..58c456e43 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -991,6 +991,17 @@ @article{chopra1996 doi = {10.1007/BF02592096} } +@article{chopra1993, + author = {Sunil Chopra and M. R. Rao}, + title = {The partition problem}, + journal = {Mathematical Programming}, + volume = {59}, + number = {1--3}, + pages = {87--115}, + year = {1993}, + doi = {10.1007/BF01581239} +} + @article{kou1977, author = {Lawrence T. Kou}, title = {Polynomial Complete Consecutive Information Retrieval Problems}, From 2e92656ce8cf96723d56d746574cf961f5851033 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Fri, 20 Mar 2026 12:58:17 +0800 Subject: [PATCH 4/8] chore: remove plan file after implementation --- .../2026-03-20-graphpartitioning-to-ilp.md | 210 ------------------ 1 file changed, 210 deletions(-) delete mode 100644 docs/plans/2026-03-20-graphpartitioning-to-ilp.md diff --git a/docs/plans/2026-03-20-graphpartitioning-to-ilp.md b/docs/plans/2026-03-20-graphpartitioning-to-ilp.md deleted file mode 100644 index fa944e42d..000000000 --- a/docs/plans/2026-03-20-graphpartitioning-to-ilp.md +++ /dev/null @@ -1,210 +0,0 @@ -# GraphPartitioning to ILP Implementation Plan - -> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. - -**Goal:** Add a `GraphPartitioning -> ILP` reduction with closed-loop tests, canonical example data, and paper documentation for issue #118. - -**Architecture:** Implement a binary ILP reduction with one partition variable `x_v` per vertex and one crossing-indicator variable `y_e` per edge. Preserve GraphPartitioning's "odd number of vertices is invalid" semantics by encoding the balance equation as `sum x_v = n / 2` over reals, so odd `n` becomes infeasible automatically because the RHS is fractional. - -**Tech Stack:** Rust workspace, reduction registry macros, `good_lp`-backed ILP model, example-db exports, Typst paper. - ---- - -## Batch 1: Rule implementation and tests - -Aligned with `add-rule` Steps 1-4 and Step 6's code-side exports. - -### Task 1: Write failing rule tests first - -**Files:** -- Create: `src/unit_tests/rules/graphpartitioning_ilp.rs` -- Read for patterns: `src/unit_tests/rules/minimummultiwaycut_ilp.rs` -- Read for patterns: `src/unit_tests/rules/maximumclique_ilp.rs` - -**Step 1: Write the failing tests** - -Add focused tests for: -- ILP structure on the canonical 6-vertex example: `num_vars = n + m = 15`, `num_constraints = 2m + 1 = 19`, objective sense is minimize, objective coefficients are attached only to edge variables. -- Constraint shape on a tiny graph: balance equality plus two `>=` linking constraints per edge. -- Closed-loop solving on the canonical example: brute-force `GraphPartitioning` optimum is 3 and the ILP solution extracts to the same optimum. -- Odd-vertex behavior: a 3-vertex graph reduces to an infeasible ILP, so `ILPSolver::solve` returns `None`. -- Solution extraction: a hand-written ILP witness maps back to the expected partition config. -- `solve_reduced` path works end-to-end. - -**Step 2: Run the new test target and verify it fails** - -Run: -```bash -cargo test --features "ilp-highs example-db" graphpartitioning_ilp -- --include-ignored -``` - -Expected: compile failure because the rule module does not exist yet. - -### Task 2: Implement the reduction rule - -**Files:** -- Create: `src/rules/graphpartitioning_ilp.rs` -- Modify: `src/rules/mod.rs` -- Read for patterns: `src/models/graph/graph_partitioning.rs` -- Read for patterns: `src/models/algebraic/ilp.rs` - -**Step 1: Write the minimal implementation** - -Implement: -- `ReductionGraphPartitioningToILP { target: ILP, num_vertices: usize }` -- `ReductionResult` impl returning the target ILP and extracting the first `n` variables as the source partition assignment. -- `ReduceTo> for GraphPartitioning` with: - - variable layout: vertex variables first, then edge variables in source edge order - - balance equality `sum_v x_v = n as f64 / 2.0` - - two linking constraints per edge: - - `y_e - x_u + x_v >= 0` - - `y_e + x_u - x_v >= 0` - - objective `min sum_e y_e` - - overhead: - - `num_vars = "num_vertices + num_edges"` - - `num_constraints = "2 * num_edges + 1"` -- `#[cfg(feature = "example-db")] canonical_rule_example_specs()` with the issue's 6-vertex graph and a canonical witness: - - source config: `[0, 0, 0, 1, 1, 1]` - - target config: `[0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0]` -- Feature-gated registration in `src/rules/mod.rs` and inclusion in `canonical_rule_example_specs()`. - -**Step 2: Run the focused tests and verify they pass** - -Run: -```bash -cargo test --features "ilp-highs example-db" graphpartitioning_ilp -- --include-ignored -``` - -Expected: all `graphpartitioning_ilp` tests pass. - -**Step 3: Refactor only if needed** - -Keep only cleanup that preserves behavior: -- small helper for balance constraint construction -- comment documenting the variable ordering used by `extract_solution` - -### Task 3: Verify registry and example-db wiring - -**Files:** -- Modify: `src/rules/mod.rs` -- Read for patterns: `src/rules/minimummultiwaycut_ilp.rs` - -**Step 1: Run export commands that depend on rule registration** - -Run: -```bash -cargo run --example export_graph -cargo run --example export_schemas -cargo run --features "example-db" --example export_examples -``` - -Expected: -- `export_graph` includes a `GraphPartitioning -> ILP` edge. -- `export_examples` completes and writes `src/example_db/fixtures/examples.json`. - -**Step 2: If export output reveals missing wiring, fix only the missing registration and rerun the failing command** - -### Task 4: Run broader code verification for the implementation batch - -**Files:** -- No new files unless a verification failure requires a minimal follow-up fix - -**Step 1: Run the relevant batch verification** - -Run: -```bash -cargo test --features "ilp-highs example-db" graphpartitioning_ilp graph_partitioning -- --include-ignored -cargo clippy --all-targets --features ilp-highs -- -D warnings -``` - -Expected: tests pass and clippy reports no warnings. - -**Step 2: Commit the implementation batch** - -Run: -```bash -git add src/rules/graphpartitioning_ilp.rs src/rules/mod.rs src/unit_tests/rules/graphpartitioning_ilp.rs -git commit -m "Add GraphPartitioning to ILP reduction" -``` - -## Batch 2: Paper entry and fixture-backed documentation - -Aligned with `add-rule` Step 5. - -### Task 5: Add the paper reduction entry - -**Files:** -- Modify: `docs/paper/reductions.typ` -- Read for patterns: nearby `GraphPartitioning` problem definition -- Read for patterns: `#reduction-rule("MinimumMultiwayCut", "ILP")` -- Read for patterns: `#reduction-rule("TravelingSalesman", "ILP", example: true, ...)` - -**Step 1: Write the fixture-backed reduction-rule entry** - -Add a `GraphPartitioning -> ILP` theorem near the other ILP reductions that includes: -- theorem body summarizing the vertex/edge-indicator formulation and the `n + m` / `2m + 1` size -- proof body sections for construction, correctness, and solution extraction -- an `example: true` walkthrough backed by `load-rule-example("GraphPartitioning", "ILP")` -- explicit note that odd `n` produces an infeasible balance equality because `n / 2` is fractional - -The example should read the exported witness data rather than hardcoding a second copy of the solution. - -**Step 2: Build the paper and verify it passes** - -Run: -```bash -make paper -``` - -Expected: Typst builds successfully and the new reduction entry resolves its example data. - -### Task 6: Final verification for the branch state - -**Files:** -- Any generated tracked outputs from the export and paper build steps - -**Step 1: Run final verification commands** - -Run: -```bash -cargo test --features "ilp-highs example-db" graphpartitioning_ilp graph_partitioning -- --include-ignored -cargo clippy --all-targets --features ilp-highs -- -D warnings -make paper -git status --short -``` - -Expected: -- tests pass -- clippy passes -- paper builds -- `git status --short` shows only intended tracked changes plus ignored/generated files under ignored export paths - -**Step 2: Commit the documentation/export batch** - -Run: -```bash -git add docs/paper/reductions.typ src/example_db/fixtures/examples.json docs/paper/reductions.pdf docs/paper/graph.json docs/src/schema/problem_schemas.json -git commit -m "Document GraphPartitioning to ILP reduction" -``` - -If generated tracked file paths differ, stage the actual tracked outputs reported by `git status --short` instead of forcing this exact list. - -### Task 7: Remove the plan file after implementation - -**Files:** -- Delete: `docs/plans/2026-03-20-graphpartitioning-to-ilp.md` - -**Step 1: Remove the temporary plan artifact** - -Run: -```bash -git rm docs/plans/2026-03-20-graphpartitioning-to-ilp.md -git commit -m "chore: remove plan file after implementation" -``` - -## Notes for the executor - -- Stay inside the issue worktree branch `issue-118`. -- Do not touch the user's main checkout. -- Do not "fix" unrelated changes in the parent repository. -- Keep the implementation scoped to this one rule; do not add model changes. From b8c8c4ca26449056b04dfe09c8fe68393020befb Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sat, 21 Mar 2026 01:02:34 +0800 Subject: [PATCH 5/8] Fix import order in graphpartitioning_ilp.rs for rustfmt compliance Co-Authored-By: Claude Opus 4.6 (1M context) --- src/rules/graphpartitioning_ilp.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/rules/graphpartitioning_ilp.rs b/src/rules/graphpartitioning_ilp.rs index 4d20d0f7d..94b280286 100644 --- a/src/rules/graphpartitioning_ilp.rs +++ b/src/rules/graphpartitioning_ilp.rs @@ -5,7 +5,7 @@ //! - Constraints: one balance equality plus two linking inequalities per edge //! - Objective: minimize the number of crossing edges -use crate::models::algebraic::{ILP, LinearConstraint, ObjectiveSense}; +use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP}; use crate::models::graph::GraphPartitioning; use crate::reduction; use crate::rules::traits::{ReduceTo, ReductionResult}; From 285aa39e68d019698a75c41775978e2f1b5e2168 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sat, 21 Mar 2026 01:47:02 +0800 Subject: [PATCH 6/8] Remove duplicate BibTeX entries introduced during merge The merge with main duplicated chopra1996, eppstein1992, kou1977, and lawler1972 entries. Keep the originals and remove duplicates. Co-Authored-By: Claude Opus 4.6 (1M context) --- docs/paper/references.bib | 43 --------------------------------------- 1 file changed, 43 deletions(-) diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 3caf67f84..3728fe98a 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -1076,16 +1076,6 @@ @phdthesis{booth1975 year = {1975} } -@article{chopra1996, - author = {Sunil Chopra and Jonathan H. Owen}, - title = {Extended formulations for the A-cut problem}, - journal = {Mathematical Programming}, - volume = {73}, - pages = {7--30}, - year = {1996}, - doi = {10.1007/BF02592096} -} - @article{coffman1972, author = {Edward G. Coffman and Ronald L. Graham}, title = {Optimal Scheduling for Two-Processor Systems}, @@ -1097,17 +1087,6 @@ @article{coffman1972 doi = {10.1007/BF00288685} } -@article{eppstein1992, - author = {David Eppstein}, - title = {Finding the $k$ Smallest Spanning Trees}, - journal = {BIT}, - volume = {32}, - number = {2}, - pages = {237--248}, - year = {1992}, - doi = {10.1007/BF01994880} -} - @techreport{Heidari2022, author = {Heidari, Shahrokh and Dinneen, Michael J. and Delmas, Patrice}, title = {An Equivalent {QUBO} Model to the Minimum Multi-Way Cut Problem}, @@ -1127,17 +1106,6 @@ @article{hu1961 doi = {10.1287/opre.9.6.841} } -@article{kou1977, - author = {Lawrence T. Kou}, - title = {Polynomial Complete Consecutive Information Retrieval Problems}, - journal = {SIAM Journal on Computing}, - volume = {6}, - number = {1}, - pages = {67--75}, - year = {1977}, - doi = {10.1137/0206005} -} - @article{haddadi2008, author = {Salim Haddadi and Zohra Layouni}, title = {Consecutive block minimization is 1.5-approximable}, @@ -1149,17 +1117,6 @@ @article{haddadi2008 doi = {10.1016/j.ipl.2008.05.003} } -@article{lawler1972, - author = {Eugene L. Lawler}, - title = {A Procedure for Computing the $K$ Best Solutions to Discrete Optimization Problems and Its Application to the Shortest Path Problem}, - journal = {Management Science}, - volume = {18}, - number = {7}, - pages = {401--405}, - year = {1972}, - doi = {10.1287/mnsc.18.7.401} -} - @article{lenstra1978, author = {Jan Karel Lenstra and Alexander H. G. Rinnooy Kan}, title = {Complexity of Scheduling under Precedence Constraints}, From f16f3a68eddaf3a299c0e88085c8f735ea510390 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sat, 21 Mar 2026 02:03:52 +0800 Subject: [PATCH 7/8] Fix formatting after merge with main Co-Authored-By: Claude Opus 4.6 (1M context) --- .claude/skills/final-review/SKILL.md | 11 +++++------ src/models/formula/qbf.rs | 1 - src/unit_tests/models/formula/qbf.rs | 7 ++----- 3 files changed, 7 insertions(+), 12 deletions(-) diff --git a/.claude/skills/final-review/SKILL.md b/.claude/skills/final-review/SKILL.md index ad2b01a79..9650cb20a 100644 --- a/.claude/skills/final-review/SKILL.md +++ b/.claude/skills/final-review/SKILL.md @@ -87,14 +87,12 @@ git fetch origin main git merge origin/main --no-edit ``` -- **Merge clean** — merge commit is ready locally. Run `cargo check` to verify the merge didn't introduce API incompatibilities (e.g., functions renamed/removed on main that the PR still calls). If `cargo check` fails, fix the compile errors before proceeding. -- **Merge conflicted** — most conflicts in this codebase are "both sides added new entries in ordered lists" (in `mod.rs`, `lib.rs`, `create.rs`, `dispatch.rs`, `reductions.typ`). These are mechanical: keep both sides, maintain alphabetical order. Delegate to a subagent for resolution, then run `cargo check` to verify. Continue with the review; if conflicts are too complex, decide whether to hold in Step 5. +- **Merge clean** — merge commit is ready locally. Run `make check && make paper` to verify the merge didn't break anything (API incompatibilities, formatting, test failures, paper compilation). If any step fails, fix the errors before proceeding. For `.bib` conflicts, also check for duplicate BibTeX keys (`grep '^@' docs/paper/references.bib | sed 's/@[a-z]*{//' | sed 's/,$//' | sort | uniq -d`) and remove duplicates. +- **Merge conflicted** — most conflicts in this codebase are "both sides added new entries in ordered lists" (in `mod.rs`, `lib.rs`, `create.rs`, `dispatch.rs`, `reductions.typ`). These are mechanical: keep both sides, maintain alphabetical order. Delegate to a subagent for resolution, then run `make check && make paper` to verify. Continue with the review; if conflicts are too complex, decide whether to hold in Step 5. - **Merge failed** — note the error and continue. **0d. Sanity check**: verify the diff touches `src/models/` or `src/rules/` (for model/rule PRs). If the diff only contains unrelated files, STOP and flag the mismatch. -**0e. Documentation build check**: if the PR touches `docs/paper/reductions.typ`, `docs/paper/references.bib`, or example specs, run `make paper` to verify the Typst paper compiles with the merged code. If compilation fails, check whether the error is in files touched by this PR. If not, note "pre-existing paper error from [source model/rule]" and continue — do not block the review on errors from other merged PRs. Only fix errors caused by this PR. - ### Step 1: Gather Context Use `gh` commands to get the PR's actual data — always from GitHub, never from local git state: @@ -380,12 +378,13 @@ Use `AskUserQuestion` only when needed: ### Step 8: Execute decision **If Push and fix CI:** -1. Push all commits (merge-with-main + any fixes) from the worktree: +1. **Pre-push verification** — run `make check && make paper` locally before pushing. Both must pass. Fix any failures, commit, then push: ```bash cd + make check && make paper git push ``` -2. Wait for CI — but **do not poll excessively**. Check once after ~60 seconds. If CI hasn't triggered or is still pending, run `make check` locally (fmt + clippy + test). If local checks pass, proceed to step 4 immediately and note "CI pending, local checks pass" when presenting the merge link. The reviewer can admin-merge or wait for CI at their discretion. Do not spend more than 1–2 CI poll attempts. If CI does run and fails, fix the issues, commit, and push again. +2. Wait for CI — but **do not poll excessively**. Check once after ~60 seconds. If CI hasn't triggered or is still pending, note "CI pending, local checks pass" when presenting the merge link (since pre-push already verified). The reviewer can admin-merge or wait for CI at their discretion. Do not spend more than 1–2 CI poll attempts. If CI does run and fails, fix the issues, commit, and push again. 3. If any follow-up items were noted during the review, post them as a comment: ```bash COMMENT_FILE=$(mktemp) diff --git a/src/models/formula/qbf.rs b/src/models/formula/qbf.rs index 5b48522c3..830ddc167 100644 --- a/src/models/formula/qbf.rs +++ b/src/models/formula/qbf.rs @@ -153,7 +153,6 @@ impl QuantifiedBooleanFormulas { } } } - } impl Problem for QuantifiedBooleanFormulas { diff --git a/src/unit_tests/models/formula/qbf.rs b/src/unit_tests/models/formula/qbf.rs index be46c741f..eccd7d28b 100644 --- a/src/unit_tests/models/formula/qbf.rs +++ b/src/unit_tests/models/formula/qbf.rs @@ -255,10 +255,7 @@ fn test_qbf_quantifier_clone() { #[test] fn test_qbf_empty_clause() { // An empty clause (disjunction of zero literals) is always false - let problem = QuantifiedBooleanFormulas::new( - 1, - vec![Quantifier::Exists], - vec![CNFClause::new(vec![])], - ); + let problem = + QuantifiedBooleanFormulas::new(1, vec![Quantifier::Exists], vec![CNFClause::new(vec![])]); assert!(!problem.is_true()); } From 341cccf5235d4f0ea692efaf1d672d1477b70a02 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sat, 21 Mar 2026 02:08:10 +0800 Subject: [PATCH 8/8] Restore chopra1996 bib entry needed by existing paper content Co-Authored-By: Claude Opus 4.6 (1M context) --- docs/paper/references.bib | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/docs/paper/references.bib b/docs/paper/references.bib index b29c3151e..cee42d912 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -905,6 +905,16 @@ @article{chopra1993 doi = {10.1007/BF01581239} } +@article{chopra1996, + author = {Sunil Chopra and Jonathan H. Owen}, + title = {Extended formulations for the A-cut problem}, + journal = {Mathematical Programming}, + volume = {73}, + pages = {7--30}, + year = {1996}, + doi = {10.1007/BF02592096} +} + @article{boothlueker1976, author = {Kellogg S. Booth and George S. Lueker}, title = {Testing for the Consecutive Ones Property, Interval Graphs, and Graph Planarity Using {PQ}-Tree Algorithms},