[Rule] HamiltonianCircuit to Satisfiability

[isPANN]

Source

HamiltonianCircuit/SimpleGraph

Target

Satisfiability

Motivation

This direct CNF encoding connects Hamiltonian Circuit to the SAT hub without passing through an optimization model. It is a canonical example of exposing a combinatorial witness through executable logical constraints.

Reference

Cook, S. A. “The Complexity of Theorem-Proving Procedures,” STOC 1971; Garey and Johnson, Computers and Intractability, 1979; Velev and Gao, “Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles,” SARA 2009. Velev and Gao's absolute encoding uses one predicate for each vertex-position pair and adjacency constraints excluding impossible consecutive vertices, matching the construction below. Cook's theorem supports the generic NP-to-CNF-SAT claim but does not state this position encoding.

Reduction Algorithm

Given G=(V,E), V={0,...,n-1}:

1. If n<3, output the fixed contradiction (z) AND (not z), matching the source model's explicit rejection of circuits with fewer than three vertices.
2. Otherwise create Boolean variable x[v,p] meaning vertex v occurs at cyclic position p, for all v,p in {0,...,n-1}.
3. For every position p, add one clause requiring some vertex at p, and pairwise clauses forbidding two vertices at p.
4. For every vertex v, add one clause requiring v in some position, and pairwise clauses forbidding v in two positions.
5. For every cyclic successor pair p,q=(p+1) mod n and every ordered pair (u,v) that is equal or is not an edge, add not x[u,p] OR not x[v,q].
6. Extract the circuit by reading the unique true vertex at each position.

The first four clause families force a permutation of the vertices. The last family accepts exactly those permutations whose consecutive pairs, including the closing pair, are graph edges. Isolated or disconnected vertices therefore make the formula unsatisfiable whenever they prevent a circuit. Self-loops cannot supply a successor because equal consecutive vertices are explicitly forbidden, and parallel copies of an edge do not change whether the corresponding successor pair is allowed.

Size Overhead

Safe upper bounds, including the fixed small-instance contradiction:

Target metric	Formula
num_vars	num_vertices * num_vertices + 1
num_clauses	2 * num_vertices + num_vertices * num_vertices * (num_vertices - 1) + num_vertices^3 + 2
num_literals	4 * num_vertices^3 + 2

Validation Method

• Exhaust every simple graph through four vertices.
• Brute-force both vertex permutations and SAT feasibility and compare the results.
• Separately test the n<3 contradiction and extraction of both circuit orientations.

Example

1. Source YES instance: five-cycle 01,12,23,34,40 plus chord 02.
2. Construction: create 25 variables x[v,p] and the four uniqueness/adjacency clause families above. Representative forbidden-successor clause: because {0,3} is not an edge, every position p contains not x[0,p] OR not x[3,p+1].
3. Target witness: set x[0,0],x[1,1],x[2,2],x[3,3],x[4,4] true and all other variables false.
4. Round trip: the assignment satisfies every clause and extracts cycle 0-1-2-3-4-0. Swapping positions of vertices 2 and 3 violates a successor clause, so the example detects missing adjacency constraints.
5. Source NO instance: the five-vertex path 01,12,23,34. Its endpoint 0 has only one distinct neighbor, but any encoded cyclic permutation would give it two distinct consecutive neighbors. Thus every placement of 0 violates a forbidden-successor clause on one side, and the target CNF is unsatisfiable.

BibTeX

@inproceedings{Cook1971,
  author = {Cook, Stephen A.},
  title = {The Complexity of Theorem-Proving Procedures},
  booktitle = {Proceedings of the Third Annual ACM Symposium on Theory of Computing},
  pages = {151--158},
  year = {1971},
  doi = {10.1145/800157.805047}
}

@book{GareyJohnson1979,
  author = {Garey, Michael R. and Johnson, David S.},
  title = {Computers and Intractability: A Guide to the Theory of NP-Completeness},
  publisher = {W. H. Freeman},
  year = {1979}
}

@inproceedings{VelevGao2009,
  author = {Velev, Miroslav N. and Gao, Ping},
  title = {Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles},
  booktitle = {Proceedings of the Eighth Symposium on Abstraction, Reformulation and Approximation},
  pages = {159--166},
  publisher = {AAAI Press},
  year = {2009}
}

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	pred path HamiltonianCircuit Satisfiability --json reports no existing reduction path.
Non-trivial	✅ Pass	The construction introduces an n × n position matrix and three non-trivial CNF constraint families.
Correctness	✅ Pass	The references exist and the stated scope is accurate; direct exhaustive checking also agrees with the source semantics through four vertices.
Completeness	⚠️ Warn	The construction works on the traced edge cases, but the issue does not document them, and the cited works do not state this exact one-hot position encoding.
Well-written	✅ Pass	All required sections and target size metrics are present; the algorithm and extraction map are implementable.

Overall: 4 passed, 0 failed, 1 warning

---

Usefulness

Both endpoint variants resolve in the current catalog:

