Skip to content

Fix #1097: HamiltonianPath to HamiltonianCircuit - #1106

Open
isPANN wants to merge 4 commits into
1075-growth-domainfrom
issue-1097
Open

Fix #1097: HamiltonianPath to HamiltonianCircuit#1106
isPANN wants to merge 4 commits into
1075-growth-domainfrom
issue-1097

Conversation

@isPANN

@isPANN isPANN commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator

Summary

Add the witness-preserving universal-vertex reduction from Hamiltonian Path to Hamiltonian Circuit, including boundary cases, canonical examples, tests, and paper documentation.

Fixes #1097

@isPANN

isPANN commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator Author

Implementation Summary

Changes

  • Added the direct HamiltonianPath<SimpleGraph> -> HamiltonianCircuit<SimpleGraph> universal-vertex reduction, including the explicit empty/singleton K3 branch and rotate/delete witness extraction.
  • Registered the reduction and its canonical five-vertex example.
  • Added focused semantic tests for closed-loop behavior, infeasible graphs, rotations and orientations, boundary instances, and loop/parallel-edge preservation.
  • Added the fixture-driven paper theorem and tutorial, with the Waggoner course-note citation that explicitly states the construction.
  • Updated the dominated-rule expectation because the new HamiltonianPath -> HamiltonianCircuit -> RuralPostman -> ILP composite route is no worse than the existing direct HamiltonianPath -> ILP edge.

Deviations from Plan

  • The PR is stacked on 1075-growth-domain at commit a9067297, as requested, instead of targeting main directly.
  • Full integration testing revealed the new dominated-route expectation above; the semantic allow-list was updated accordingly.

Open Questions

  • None.

Verification

  • Independent mathematical constructor: 53,724 checks.
  • Independent adversary with two Hypothesis strategies: 19,523 checks.
  • Cross-comparison: all 1,100 simple graphs through five vertices, zero disagreements.
  • make test: passed.
  • make clippy: passed.
  • make paper: passed.
  • make coverage: passed and generated the HTML report.

@isPANN

isPANN commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator Author

Agentic Review Report

Structural Check

Structural Review: rule HamiltonianPath -> HamiltonianCircuit

Structural Completeness

# Check Status
1 Rule file exists PASS — src/rules/hamiltonianpath_hamiltoniancircuit.rs exists in the corrected PR range.
2 #[reduction(...)] macro present PASS — reduction is registered with vertex/edge overhead expressions.
3 ReductionResult impl present PASS — ReductionHamiltonianPathToHamiltonianCircuit implements ReductionResult.
4 ReduceTo impl present PASS — HamiltonianPath<SimpleGraph> implements ReduceTo<HamiltonianCircuit<SimpleGraph>>.
5 Test link present PASS — rule module links the dedicated unit-test file.
6 Test file exists PASS — dedicated test file exists.
7 Closed-loop test present PASS — closed-loop test plus five focused boundary/extraction tests.
8 Registered in rules/mod.rs PASS — module and canonical-example aggregation are registered.
9 Canonical rule example registered PASS — fixture builder is included by canonical_rule_example_specs().
10 Example-db lookup tests exist PASS — generic coverage and solution-pair consistency tests exercise the example.
11 Paper reduction-rule entry PASS — fixture-driven theorem and tutorial are present.
12 Blacklisted generated-file check PASS — no prohibited generated paths appear in the six-file diff.

Build Status

  • make test: PASS — 5,437 library tests, 75 integration tests, CLI/unit suites, 151 rustdoc tests, and remaining workspace suites passed.
  • make clippy: PASS — all targets with ilp-highs and -D warnings.

