Implementation Summary

Changes

• Added src/rules/hamiltoniancircuit_travelingsalesman.rs implementing the textbook HC -> TSP reduction on the complete graph with 1/2 edge weights, deterministic cycle extraction, and a canonical example fixture.
• Registered the new rule and canonical example in src/rules/mod.rs.
• Added src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs covering closed-loop behavior, target structure, a non-Hamiltonian cost gap, and solution extraction.
• Added a new HamiltonianCircuit -> TravelingSalesman theorem and worked example to docs/paper/reductions.typ.

Deviations from Plan

• Replaced the planned Petersen-graph negative test with a 4-vertex star graph because the Petersen reduction creates a 45-edge TSP instance, which is not tractable for the repository's brute-force target-solver tests.
• Used make paper's existing export pipeline (export_examples, export_graph, export_schemas) instead of a non-existent make regenerate-fixtures target.

Open Questions

• None.

Codecov Report

❌ Patch coverage is 96.66667% with 4 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.58%. Comparing base (669f090) to head (ba6ef2b).
⚠️ Report is 2 commits behind head on main.

@@           Coverage Diff            @@
##             main     #745    +/-   ##
========================================
  Coverage   97.58%   97.58%            
========================================
  Files         415      419     +4     
  Lines       51632    51819   +187     
========================================
+ Hits        50386    50569   +183     
- Misses       1246     1250     +4     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

Agentic Review Report

Structural Check

Structural Review: rule HamiltonianCircuit -> TravelingSalesman

Structural Completeness

Build Status

• make test: PASS
• make clippy: PASS

Semantic Review

• reduce_to(): OK - builds K_n on the same vertex set and assigns weight 1 to source edges and 2 to non-edges, matching the reduction.
• extract_solution(): OK - reconstructs a cycle ordering from the selected degree-2 edges and returns a source configuration of length n.
• Overhead formulas: OK - num_vertices = num_vertices and num_edges = n(n - 1) / 2 match the complete-graph target size exactly.
• Example/test coverage: OK - the closed-loop test, weight check, and non-Hamiltonian gap test cover the intended reduction behavior.

Issue Compliance

Summary

• 12/12 structural checks passed
• 6/6 issue compliance checks passed
• make test and make clippy passed
• No findings

Quality Check

Quality Review

Design Principles

• DRY: OK
• KISS: OK
• HC/LC: OK

Test Quality

• Naive test detection: ISSUE — all new tests stay on 4-vertex cases (cycle4_hc() and star(4)), so the extractor and weight mapping are not exercised on a larger Hamiltonian-cycle instance. src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs

Issues

Critical (Must Fix)

• None.

Important (Should Fix)

• None.

Minor (Nice to Have)

• Broaden the rule tests beyond 4-vertex graphs so the reduction is validated on at least one 5+ vertex case.

Summary

• Minor: tests only cover 4-vertex instances; no 5+ vertex case.

Agentic Feature Tests

Summary

Per-Feature Details

HamiltonianCircuit -> TravelingSalesman

• Role: downstream CLI user validating a new reduction from the catalog and docs
• Use Case: find the rule, create the canonical source example, solve it, and reduce it to TravelingSalesman
• What they tried: pred list, pred list --rules, pred show HamiltonianCircuit, pred show TravelingSalesman, pred create --example HamiltonianCircuit, pred create --example HamiltonianCircuit --to TravelingSalesman --example-side source/target, pred solve - --solver brute-force, and pred reduce - --to TravelingSalesman
• Discoverability: yes; the model and rule are visible in the catalog, and show exposes the outgoing reduction
• Setup: no special setup was needed beyond running the CLI in the worktree; the commands executed successfully
• Functionality: the model example created correctly; the canonical rule witness created correctly; brute-force solving succeeded; reducing the canonical source example produced a TravelingSalesman instance with the expected 1/2 edge weights and Valid(4) target evaluation
• Expected vs Actual Outcome: matched; the canonical source example was the 4-cycle, and reduction produced the documented TSP witness. One nuance: plain pred create --example HamiltonianCircuit returns the standalone model example, not the rule witness, so --to TravelingSalesman is needed to reach the canonical reduction example
• Blocked steps: none
• Friction points: the distinction between model examples and rule examples is easy to miss if a user only sees pred create --example HamiltonianCircuit
• Doc suggestions: add a concrete pred create --example HamiltonianCircuit --to TravelingSalesman --example-side source example near the new rule docs, and mention the corresponding target-side witness command so users can reproduce the canonical pair directly

Issues Found

None.

Suggestions

• Add an explicit CLI example for the rule-specific canonical witness, not just the model-level example.
• Mention that the reduction witness lives behind --to TravelingSalesman, so users do not confuse it with the standalone HamiltonianCircuit example.

Additional Local Verification

Important (Should Fix)

• The rule is not correct on the full admitted HamiltonianCircuit input domain. reduce_to() always builds K_n on the same vertex set (src/rules/hamiltoniancircuit_travelingsalesman.rs), but TravelingSalesman has no feasible Hamiltonian cycle for n < 3. A confirmed out-of-tree reproduction with a 2-vertex source graph produced source_dims=[2, 2], target_vertices=2 target_edges=1, and BruteForce::find_best(target) == None. That breaks the documented invariant that the target optimum distinguishes YES from NO HC instances; for these valid source instances the target has no optimum at all. The new tests only exercise 4-vertex inputs, so this regression is currently uncovered (src/unit_tests/rules/hamiltoniancircuit_travelingsalesman.rs).

Generated by review-pipeline