• HamiltonianCircuit { graph: SimpleGraph }, with size fields num_vertices and num_edges.
• Satisfiability, with size fields num_vars, num_clauses, and num_literals.

There is currently no HamiltonianCircuit → Satisfiability path, so this is a new connection to the SAT hub rather than a dominated direct edge.

Non-trivial

This is a genuine structural transformation. It creates Boolean variables indexed by both source vertices and cyclic positions, enforces a permutation with at-least-one and pairwise at-most-one clauses, and then filters permutations with cyclic successor clauses. Extraction decodes the unique vertex at each position.

Correctness

• Cook's 1971 paper exists with the stated title, author, venue, year, pages, and DOI. Theorem 1 covers every language accepted by a polynomial-time nondeterministic machine, and its proof explicitly constructs a CNF formula satisfiable exactly when the machine accepts. This supports the generic NP-to-CNF-SAT claim, but not this particular position encoding: ACM record, paper text.
• Garey and Johnson (1979), Appendix A1, entry GT37 (book pp. 198–199), defines HAMILTONIAN CIRCUIT for an unrestricted graph G=(V,E) and cites Karp's NP-completeness reduction. It does not present the direct encoding proposed here. This matches the issue's explicit disclaimer that the position encoding is not attributed verbatim to Cook.
• Independent check: /tmp/validate_reduction_issue_examples.py exhaustively compared Hamiltonian-circuit feasibility with the generated CNF for every loop-free undirected graph on n = 0,1,2,3,4; all cases passed. The five-vertex worked example also passed.

The overhead bounds are safe. For n ≥ 3, the exact worst-case counts under the stated pairwise encoding are at most n² variables, 2n + n²(n-1) + n³ clauses, and 4n³ literal occurrences. The issue's extra +1 variable / +2 clauses / +2 literals cover the fixed contradiction used for n < 3.

Completeness

Literature scope. Cook's theorem has no graph-side precondition, and Garey–Johnson GT37 defines the source on an arbitrary graph. However, neither cited source states or proves this exact one-hot positional construction. The issue gives a sound self-contained argument, but a direct encoding citation should be added so the literature check can verify the same construction rather than only the generic existence result.

Codebase scope. SimpleGraph::new can represent the empty graph, isolated vertices, disconnected graphs, self-loops, and parallel edges. The Hamiltonian-circuit model explicitly rejects every instance with fewer than three vertices.

Hand traces beyond the worked example:

1. n = 0, 1, or 2. Step 1 emits (z) ∧ (¬z), which is a well-formed unsatisfiable SAT instance. The source evaluator also returns false before inspecting edges, so feasibility is preserved.
2. An isolated vertex with n ≥ 3. The row/column clauses force that vertex into exactly one cyclic position. For either adjacent cyclic position, every distinct successor pair involving it is a non-edge and is forbidden, so the CNF is unsatisfiable, matching the source.
3. Self-loops and parallel edges. A satisfying position matrix is a permutation, so consecutive vertices are distinct; self-loops cannot create a false circuit. Parallel edges have the same has_edge(u,v) truth value as one edge, matching the source evaluator. On K3, setting x[0,0], x[1,1], and x[2,2] true satisfies the formula and extracts the valid cycle, regardless of extra loops or duplicate edges.

These cases work, but the issue body does not say that loops, duplicate edges, isolated vertices, and disconnected graphs are handled. Per the quality-gate rubric, this is a warning rather than a failure.

Well-written

All required template sections are substantive. Symbols G, V, E, and n are defined before use; the overhead metric names match the target model; the example has five vertices, contains both allowed and forbidden successor pairs, gives a concrete SAT witness, and demonstrates a mutation that violates the encoding.

Recommendations

• Add one sentence documenting behavior for n < 3, isolated/disconnected graphs, self-loops, and parallel edges.
• Add a direct reference for a Hamiltonian-cycle SAT encoding. For example, Zhou (CP 2024) explicitly discusses position/distance SAT encodings and their correctness, although its encoding is not identical to this pairwise one-hot formulation: paper.
• Add a Garey–Johnson BibTeX entry because the Reference section cites the book but the BibTeX section currently contains only Cook.

[isPANN]

Rule Fix

Diagnosis:

• Example correctness/completeness: the body had a valid YES example but no concrete NO example, so it did not exercise rejection of a non-Hamiltonian graph.
• Literature traceability: Cook (1971) establishes the generic NP-to-CNF construction, and Garey--Johnson defines Hamiltonian Circuit, but neither source states this direct one-hot position encoding.
• Edge-case documentation: the construction handled small, disconnected, isolated, self-loop, and parallel-edge cases, but the body did not explain why.

Literature:

• Velev and Gao, Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles (SARA 2009), directly describes the absolute permutation encoding with one predicate per vertex-position pair and constraints excluding impossible adjacent vertices. The issue's construction agrees with that canonical encoding.
• Zhou, Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination (CP 2024), surveys Hamiltonian-cycle SAT encodings and cites Velev--Gao as the absolute permutation encoding.

Changes:

• Added Velev--Gao as a direct construction reference and supplied its BibTeX entry, plus the missing Garey--Johnson entry.
• Added a concrete five-vertex path NO instance and explained why its CNF is unsatisfiable.
• Documented the behavior for n < 3, isolated/disconnected vertices, self-loops, and parallel edges.
• Left the reduction algorithm and overhead formulas unchanged because testing confirmed them.

Smoke test:

• 178 checks passed across all required buckets on both the original construction and the post-edit re-smoke: 76 exhaustive simple-graph feasibility comparisons through four vertices, 11 extracted SAT witnesses, 5 overhead spot-checks, and 81 target-validity checks, plus the dedicated YES, NO, and small-instance cases.
• Key confirming instances: the five-cycle with chord extracted 0-1-2-3-4-0; the five-vertex path encoded UNSAT; every graph with fewer than three vertices encoded to the fixed contradiction.

[isPANN]

Issue Quality Check — Rule (Re-check)

Check	Result	Details
Usefulness	✅ Pass	pred path HamiltonianCircuit Satisfiability --json reports no existing reduction path.
Non-trivial	✅ Pass	The construction introduces an n × n position matrix and complete permutation and cyclic-adjacency CNF constraints.
Correctness	✅ Pass	All three references exist, their claimed scopes are accurate, and the direct Velev--Gao construction agrees with the issue.
Completeness	✅ Pass	The direct encoding applies to the full source model, and the body now covers all traced codebase edge cases.
Well-written	✅ Pass	Every required section, metric, extraction step, YES witness, mutation, and concrete NO instance is present and implementable.

Overall: 5 passed, 0 failed, 0 warnings

Previously: 4 passed, 0 failed, 1 warning. The earlier completeness warning is resolved by the direct construction citation and explicit edge-case discussion.

---

Usefulness

Both endpoint variants resolve in the current catalog:

• HamiltonianCircuit { graph: SimpleGraph }, with size fields num_vertices and num_edges.
• Satisfiability, with size fields num_vars, num_clauses, and num_literals.

There remains no registered HamiltonianCircuit → Satisfiability path, so this rule adds a novel connection to the SAT hub.

Non-trivial

The rule is a genuine structural transformation. It creates one Boolean variable for every vertex-position pair, two exactly-one constraint families that force a permutation, and cyclic forbidden-successor clauses. The extraction map decodes a SAT assignment back into the vertex order of a Hamiltonian circuit.

Correctness

• Cook's 1971 paper exists with the stated metadata and establishes the generic polynomial CNF construction for nondeterministic polynomial-time languages; the issue accurately says that Cook does not state this particular position encoding: DOI.
• Garey and Johnson's 1979 book exists and includes Hamiltonian Circuit among its NP-complete graph problems. The issue uses it only for background, not as the source of the direct encoding.
• Velev and Gao's SARA 2009 paper explicitly studies the absolute SAT encoding of Hamiltonian cycles: one predicate for each object and possible permutation position, with adjacency constraints requiring consecutive permutation elements to be graph neighbors. This supports the issue's exact construction family: paper, independent later bibliography and survey context.

The clause bounds also agree with direct counting. For n ≥ 3, there are n² variables; at most 2n + n²(n-1) + n³ clauses; and at most 4n³ literal occurrences. The additive small-instance terms safely cover (z) ∧ (¬z).

Independent smoke testing passed 178 bucket checks per run, including all 76 simple graphs through four vertices, 11 extracted target witnesses, five overhead checks, and 81 CNF structural-validity checks.

Completeness

Literature scope. The absolute permutation encoding takes an HCP graph directly and imposes the permutation and graph-neighbor constraints; it does not require connectedness, minimum degree, or another hidden graph precondition. The issue's self-contained construction likewise handles every graph accepted by the source representation.

Codebase scope. SimpleGraph::new permits empty graphs, isolated vertices, disconnected graphs, self-loops, and parallel edges; HamiltonianCircuit explicitly rejects n < 3. The edited issue now states the corresponding behavior:

1. For n = 0, 1, 2, Step 1 emits the fixed contradiction, matching the source evaluator.
2. An isolated vertex is forced into a position but has no allowed predecessor or successor, so the target is unsatisfiable.
3. Disconnected graphs are rejected unless a single cycle spans every vertex, which is impossible across components.
4. Equal consecutive vertices are explicitly forbidden, so self-loops cannot create a false witness.
5. Parallel copies do not change has_edge(u,v), so they do not change either source or target feasibility.
6. On K3, the cyclic assignment 0,1,2 satisfies the encoding, confirming the positive boundary case.

These traces match how existing HamiltonianCircuit reductions special-case n < 3 and otherwise use the source graph's adjacency relation.

Well-written

All required sections are substantive. Symbols G, V, E, n, v, and p are defined before use; the overhead fields match the target getters; construction and extraction are step-by-step. The five-cycle-plus-chord YES example includes a concrete SAT witness and a falsifying mutation, while the five-vertex path supplies a concrete NO case with an explicit unsatisfiability argument.

Recommendations

• No blocking or warning-level changes remain.