Semantic Review

  • Construction: OK — for n >= 2, copies every source edge and adds one fresh universal vertex adjacent to all old vertices.
  • Small instances: OK — empty and singleton source instances map to K3, preserving satisfiability and unique extraction.
  • extract_solution: OK — rotating at and deleting the universal vertex returns exactly the source path for arbitrary rotations and orientations.
  • Overhead: OK — exact normal sizes are n + 1 vertices and m + n edges; registered n + 3 and m + n + 3 are safe bounds across both branches.
  • Examples/tests: OK — cover feasible/infeasible boundaries, rotations, reversal, disconnected/star cases, self-loops, and repeated edges.
  • Paper proof: OK — forward extension and reverse rotate/delete arguments are logically sound and representation edge cases are documented.
  • Review context: NOTE — the generated implementation packet compared this stacked PR to main. Review was correctly scoped to a9067297..3345b5d (six files). This is a pipeline-context defect, not a PR defect.

Issue Compliance

# Check Status
1 Source/target match OK
2 Reduction algorithm matches OK
3 Solution extraction matches OK
4 Correctness preserved OK
5 Overhead expressions match OK
6 Example matches OK

Summary

  • 12/12 structural checks passed.
  • 6/6 issue compliance checks passed.
  • No PR implementation failures or issues found.

Quality Check

Quality Review

Design Principles

  • DRY: OK — no duplicated logic warranting a shared helper.
  • KISS: OK — direct two-branch construction without unnecessary abstraction.
  • HC/LC: OK — reduction, registration, example, paper, and tests remain in established project locations.

Test Quality

  • Naive test detection: OK.
  • Non-trivial closed-loop test verifies exact target structure.
  • Extraction tests cover cyclic rotation and reversal.
  • Boundary tests cover empty, singleton, and both two-vertex feasibility cases.
  • Negative tests cover connected star and disconnected instances.
  • Representation tests verify self-loop and parallel-edge preservation.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

None.

Minor (Nice to Have)

None.

Summary

  • No quality issues found in the actual six-file PR range.

Agentic Feature Tests

Feature: HamiltonianPath -> HamiltonianCircuit
Mode: Blind CLI downstream-user flow
Verdict: Pass with one medium-severity pre-existing issue
Critical Issues: 0

Check Result
pred list model catalog Pass — both endpoints listed
pred list --rules Pass — direct rule listed
pred show both endpoints Pass — incoming/outgoing rule displayed
pred create --example HamiltonianPath Pass — valid source created
Solve source example Pass — Or(true) with valid path
Reduce to HamiltonianCircuit Pass — exact one-step bundle produced
Solve feasible reduced bundle Pass — target circuit extracted to valid source path
Evaluate target/source witnesses Pass — both Or(true)
Rule-specific canonical example Pass — reduction and solving completed correctly

Functional verification

The model example reduced from 6 vertices/8 edges to 7 vertices/14 edges by adding one universal vertex. Bundle solving returned target circuit [0, 1, 3, 5, 6, 4, 2], extracted source path [4, 2, 0, 1, 3, 5], and both evaluations returned Or(true). The rule-specific canonical example also reduced and solved correctly.

Issues Found

  1. [Medium][confirmed][pre-existing] Infeasible reduced bundles error instead of returning Or(false).

    A disconnected source and its extracted target both solve directly as Or(false), but solving the reduction bundle exits 1 with:

    Error: Bundle solving requires a witness-capable target problem and witness-capable reduction path; HamiltonianCircuit only supports aggregate-value solving.
    

    Source inspection confirms the same unconditional missing-config gate exists at base commit a9067297; PR Fix #1097: HamiltonianPath to HamiltonianCircuit #1106 did not introduce this generic CLI limitation, but its new rule exposes it for infeasible instances.

Discoverability and Documentation

  • Discoverability: Good — visible through rule listing and both endpoint detail views.
  • Setup/functionality: Pass for the documented feasible workflow.
  • Documentation: Partial — general create/reduce/solve flows are documented, but there is no rule-specific CLI walkthrough and infeasible-bundle behavior is not explained.
  • Suggested improvement: document the infeasible decision-bundle limitation separately from this PR or make bundle solving return the equivalent aggregate false result.

Generated by review-pipeline

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant