From 3c8f88931445c2a0a321a9cbc8bf59518589150d Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 08:36:46 +0800 Subject: [PATCH 1/3] Add plan for #258: [Rule] HamiltonianCircuit to TravelingSalesman --- ...hamiltoniancircuit-to-travelingsalesman.md | 235 ++++++++++++++++++ 1 file changed, 235 insertions(+) create mode 100644 docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md diff --git a/docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md b/docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md new file mode 100644 index 000000000..770e5cd25 --- /dev/null +++ b/docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md @@ -0,0 +1,235 @@ +# HamiltonianCircuit to TravelingSalesman Implementation Plan + +> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. + +**Goal:** Implement issue #258 by adding the primitive reduction `HamiltonianCircuit -> TravelingSalesman`, plus tests, canonical example data, paper documentation, and regenerated exports/fixtures. + +**Architecture:** The reduction should build the complete graph on the same vertex set, assign weight `1` to source edges and weight `2` to non-edges, and rely on the existing optimization-style `TravelingSalesman` model. `ReductionResult::extract_solution()` must turn the selected TSP cycle edges back into a Hamiltonian-circuit vertex permutation by traversing the unique degree-2 cycle. Use a small 4-cycle source instance for the canonical rule example and paper walkthrough so the transformed complete graph stays readable. + +**Tech Stack:** Rust workspace, `#[reduction]` registry macro, `BruteForce`, `example-db`, Typst paper, export helpers. + +--- + +## Information Checklist + +| # | Item | Value | +|---|------|-------| +| 1 | Source problem | `HamiltonianCircuit` | +| 2 | Target problem | `TravelingSalesman` | +| 3 | Reduction algorithm | Build `K_n` on the same vertices; weight each edge `1` if it exists in the source graph and `2` otherwise | +| 4 | Solution extraction | Traverse the selected TSP cycle and emit a Hamiltonian-circuit permutation in source vertex IDs | +| 5 | Correctness argument | TSP uses exactly `n` edges; total weight `n` is achievable iff every selected edge has weight `1`, i.e. iff the tour is a Hamiltonian circuit in the source graph | +| 6 | Size overhead | `num_vertices = "num_vertices"`, `num_edges = "num_vertices * (num_vertices - 1) / 2"` | +| 7 | Concrete example | 4-cycle `(0,1),(1,2),(2,3),(3,0)` mapped to weighted `K_4` with cycle edges weight `1` and diagonals weight `2` | +| 8 | Solving strategy | `BruteForce::find_all_best()` on the target TSP instance | +| 9 | Reference | Garey & Johnson ND22; the issue comments also confirm the sat-to-opt framing already expected by this codebase | + +## Batch 1: Rule, Tests, Example Data + +### Task 1: Lock the target behavior with focused rule tests + +**Files:** +- Create: `src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs` +- Modify: `src/rules/mod.rs` +- Reference: `src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs` +- Reference: `src/rules/test_helpers.rs` + +**Step 1: Write the failing tests** + +Add tests that cover: +- `test_hamiltoniancircuit_to_travelingsalesman_closed_loop` on a YES instance using `assert_satisfaction_round_trip_from_optimization_target` +- `test_hamiltoniancircuit_to_travelingsalesman_structure` to verify the target graph is complete and weights are `1/2` according to source-edge membership +- `test_hamiltoniancircuit_to_travelingsalesman_nonhamiltonian_cost_gap` on the Petersen graph, asserting the optimal TSP value is strictly greater than `num_vertices` +- `test_hamiltoniancircuit_to_travelingsalesman_extract_solution_cycle` to verify `extract_solution()` returns a valid Hamiltonian-circuit permutation for a known target witness + +**Step 2: Wire the module so the test can compile once the rule exists** + +Add `pub(crate) mod hamiltoniancircuit_travelingsalesman;` to `src/rules/mod.rs`. + +**Step 3: Run the focused test to verify it fails** + +Run: `cargo test hamiltoniancircuit_to_travelingsalesman --lib` + +Expected: compile failure or unresolved `ReduceTo> for HamiltonianCircuit` until the rule file is implemented. + +### Task 2: Implement the primitive reduction + +**Files:** +- Create: `src/rules/hamiltoniancircuit_travelingsalesman.rs` +- Modify: `src/rules/mod.rs` +- Reference: `src/models/graph/hamiltonian_circuit.rs` +- Reference: `src/models/graph/traveling_salesman.rs` +- Reference: `src/rules/sat_maximumindependentset.rs` + +**Step 1: Add the reduction result type** + +Define a `ReductionHamiltonianCircuitToTravelingSalesman` struct that stores the target `TravelingSalesman` instance. + +**Step 2: Implement `ReductionResult`** + +Implement: +- `target_problem()` as a simple reference getter +- `extract_solution()` by: + - collecting the selected target edges + - building degree-2 adjacency from those selected edges + - traversing the single cycle to recover a permutation of all vertices + - returning that permutation in source vertex order + +Use the target graph’s edge order directly; do not add extra index mapping state unless traversal proves impossible without it. + +**Step 3: Implement `ReduceTo>`** + +Build the complete graph on the source vertex set and weight edges with: +- `1` if `self.graph().has_edge(u, v)` +- `2` otherwise + +Register the reduction with: + +```rust +#[reduction(overhead = { + num_vertices = "num_vertices", + num_edges = "num_vertices * (num_vertices - 1) / 2", +})] +``` + +**Step 4: Link the new test module** + +Add: + +```rust +#[cfg(test)] +#[path = "../unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs"] +mod tests; +``` + +to the bottom of the new rule file. + +**Step 5: Run the focused test to verify it passes** + +Run: `cargo test hamiltoniancircuit_to_travelingsalesman --lib` + +Expected: all new rule tests pass. + +### Task 3: Add canonical rule example data + +**Files:** +- Modify: `src/rules/hamiltoniancircuit_travelingsalesman.rs` +- Modify: `src/rules/mod.rs` +- Reference: `src/rules/minimumvertexcover_maximumindependentset.rs` + +**Step 1: Add `canonical_rule_example_specs()` to the rule file** + +Use a 4-cycle source graph: +- source config: `[0, 1, 2, 3]` +- target graph: weighted `K_4` +- target config: select the four cycle edges that correspond to the source circuit + +Construct the example with `rule_example_with_witness::<_, TravelingSalesman>()`. + +**Step 2: Register the example spec in `src/rules/mod.rs`** + +Extend `canonical_rule_example_specs()` with `hamiltoniancircuit_travelingsalesman::canonical_rule_example_specs()`. + +**Step 3: Regenerate the exports needed by docs and fixtures** + +Run: +- `cargo run --example export_graph` +- `cargo run --example export_schemas` + +Expected: updated reduction graph and problem schema exports include the new rule. + +### Task 4: Validate batch-1 behavior before touching paper + +**Files:** +- No new files + +**Step 1: Run the focused rule/example checks** + +Run: +- `cargo test hamiltoniancircuit_to_travelingsalesman --lib` +- `cargo test example_db --lib` + +Expected: the new rule behaves correctly and the canonical witness round-trips. + +**Step 2: Commit the implementation batch** + +Run: + +```bash +git add src/rules/mod.rs \ + src/rules/hamiltoniancircuit_travelingsalesman.rs \ + src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs +git commit -m "Add HamiltonianCircuit to TravelingSalesman reduction" +``` + +Do not commit `docs/plans/...` beyond the initial plan-only PR commit; that file is removed later by the pipeline. + +## Batch 2: Paper Entry and Full Verification + +### Task 5: Document the rule in the paper + +**Files:** +- Modify: `docs/paper/reductions.typ` +- Reference: `docs/paper/reductions.typ` (`TravelingSalesman -> ILP`, `TravelingSalesman -> QUBO`) + +**Step 1: Add the theorem entry** + +Write a new `#reduction-rule("HamiltonianCircuit", "TravelingSalesman", ...)` entry that: +- states the `O(n^2)` construction on the complete graph +- explains the sat-to-opt correctness criterion (`opt = n iff HC exists`) +- describes solution extraction from selected TSP edges back to a Hamiltonian-circuit permutation + +**Step 2: Add the worked example block** + +Use the canonical 4-cycle fixture and start the `extra:` block with: +- `pred create --example HamiltonianCircuit -o hc.json` +- `pred reduce hc.json --to ... -o bundle.json` +- `pred solve bundle.json` +- `pred evaluate hc.json --config ...` + +The example text should explicitly call out the two diagonal non-edges having weight `2`. + +### Task 6: Regenerate fixtures and run the repo verification set + +**Files:** +- Generated: exports and example fixtures + +**Step 1: Regenerate example fixtures** + +Run: `make regenerate-fixtures` + +Expected: `src/example_db/fixtures/examples.json` gains the new rule example. + +**Step 2: Build the paper** + +Run: `make paper` + +Expected: Typst succeeds and the new theorem/example renders without missing fixture data. + +**Step 3: Run final verification** + +Run: +- `make test` +- `make clippy` +- `make fmt-check` + +Expected: all checks pass. + +**Step 4: Commit the documentation/export batch** + +Run: + +```bash +git add docs/paper/reductions.typ \ + src/example_db/fixtures/examples.json +git commit -m "Document HamiltonianCircuit to TravelingSalesman reduction" +``` + +Include any tracked export updates from `cargo run --example export_graph` / `cargo run --example export_schemas` if they changed. + +## Implementation Notes + +- Favor the existing `SimpleGraph::new(n, edges)` edge ordering and build tests around `graph.edges()` rather than hard-coding index assumptions from manual combinatorics. +- In the non-Hamiltonian test, assert the target optimum is `> n`; do not require a specific gap. +- Keep `extract_solution()` tolerant of either tour orientation. It only needs to return a valid Hamiltonian-circuit permutation, not a canonical rotation. +- This rule is a single primitive endpoint pair. Do not add extra cast rules or variant registrations. From 9abcc379820d6999170bf84dab45aff4a7d91350 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 08:49:53 +0800 Subject: [PATCH 2/3] Implement #258: [Rule] HamiltonianCircuit to TravelingSalesman --- docs/paper/reductions.typ | 38 +++++ .../hamiltoniancircuit_travelingsalesman.rs | 130 ++++++++++++++++++ src/rules/mod.rs | 2 + .../hamiltoniancircuit_travelingsalesman.rs | 74 ++++++++++ 4 files changed, 244 insertions(+) create mode 100644 src/rules/hamiltoniancircuit_travelingsalesman.rs create mode 100644 src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 9167a0c15..7252348d4 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -6680,6 +6680,44 @@ The following reductions to Integer Linear Programming are straightforward formu _Solution extraction._ Sort tasks by their completion times $C_j$ and encode that order back into the source schedule representation. ] +#let hc_tsp = load-example("HamiltonianCircuit", "TravelingSalesman") +#let hc_tsp_sol = hc_tsp.solutions.at(0) +#let hc_tsp_n = graph-num-vertices(hc_tsp.source.instance) +#let hc_tsp_source_edges = hc_tsp.source.instance.graph.edges +#let hc_tsp_target_edges = hc_tsp.target.instance.graph.edges +#let hc_tsp_target_weights = hc_tsp.target.instance.edge_weights +#let hc_tsp_weight_one = hc_tsp_target_edges.enumerate().filter(((i, _)) => hc_tsp_target_weights.at(i) == 1).map(((i, e)) => (e.at(0), e.at(1))) +#let hc_tsp_weight_two = hc_tsp_target_edges.enumerate().filter(((i, _)) => hc_tsp_target_weights.at(i) == 2).map(((i, e)) => (e.at(0), e.at(1))) +#let hc_tsp_selected_edges = hc_tsp_target_edges.enumerate().filter(((i, _)) => hc_tsp_sol.target_config.at(i) == 1).map(((i, e)) => (e.at(0), e.at(1))) +#reduction-rule("HamiltonianCircuit", "TravelingSalesman", + example: true, + example-caption: [Cycle graph on $#hc_tsp_n$ vertices to weighted $K_#hc_tsp_n$], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(hc_tsp.source) + " -o hc.json", + "pred reduce hc.json --to " + target-spec(hc_tsp) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate hc.json --config " + hc_tsp_sol.source_config.map(str).join(","), + ) + + *Step 1 -- Start from the source graph.* The canonical source fixture is the cycle on vertices ${0, 1, 2, 3}$ with edges #hc_tsp_source_edges.map(e => $(#e.at(0), #e.at(1))$).join(", "). The stored Hamiltonian-circuit witness is the permutation $[#hc_tsp_sol.source_config.map(str).join(", ")]$.\ + + *Step 2 -- Complete the graph and encode adjacency by weights.* The target keeps the same $#hc_tsp_n$ vertices but adds the missing diagonals, so it becomes $K_#hc_tsp_n$ with $#graph-num-edges(hc_tsp.target.instance)$ undirected edges. The original cycle edges #hc_tsp_weight_one.map(e => $(#e.at(0), #e.at(1))$).join(", ") receive weight 1, while the diagonals #hc_tsp_weight_two.map(e => $(#e.at(0), #e.at(1))$).join(", ") receive weight 2.\ + + *Step 3 -- Verify the canonical witness.* The stored target configuration $[#hc_tsp_sol.target_config.map(str).join(", ")]$ selects the tour edges #hc_tsp_selected_edges.map(e => $(#e.at(0), #e.at(1))$).join(", "). Its total cost is $1 + 1 + 1 + 1 = #hc_tsp_n$, so every chosen edge is a weight-1 source edge, and traversing the selected cycle recovers the Hamiltonian circuit $[#hc_tsp_sol.source_config.map(str).join(", ")]$.\ + + *Multiplicity:* The fixture stores one canonical witness. For the 4-cycle there are $4 times 2 = 8$ Hamiltonian-circuit permutations (choice of start vertex and direction), but they all induce the same undirected target edge set. + ], +)[ + @garey1979 This $O(n^2)$ reduction constructs the complete graph on the same vertex set and uses edge weights to distinguish source edges from non-edges: weight 1 means "present in the source" and weight 2 means "missing in the source" ($n (n - 1) / 2$ target edges). +][ + _Construction._ Given a Hamiltonian Circuit instance $G = (V, E)$ with $n = |V|$, construct the complete graph $K_n$ on the same vertex set. For each pair $u < v$, set $w(u, v) = 1$ if $(u, v) in E$ and $w(u, v) = 2$ otherwise. The target TSP instance asks for a minimum-weight Hamiltonian cycle in this weighted complete graph. + + _Correctness._ ($arrow.r.double$) If $G$ has a Hamiltonian circuit $v_0, v_1, dots, v_(n-1), v_0$, then the same cycle exists in $K_n$. Every chosen edge belongs to $E$, so each edge has weight 1 and the resulting TSP tour has total cost $n$. ($arrow.l.double$) Every TSP tour on $n$ vertices uses exactly $n$ edges, and every target edge has weight at least 1, so any tour has cost at least $n$. If the optimum cost is exactly $n$, every selected edge must therefore have weight 1. Those edges are precisely edges of $G$, so the optimal TSP tour is already a Hamiltonian circuit in the source graph. + + _Solution extraction._ Read the selected TSP edges, traverse the unique degree-2 cycle they form, and return the resulting vertex permutation as the source Hamiltonian-circuit witness. +] + #let tsp_ilp = load-example("TravelingSalesman", "ILP") #let tsp_ilp_sol = tsp_ilp.solutions.at(0) #reduction-rule("TravelingSalesman", "ILP", diff --git a/src/rules/hamiltoniancircuit_travelingsalesman.rs b/src/rules/hamiltoniancircuit_travelingsalesman.rs new file mode 100644 index 000000000..f34703f7d --- /dev/null +++ b/src/rules/hamiltoniancircuit_travelingsalesman.rs @@ -0,0 +1,130 @@ +//! Reduction from HamiltonianCircuit to TravelingSalesman. +//! +//! The standard construction embeds the source graph into the complete graph on the +//! same vertex set, assigning weight 1 to source edges and weight 2 to non-edges. +//! The target optimum is exactly n iff the source graph contains a Hamiltonian circuit. + +use crate::models::graph::{HamiltonianCircuit, TravelingSalesman}; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; + +/// Result of reducing HamiltonianCircuit to TravelingSalesman. +#[derive(Debug, Clone)] +pub struct ReductionHamiltonianCircuitToTravelingSalesman { + target: TravelingSalesman, +} + +impl ReductionResult for ReductionHamiltonianCircuitToTravelingSalesman { + type Source = HamiltonianCircuit; + type Target = TravelingSalesman; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + let graph = self.target.graph(); + let n = graph.num_vertices(); + if n == 0 { + return vec![]; + } + + let edges = graph.edges(); + if target_solution.len() != edges.len() { + return vec![0; n]; + } + + let mut adjacency = vec![Vec::new(); n]; + let mut selected_count = 0usize; + for (idx, &selected) in target_solution.iter().enumerate() { + if selected != 1 { + continue; + } + let (u, v) = edges[idx]; + adjacency[u].push(v); + adjacency[v].push(u); + selected_count += 1; + } + + if selected_count != n || adjacency.iter().any(|neighbors| neighbors.len() != 2) { + return vec![0; n]; + } + + for neighbors in &mut adjacency { + neighbors.sort_unstable(); + } + + let mut order = Vec::with_capacity(n); + let mut prev = None; + let mut current = 0usize; + + for _ in 0..n { + order.push(current); + let neighbors = &adjacency[current]; + let next = match prev { + Some(previous) => { + if neighbors[0] == previous { + neighbors[1] + } else { + neighbors[0] + } + } + None => neighbors[0], + }; + prev = Some(current); + current = next; + } + + order + } +} + +#[reduction( + overhead = { + num_vertices = "num_vertices", + num_edges = "num_vertices * (num_vertices - 1) / 2", + } +)] +impl ReduceTo> for HamiltonianCircuit { + type Result = ReductionHamiltonianCircuitToTravelingSalesman; + + fn reduce_to(&self) -> Self::Result { + let num_vertices = self.num_vertices(); + let target_graph = SimpleGraph::complete(num_vertices); + let weights = target_graph + .edges() + .into_iter() + .map(|(u, v)| if self.graph().has_edge(u, v) { 1 } else { 2 }) + .collect(); + let target = TravelingSalesman::new(target_graph, weights); + + ReductionHamiltonianCircuitToTravelingSalesman { target } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "hamiltoniancircuit_to_travelingsalesman", + build: || { + let source = HamiltonianCircuit::new(SimpleGraph::cycle(4)); + crate::example_db::specs::rule_example_with_witness::< + _, + TravelingSalesman, + >( + source, + SolutionPair { + source_config: vec![0, 1, 2, 3], + target_config: vec![1, 0, 1, 1, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index d7929687b..421832b71 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -13,6 +13,7 @@ pub(crate) mod factoring_circuit; mod graph; pub(crate) mod graphpartitioning_maxcut; pub(crate) mod graphpartitioning_qubo; +pub(crate) mod hamiltoniancircuit_travelingsalesman; mod kcoloring_casts; mod knapsack_qubo; mod ksatisfiability_casts; @@ -105,6 +106,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec HamiltonianCircuit { + HamiltonianCircuit::new(SimpleGraph::cycle(4)) +} + +#[test] +fn test_hamiltoniancircuit_to_travelingsalesman_closed_loop() { + let source = cycle4_hc(); + let reduction = ReduceTo::>::reduce_to(&source); + + assert_satisfaction_round_trip_from_optimization_target( + &source, + &reduction, + "HamiltonianCircuit -> TravelingSalesman", + ); +} + +#[test] +fn test_hamiltoniancircuit_to_travelingsalesman_structure() { + let source = cycle4_hc(); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + + assert_eq!(target.graph().num_vertices(), 4); + assert_eq!(target.graph().num_edges(), 6); + + for ((u, v), weight) in target.graph().edges().into_iter().zip(target.weights()) { + let expected = if source.graph().has_edge(u, v) { 1 } else { 2 }; + assert_eq!(weight, expected, "unexpected weight on edge ({u}, {v})"); + } +} + +#[test] +fn test_hamiltoniancircuit_to_travelingsalesman_nonhamiltonian_cost_gap() { + let source = HamiltonianCircuit::new(SimpleGraph::star(4)); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + let best = BruteForce::new() + .find_best(target) + .expect("complete weighted graph should always admit a tour"); + + match target.evaluate(&best) { + SolutionSize::Valid(cost) => assert!(cost > 4, "expected cost > 4, got {cost}"), + SolutionSize::Invalid => panic!("best TSP solution evaluated as invalid"), + } +} + +#[test] +fn test_hamiltoniancircuit_to_travelingsalesman_extract_solution_cycle() { + let source = cycle4_hc(); + let reduction = ReduceTo::>::reduce_to(&source); + let target = reduction.target_problem(); + let cycle_edges = [(0usize, 1usize), (1, 2), (2, 3), (0, 3)]; + let target_solution: Vec = target + .graph() + .edges() + .into_iter() + .map(|(u, v)| usize::from(cycle_edges.contains(&(u, v)) || cycle_edges.contains(&(v, u)))) + .collect(); + + let extracted = reduction.extract_solution(&target_solution); + + assert_eq!(target.evaluate(&target_solution), SolutionSize::Valid(4)); + assert_eq!(extracted.len(), 4); + assert!(source.evaluate(&extracted)); +} From 3f3d3982302fad667efc881bb08234e83c9561e3 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Sun, 22 Mar 2026 08:49:57 +0800 Subject: [PATCH 3/3] chore: remove plan file after implementation --- ...hamiltoniancircuit-to-travelingsalesman.md | 235 ------------------ 1 file changed, 235 deletions(-) delete mode 100644 docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md diff --git a/docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md b/docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md deleted file mode 100644 index 770e5cd25..000000000 --- a/docs/plans/2026-03-22-hamiltoniancircuit-to-travelingsalesman.md +++ /dev/null @@ -1,235 +0,0 @@ -# HamiltonianCircuit to TravelingSalesman Implementation Plan - -> **For Claude:** REQUIRED SUB-SKILL: Use superpowers:executing-plans to implement this plan task-by-task. - -**Goal:** Implement issue #258 by adding the primitive reduction `HamiltonianCircuit -> TravelingSalesman`, plus tests, canonical example data, paper documentation, and regenerated exports/fixtures. - -**Architecture:** The reduction should build the complete graph on the same vertex set, assign weight `1` to source edges and weight `2` to non-edges, and rely on the existing optimization-style `TravelingSalesman` model. `ReductionResult::extract_solution()` must turn the selected TSP cycle edges back into a Hamiltonian-circuit vertex permutation by traversing the unique degree-2 cycle. Use a small 4-cycle source instance for the canonical rule example and paper walkthrough so the transformed complete graph stays readable. - -**Tech Stack:** Rust workspace, `#[reduction]` registry macro, `BruteForce`, `example-db`, Typst paper, export helpers. - ---- - -## Information Checklist - -| # | Item | Value | -|---|------|-------| -| 1 | Source problem | `HamiltonianCircuit` | -| 2 | Target problem | `TravelingSalesman` | -| 3 | Reduction algorithm | Build `K_n` on the same vertices; weight each edge `1` if it exists in the source graph and `2` otherwise | -| 4 | Solution extraction | Traverse the selected TSP cycle and emit a Hamiltonian-circuit permutation in source vertex IDs | -| 5 | Correctness argument | TSP uses exactly `n` edges; total weight `n` is achievable iff every selected edge has weight `1`, i.e. iff the tour is a Hamiltonian circuit in the source graph | -| 6 | Size overhead | `num_vertices = "num_vertices"`, `num_edges = "num_vertices * (num_vertices - 1) / 2"` | -| 7 | Concrete example | 4-cycle `(0,1),(1,2),(2,3),(3,0)` mapped to weighted `K_4` with cycle edges weight `1` and diagonals weight `2` | -| 8 | Solving strategy | `BruteForce::find_all_best()` on the target TSP instance | -| 9 | Reference | Garey & Johnson ND22; the issue comments also confirm the sat-to-opt framing already expected by this codebase | - -## Batch 1: Rule, Tests, Example Data - -### Task 1: Lock the target behavior with focused rule tests - -**Files:** -- Create: `src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs` -- Modify: `src/rules/mod.rs` -- Reference: `src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs` -- Reference: `src/rules/test_helpers.rs` - -**Step 1: Write the failing tests** - -Add tests that cover: -- `test_hamiltoniancircuit_to_travelingsalesman_closed_loop` on a YES instance using `assert_satisfaction_round_trip_from_optimization_target` -- `test_hamiltoniancircuit_to_travelingsalesman_structure` to verify the target graph is complete and weights are `1/2` according to source-edge membership -- `test_hamiltoniancircuit_to_travelingsalesman_nonhamiltonian_cost_gap` on the Petersen graph, asserting the optimal TSP value is strictly greater than `num_vertices` -- `test_hamiltoniancircuit_to_travelingsalesman_extract_solution_cycle` to verify `extract_solution()` returns a valid Hamiltonian-circuit permutation for a known target witness - -**Step 2: Wire the module so the test can compile once the rule exists** - -Add `pub(crate) mod hamiltoniancircuit_travelingsalesman;` to `src/rules/mod.rs`. - -**Step 3: Run the focused test to verify it fails** - -Run: `cargo test hamiltoniancircuit_to_travelingsalesman --lib` - -Expected: compile failure or unresolved `ReduceTo> for HamiltonianCircuit` until the rule file is implemented. - -### Task 2: Implement the primitive reduction - -**Files:** -- Create: `src/rules/hamiltoniancircuit_travelingsalesman.rs` -- Modify: `src/rules/mod.rs` -- Reference: `src/models/graph/hamiltonian_circuit.rs` -- Reference: `src/models/graph/traveling_salesman.rs` -- Reference: `src/rules/sat_maximumindependentset.rs` - -**Step 1: Add the reduction result type** - -Define a `ReductionHamiltonianCircuitToTravelingSalesman` struct that stores the target `TravelingSalesman` instance. - -**Step 2: Implement `ReductionResult`** - -Implement: -- `target_problem()` as a simple reference getter -- `extract_solution()` by: - - collecting the selected target edges - - building degree-2 adjacency from those selected edges - - traversing the single cycle to recover a permutation of all vertices - - returning that permutation in source vertex order - -Use the target graph’s edge order directly; do not add extra index mapping state unless traversal proves impossible without it. - -**Step 3: Implement `ReduceTo>`** - -Build the complete graph on the source vertex set and weight edges with: -- `1` if `self.graph().has_edge(u, v)` -- `2` otherwise - -Register the reduction with: - -```rust -#[reduction(overhead = { - num_vertices = "num_vertices", - num_edges = "num_vertices * (num_vertices - 1) / 2", -})] -``` - -**Step 4: Link the new test module** - -Add: - -```rust -#[cfg(test)] -#[path = "../unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs"] -mod tests; -``` - -to the bottom of the new rule file. - -**Step 5: Run the focused test to verify it passes** - -Run: `cargo test hamiltoniancircuit_to_travelingsalesman --lib` - -Expected: all new rule tests pass. - -### Task 3: Add canonical rule example data - -**Files:** -- Modify: `src/rules/hamiltoniancircuit_travelingsalesman.rs` -- Modify: `src/rules/mod.rs` -- Reference: `src/rules/minimumvertexcover_maximumindependentset.rs` - -**Step 1: Add `canonical_rule_example_specs()` to the rule file** - -Use a 4-cycle source graph: -- source config: `[0, 1, 2, 3]` -- target graph: weighted `K_4` -- target config: select the four cycle edges that correspond to the source circuit - -Construct the example with `rule_example_with_witness::<_, TravelingSalesman>()`. - -**Step 2: Register the example spec in `src/rules/mod.rs`** - -Extend `canonical_rule_example_specs()` with `hamiltoniancircuit_travelingsalesman::canonical_rule_example_specs()`. - -**Step 3: Regenerate the exports needed by docs and fixtures** - -Run: -- `cargo run --example export_graph` -- `cargo run --example export_schemas` - -Expected: updated reduction graph and problem schema exports include the new rule. - -### Task 4: Validate batch-1 behavior before touching paper - -**Files:** -- No new files - -**Step 1: Run the focused rule/example checks** - -Run: -- `cargo test hamiltoniancircuit_to_travelingsalesman --lib` -- `cargo test example_db --lib` - -Expected: the new rule behaves correctly and the canonical witness round-trips. - -**Step 2: Commit the implementation batch** - -Run: - -```bash -git add src/rules/mod.rs \ - src/rules/hamiltoniancircuit_travelingsalesman.rs \ - src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs -git commit -m "Add HamiltonianCircuit to TravelingSalesman reduction" -``` - -Do not commit `docs/plans/...` beyond the initial plan-only PR commit; that file is removed later by the pipeline. - -## Batch 2: Paper Entry and Full Verification - -### Task 5: Document the rule in the paper - -**Files:** -- Modify: `docs/paper/reductions.typ` -- Reference: `docs/paper/reductions.typ` (`TravelingSalesman -> ILP`, `TravelingSalesman -> QUBO`) - -**Step 1: Add the theorem entry** - -Write a new `#reduction-rule("HamiltonianCircuit", "TravelingSalesman", ...)` entry that: -- states the `O(n^2)` construction on the complete graph -- explains the sat-to-opt correctness criterion (`opt = n iff HC exists`) -- describes solution extraction from selected TSP edges back to a Hamiltonian-circuit permutation - -**Step 2: Add the worked example block** - -Use the canonical 4-cycle fixture and start the `extra:` block with: -- `pred create --example HamiltonianCircuit -o hc.json` -- `pred reduce hc.json --to ... -o bundle.json` -- `pred solve bundle.json` -- `pred evaluate hc.json --config ...` - -The example text should explicitly call out the two diagonal non-edges having weight `2`. - -### Task 6: Regenerate fixtures and run the repo verification set - -**Files:** -- Generated: exports and example fixtures - -**Step 1: Regenerate example fixtures** - -Run: `make regenerate-fixtures` - -Expected: `src/example_db/fixtures/examples.json` gains the new rule example. - -**Step 2: Build the paper** - -Run: `make paper` - -Expected: Typst succeeds and the new theorem/example renders without missing fixture data. - -**Step 3: Run final verification** - -Run: -- `make test` -- `make clippy` -- `make fmt-check` - -Expected: all checks pass. - -**Step 4: Commit the documentation/export batch** - -Run: - -```bash -git add docs/paper/reductions.typ \ - src/example_db/fixtures/examples.json -git commit -m "Document HamiltonianCircuit to TravelingSalesman reduction" -``` - -Include any tracked export updates from `cargo run --example export_graph` / `cargo run --example export_schemas` if they changed. - -## Implementation Notes - -- Favor the existing `SimpleGraph::new(n, edges)` edge ordering and build tests around `graph.edges()` rather than hard-coding index assumptions from manual combinatorics. -- In the non-Hamiltonian test, assert the target optimum is `> n`; do not require a specific gap. -- Keep `extract_solution()` tolerant of either tour orientation. It only needs to return a valid Hamiltonian-circuit permutation, not a canonical rotation. -- This rule is a single primitive endpoint pair. Do not add extra cast rules or variant registrations.