Fix #1098: HamiltonianCircuit to Satisfiability

[isPANN]

Summary

Add a witness-preserving vertex-position CNF encoding from Hamiltonian Circuit to Satisfiability.

Fixes #1098

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 97.94%. Comparing base (a906729) to head (46303b6).

Additional details and impacted files

@@                 Coverage Diff                 @@
##           1075-growth-domain    #1107   +/-   ##
===================================================
  Coverage               97.94%   97.94%           
===================================================
  Files                    1051     1051           
  Lines                  110605   110605           
===================================================
  Hits                   108327   108327           
  Misses                   2278     2278           

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[isPANN]

Implementation Summary

Changes

• Added a witness-preserving HamiltonianCircuit<SimpleGraph> -> Satisfiability reduction using the vertex-position permutation encoding, including the fixed contradictory target for graphs with fewer than three vertices.
• Registered safe symbolic overheads for SAT variables, clauses, and literal occurrences, plus canonical example-db data for the five-cycle-with-chord instance.
• Added ten focused tests covering closed-loop extraction, exact target structure, both circuit orientations, infeasible and small instances, isolated vertices, loops, parallel edges, overhead evaluation, and canonical example metrics.
• Added the fixture-driven Typst paper theorem/tutorial and the Velev-Gao 2009 reference.

Deviations from Plan

• This base revision has no tracked src/example_db/fixtures/examples.json; examples are generated in memory and exported to ignored docs/paper/data/examples.json. The implementation used that repository-supported path and verified the generated example data directly.
• PR Fix #1098: HamiltonianCircuit to Satisfiability #1107 is stacked on 1075-growth-domain, whose tip is the requested base commit a9067297, so unrelated changes from that base branch are excluded from this PR.

Open Questions

• None.

Verification

• Mathematical verification: 10,549 constructor checks, 143,646 independent adversary checks, and 1,100 structural cross-comparisons with zero disagreements.
• make test clippy: passed.
• make paper: passed.
• make coverage: 97.94% overall; new reduction and test files are 100% covered.

[isPANN]

Agentic Review Report

Review scope: stacked PR range a9067297..b3e5c5e (5 files).

Structural Check

Structural Review: rule HamiltonianCircuit → Satisfiability

Structural Completeness

#	Check	Status
1	Rule file exists	PASS — src/rules/hamiltoniancircuit_satisfiability.rs
2	#[reduction(...)] macro present	PASS — safe symbolic bounds provided for variables, clauses, and literals
3	ReductionResult implementation present	PASS
4	ReduceTo<Satisfiability> implementation present	PASS
5	Unit-test module link present	PASS
6	Rule test file exists	PASS — 10 focused tests
7	Closed-loop test present	PASS
8	Registered in src/rules/mod.rs	PASS
9	Canonical rule example registered	PASS — five-cycle plus chord, with source and target witnesses
10	Example-database lookup/build coverage exists	PASS — generic uniqueness, consistency, and direct-reduction coverage tests exercise the registration
11	Paper reduction-rule entry present	PASS — includes construction, correctness proof, variable mapping, extraction, tutorial example, and Velev–Gao reference
12	Blacklisted generated-file check	PASS — none of the four prohibited generated paths occurs in the corrected five-file PR range

Build Status

• make test: INCOMPLETE — the workspace-wide run was interrupted after prolonged shared Cargo/resource contention. Before interruption, the library suite passed 5441/5441, the main integration suite passed 75/75, the CLI integration batch passed 330/330, pred_sym passed 17/17, and the macro crate passed 26/26; all observed doctests were passing when interrupted.
• make clippy: NOT RUN — the sequential make test clippy command did not reach clippy before interruption.
• Limitation: this is an incomplete workspace-wide build verdict, not an observed code failure. No additional expensive checks were started.

Semantic Review

• Correctness preservation: OK — for n ≥ 3, the two exactly-one clause families force an n × n permutation matrix. Cyclic successor clauses forbid every equal or nonadjacent ordered pair, including the last-to-first transition. Thus satisfying assignments correspond exactly to Hamiltonian circuits. For n < 3, both the source model and the fixed contradictory CNF are infeasible.
• Solution extraction: OK — scanning each position for its unique true vertex reconstructs a permutation of source length n; the successor clauses guarantee every consecutive and closing edge.
• Overhead accuracy: OK — for n ≥ 3, the exact permutation-family count is 2n + n²(n−1) clauses and 2n³ literals. At most n³ forbidden-successor clauses contribute at most 2n³ literals. Therefore the declared bounds n²+1, 2n+n²(n−1)+n³+2, and 4n³+2 safely cover both the general construction and the (1 variable, 2 clauses, 2 literals) small-instance branch.
• Example quality: OK — the five-cycle-plus-chord example provides valid source/target data, demonstrates the matrix encoding, identifies representative clauses, verifies extraction, and explains witness multiplicity.
• Paper proof: OK — both directions are logically complete, the cyclic closing edge is explicit, extraction matches the implementation, and the direct Velev–Gao absolute-encoding reference is included.
• Required test coverage: ISSUE — the linked issue explicitly requires exhaustive enumeration of all simple graphs through four vertices. The added tests cover selected positive/negative, disconnected, small, loop, parallel-edge, orientation, extraction, metric, and overhead cases, but do not enumerate every simple graph through n = 4.
• Reproduction classification: confirmed by direct inspection of the dedicated test module; no exhaustive graph-enumeration test is present.

Issue Compliance

#	Check	Status
1	Source/target match issue	OK — HamiltonianCircuit<SimpleGraph> → Satisfiability
2	Reduction algorithm matches	OK — fixed contradiction for n < 3, vertex-position variables, both one-hot families, and cyclic forbidden-successor clauses
3	Solution extraction matches	OK — reads the unique true vertex at each position
4	Correctness preserved	OK — verified directly in both directions
5	Overhead expressions match	OK — expressions exactly match the requested safe bounds
6	Example and citation match	OK — five-cycle-plus-chord YES example, path-five NO test, and direct Velev–Gao 2009 reference
7	Required exhaustive test matrix	ISSUE — no exhaustive all-simple-graphs-through-four test is present

Summary

• 12/12 structural checks passed.
• 6/7 issue-compliance checks passed.
• Findings:
  • The issue-mandated exhaustive simple-graph test through four vertices is missing.
  • The full make test clippy verdict is incomplete because the shared, resource-contended workspace run was interrupted during doctests; all completed suites passed, and clippy was not reached.

---

Quality Check

Quality Review

Design Principles

• DRY: OK — The two one-hot clause families are symmetric but remain clearer as direct loops; extracting an abstraction would add indirection without meaningful reuse.
• KISS: OK — The reduction directly implements the vertex-position encoding with straightforward control flow and no unnecessary abstraction.
• HC/LC: OK — Construction, solution extraction, registration, and canonical-example logic remain focused on this single reduction.

Test Quality

• Naive test detection: ISSUE
  • The nontrivial NO-instance tests enumerate only permutation-derived assignments (src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs:76 and src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs:104). They do not establish that the target formula is unsatisfiable over all Boolean assignments. A defect in the one-hot clauses could admit a non-permutation assignment without failing these tests. Add an end-to-end normal-branch NO case small enough for BruteForce::find_witness()—for example, a three-vertex path—and assert that no SAT witness exists.
  • test_five_cycle_with_chord_structure depends on clauses occupying exact vector indices (src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs:54). Clause ordering is not part of the reduction contract, so these assertions make harmless construction reordering break the test. Prefer semantic containment or family-count assertions.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

• Add an end-to-end unsatisfiable test for the ordinary n >= 3 encoding that searches the full target assignment space, rather than checking only assignments produced from source permutations (src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs:76).
• Reproduction classification: confirmed by direct inspection; the cited NO tests only evaluate assignments generated from vertex permutations, not all Boolean assignments.

Minor (Nice to Have)

• Replace clause-index assertions with order-independent semantic assertions (src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs:54).
• Reproduction classification: confirmed; the test reads fixed clause-vector positions.

Summary

• Important: The normal reduction branch lacks an end-to-end target-unsatisfiability test capable of detecting malformed one-hot constraints.
• Minor: Several structural assertions are unnecessarily coupled to clause insertion order.

---

Agentic Feature Tests

Feature: HamiltonianCircuit → Satisfiability
Mode: Blind, ephemeral downstream-user persona
Verdict: PASS
Critical issues: 0
Repository modifications: None

Test Profile

• Role: CLI user validating a canonical HamiltonianCircuit instance and its SAT reduction.
• Use case: Discover both models and their reduction, create and solve the canonical source, reduce it to Satisfiability, solve the bundle, evaluate both witnesses, and verify the extracted circuit.
• Expected outcome: The source and target are satisfiable, and the extracted witness is a valid Hamiltonian circuit.
• Documentation surface: README.md and docs/src/cli.md, isolated under an ephemeral /tmp directory.
• Review range: a9067297..b3e5c5e.

Results

Area	Result	Evidence
Discoverability	Pass	pred list, pred list --rules, and both pred show commands expose the models and direct reduction.
Setup	Pass	Temporary-target CLI build completed successfully; pred --version returned pred 0.6.0.
Source creation	Pass	Canonical HamiltonianCircuit example created successfully.
Source solving	Pass	Brute-force returned Or(true) with circuit [0,1,2,5,4,3].
Reduction	Pass	A direct one-step HamiltonianCircuit → Satisfiability bundle was created.
Reduced solving	Pass	Bundle solving through the registered SAT → NAE-SAT → ILP path returned Or(true).
Extraction	Pass	Extracted circuit [2,5,3,4,1,0] evaluated to Or(true).
Target evaluation	Pass	The returned 36-variable SAT assignment evaluated to Or(true).
Circuit verification	Pass	The extracted witness visits every vertex once and all six cyclic edges exist.
Canonical rule example	Pass	Its generated 25-variable, 175-clause target exactly matched a fresh reduction of its source.

Commands and Results

Command	Result
cargo build -p problemreductions-cli --bin pred with temporary CARGO_TARGET_DIR	Exit 0; completed in 6m56s
pred --version	Exit 0; pred 0.6.0
pred list	Exit 0; HamiltonianCircuit and Satisfiability present
pred list --rules	Exit 0; direct HamiltonianCircuit/SimpleGraph → Satisfiability rule present
pred show HamiltonianCircuit	Exit 0; Satisfiability listed among 10 outgoing reductions
pred show Satisfiability	Exit 0; HamiltonianCircuit listed among incoming reductions
pred create --example HamiltonianCircuit -o hc.json	Exit 0; canonical six-vertex source created
pred solve hc.json --solver brute-force	Exit 0; Or(true), witness [0,1,2,5,4,3]
pred reduce hc.json --to Satisfiability -o hc-sat-bundle.json	Exit 0; one-step bundle, 36 variables and 300 clauses
pred solve hc-sat-bundle.json	Exit 0; Or(true), extracted witness [2,5,3,4,1,0]
pred evaluate sat-target.json --config <returned-assignment>	Exit 0; Or(true)
pred evaluate hc.json --config 2,5,3,4,1,0	Exit 0; Or(true)
Independent cyclic-edge check	All six edges present; all vertices distinct and covered
pred create --example HamiltonianCircuit --to Satisfiability	Exit 0; canonical five-vertex rule source created
Same command with --example-side target	Exit 0; canonical SAT target created
Fresh reduction compared with canonical target	Exact JSON match
Canonical rule bundle solve	Exit 0; Or(true), extracted witness [4,3,2,1,0]

Findings

No confirmed functional, setup, safety, or extraction defects.

• Informational — feature-specific documentation: The generic CLI guide documents all necessary commands, including canonical rule examples, reduction bundles, and bundle solving. It does not include a worked HamiltonianCircuit → Satisfiability transcript, but this did not prevent discovery or successful use.
• Classification: Confirmed documentation enhancement opportunity; non-blocking.

Expected vs. Actual

The expected outcome was fully met. Both canonical workflows produced satisfiable target formulas, solving mapped the result back to valid Hamiltonian circuits, and independent evaluation confirmed both the SAT assignment and extracted source witness.

---

Generated by review-pipeline