Hamiltonian \(s\)–\(t\) Paths in Solid Grid Graphs
are Decided in Polynomial Time,
an Algorithm with a Lean 4 Proof

Z. Zzyzek
Video Paper Code Lean Proof Demo

A narrated eighteen-minute explainer. The problem, Sheffield's flips and heights, the phase and its certificate, phantom endpoints, holes and vortices, flip classes, and one complete run.

  • 0:00 Title
  • 0:11 The problem
  • 0:57 Earlier results
  • 1:38 Pieces and flips
  • 2:35 Heights
  • 4:28 The phase and the certificate
  • 7:43 Phantom endpoints and deletion walks
  • 9:21 Inner endpoints become holes
  • 9:50 Vortices
  • 10:08 The slit height
  • 11:17 Quadrant labels and the potential
  • 12:50 Two vortices
  • 13:33 Flip classes and the class search
  • 16:08 One complete run
  • 17:21 Closing

Abstract

A grid graph is a finite set of lattice points with every unit edge between two of its points. It is solid when it has no holes. We give an algorithm that decides, for a solid grid graph \(V\) and two distinct points \(s, t \in V\), whether \(V\) has a Hamiltonian path from \(s\) to \(t\). Correctness and a polynomial step bound are proved in Lean 4 with Mathlib. The main theorem decideHamPath_main states that the algorithm returns true exactly when a Hamiltonian \(s\)–\(t\) path exists, and that it takes at most \(5\,220\,000\,(|V|+3)^6\) steps of explicit cost functions. Its only axioms are propext, Classical.choice and Quot.sound. The algorithm extends Sheffield's height-function algorithm for Hamiltonian cycles. Each endpoint gets a phantom edge to a missing neighbour, which moves its degree-one defect off the vertex set. An endpoint with all eight king neighbours present is deleted and becomes a hole, and its degree-one defect is a vortex of the height field. A slit height and a quadrant label give a potential that rises along every arc, which replaces the height function in Sheffield's counting argument. The count behind a stuck phase is proved with chained rows, straight runs of rows through several cuts.

A Hamiltonian s-t path on a 197-point solid grid graph
A Hamiltonian path from \(s\) to \(t\) on a solid grid graph with 197 points, found by the algorithm. The path is coloured along its length, from blue at \(s\) to orange at \(t\). Both endpoints are inner, so the run goes through the two-hole case.

The Problem

A grid graph is given by a finite set \(V \subset \mathbb{Z}^2\) of lattice points. Its edges are the unit segments between two points of \(V\). A Hamiltonian \(s\)–\(t\) path visits every point of \(V\) exactly once, starting at \(s\) and ending at \(t\). For general grid graphs, deciding whether such a path exists is NP-complete (Itai, Papadimitriou and Szwarcfiter, 1982). A grid graph is solid when it has no holes, that is, when every missing point can reach the outside of \(V\) by king moves through missing points.

A solid and a non-solid grid graph
Left, a solid grid graph. Right, not solid. The red point is missing, and all eight of its king neighbours (purple dashed box) are in \(V\), so it cannot reach the outside.
A Hamiltonian path and its phantom edges
Left, a Hamiltonian path from \(s\) to \(t\). Right, the same path with two phantom edges (dashed) to the missing points \(p\) and \(q\), which give \(s\) and \(t\) degree 2.

Itai, Papadimitriou and Szwarcfiter posed the solid case in 1982, and it has been listed as open since (Keshavarz-Kohjerdi 2011, Keshavarz-Kohjerdi and Bagheri 2016). For Hamiltonian cycles in solid grid graphs, Umans and Lenhart (1997) gave a polynomial algorithm, and Sheffield (2000) gave a second one based on height functions. Sheffield's introduction remarks that similar results hold for paths with fixed endpoints. This work gives a written proof of the path case and checks it in Lean.

The Result

Theorem (decideHamPath_main). Let \(V \subset \mathbb{Z}^2\) be finite and solid, and let \(s \ne t\) be points of \(V\). Then decideHamPath V s t = true if and only if there is an edge set \(H\) of the grid graph on \(V\) with degree 1 at \(s\) and \(t\), degree 2 at every other point, and one connected component. The cost decideHamPathCost V s t is at most \(5\,220\,000\,(|V|+3)^6\). 

theorem SolidGridHam.HP.decideHamPath_main {V : Finset Pt} {s t : Pt}
    (hs : Solid V) (hst : s ≠ t) (hsV : s ∈ V) (htV : t ∈ V) :
    (decideHamPath V s t = true ↔ ∃ H, IsFactor V (dST s t) H ∧ ncomp V H = 1) ∧
      decideHamPathCost V s t ≤ 5220000 * (V.card + 3) ^ 6

An edge set with these degrees and one component is exactly a Hamiltonian \(s\)–\(t\) path. An endpoint is inner when all eight of its king neighbours lie in \(V\). The algorithm dispatches on which endpoints are inner, and each case has its own proved bound.

\(s\)\(t\)Lean theoremBound
not innernot innerboundaryEndpoints_main\(1\,060\,000\,(|V|+3)^4\)
exactly one inneroneHoleCase_main\(2\,513\,000\,(|V|+3)^5\)
innerinnertwoHoleCase_main\(5\,217\,000\,(|V|+3)^6\)
all cases, plus the dispatchdecideHamPath_main\(5\,220\,000\,(|V|+3)^6\)

Running time is stated through explicit cost functions written beside each algorithm in Lean. Primitive operations on finite sets (membership, insertion, a cell flip) are charged a constant. The bound is proved for these functions, not for a machine model, and a machine implementation may have a larger exponent, though still polynomial.

The Starting Point, Sheffield's Algorithm

Sheffield's algorithm decides Hamiltonian cycles in solid grid graphs. It starts from any 2-factor, a set of edges with degree 2 at every point, which splits \(V\) into disjoint cycles called pieces. It then flips unit cells, toggling their four sides, to join pieces one at a time. A height function on the cells orders these flips so that the search cannot run in circles. When no more pieces can be joined, a locally checkable certificate proves that no 2-factor has fewer pieces, so no Hamiltonian cycle exists. In a solid grid graph every 2-factor can be reached from every other by flips, so one run decides the question.

The ideas of the algorithm in four pictures
(a) A 2-factor of the \(4 \times 4\) block with two pieces (blue, red). (b) Flipping the yellow cell joins them into one cycle. (c) A path from \(s\) to \(t\) with a phantom edge at each endpoint (dashed) to a missing point (red circle), so that \(s\) and \(t\) have degree 2, as in a cycle. (d) An inner endpoint \(t\) deleted, leaving a hole (grey cells). Two path factors differ by the purple cycle around the hole, and no flip changes how many such cycles go around it.

The path algorithm reduces the path problem to situations where this machinery still works. Every component exists for one of two reasons. Either it restores a hypothesis of Sheffield's argument that a path endpoint breaks, or it pays for that repair with a bounded amount of branching.

The outcomes of one phase step
The outcomes of one phase step, with a height in every cell. (a) Merge, a yellow merging cell joins two pieces. (b) Stuck, the row of the only critical cell falls into a square that is not a cell (red cross). (c) Odd, a row of odd length is lowered, which joins two pieces. (d, e) Bridge, flipping the last cell of an even row splits a piece, and the phase continues. (f, g) Twist, at a leaf with an inner endpoint, where the whole row is lowered.

Each round of the loop is a phase and a reduction. A phase joins pieces by flipping a merging cell, and when none exists it builds bridges, flips that split a piece to expose a merging cell. The reduction then undoes or lowers the bridges, and the round ends with one piece fewer. If a phase is stuck, the certificate proves that no factor has fewer pieces. Sheffield's count for a stuck phase has a gap, which this work closes with chained rows, straight runs of rows through several cuts (stuck_minimal).

Endpoints, Phantoms and Deletion Walks

A Hamiltonian path has degree 1 at \(s\) and \(t\), while Sheffield's local rules and his height function both use degree 2 at every point. The repair is a phantom. If an endpoint has a missing lattice neighbour \(p\), the edge from the endpoint to \(p\) is added. The endpoint then has degree 2, and the degree-one defect sits at \(p\), outside \(V\), where no cell is ever flipped. With phantoms at both endpoints, the phase and the certificate work again, provided the endpoints are at king distance at least 2 (Far) and their phantoms do not point away from each other across a gap of 2 (not opposed).

An endpoint may have no usable phantom. Then the algorithm deletes the endpoint and branches over its neighbour \(w\) on the path. \(V\) has a Hamiltonian \(s\)–\(t\) path exactly when \(V \setminus \{t\}\) has one from \(s\) to some neighbour \(w\) of \(t\), and the deleted \(t\) becomes the phantom of \(w\). Repeating this is a deletion walk. Each end of the branching is a leaf, where the algorithm runs a final test. A potential on the ring of king neighbours shows that a walk makes at most 13 final tests, and there are at most 208 in every case, a constant. When \(s\) and \(t\) are far apart, the walks stop right after the first deletions.

Deletion walks
Left, a deletion walk with two boundary endpoints. The walk deletes \(t_0\) and then \(t_1\), which lie within king distance 1 of \(s\) (purple box), and the deleted \(t_1\) becomes a usable phantom of \(t\). Right, the walk on the side of \(s\) after the inner endpoint \(t\) has been deleted (grey hole cells).

Inner Endpoints, Holes and Vortices

An inner endpoint has no missing neighbour to take a phantom. Deleting it leaves a one-point hole, and the deleted endpoint becomes the phantom of its neighbour on the path, so the degree-one defect sits at the hole's centre. Around this point the arcs that define the height do not balance, which is called a vortex, and no height function exists. Two things are lost, and each is put back separately.

The order of the flips. The height is replaced by a slit height that jumps across one ray from the vortex, plus a quadrant label. The combination \(2\tau + \mathrm{lab}\) still rises along every arc, which is the only property the certificate uses.

Quadrant label and slit height around a vortex
Left, the quadrant label around a vortex (open circle). It changes by \(\pm 1\) across the blue lines and by \(\pm 3\) across the slit (red dashed). Right, a factor of a \(4 \times 4\) instance with its slit height (bold) and quadrant label (small, purple) in each cell.

Reachability by flips. Fix one factor \(F\) of the leaf as a reference. Any other factor \(G\) differs from \(F\) by a set of alternating cycles. The signed number of these that go around the hole is the class of \(G\). The cells around the hole are not cells of the graph, so no flip changes the class, and factors in different classes cannot reach each other by flips. The algorithm therefore enumerates the classes, at most \(2|V|+1\) per hole, builds the least factor of each class by a relaxation (classSearch), and runs Sheffield's loop in each class. The class enumeration is the main source of the polynomial degree. Two inner endpoints give two holes and at most \((2|V|+1)^2\) class pairs.

Two classes at one leaf
Two classes at one leaf of the \(4 \times 5\) block. (a) The least factor of class \(h = 0\). (b) The least factor of class \(h = 1\). (c) Their difference (purple) is one alternating cycle around the hole. The loop succeeds in class 0 and is stuck in class 1.

Worked Examples

One complete run, one inner endpoint

\(V\) is the \(4 \times 4\) block without its top-left point, so \(|V| = 15\), with \(s = (0,2)\) and \(t = (2,2)\). \(t\) is inner and \(s\) is not, so the run goes through the one-hole case. The first leaf ends with a certificate that it holds no Hamiltonian path, and the second finds one.

One run of decideHamPath on 15 points
(a) The input. (b) Leaf 1, after deleting \(t\) and \(s\); their neighbours \(w\) and \(x\) get phantoms and are Far, so the walk stops at once. (c) The least factor of the only nonempty class, with 3 pieces and a merging cell. (d) After the flip, 2 pieces, and the phase is stuck, so leaf 1 answers no. (e) Leaf 2, the next neighbour of \(s\), with 2 pieces. (f) After the flip, 1 piece. (g) Adding back \(s\) and \(t\) gives the Hamiltonian \(s\)–\(t\) path.

The bulk case, both endpoints inner and far apart

When \(s\) and \(t\) are far apart, the walks stop at once and the work is in the loop. This run on 34 points needs a bridge.

One run with both endpoints inner
(a) The input. (b) The leaf after deleting \(t\) and \(s\). (c) The least factor of the class pair \((0,0)\), with 4 pieces. (d, e) Two phases bring it to 2 pieces, and no merging cell is left. (f) The bridge step flips a cell of the dashed row and splits the path, and a merging cell appears. (g) The reduction flips it and lowers the bridge, leaving 1 piece. (h) The Hamiltonian \(s\)–\(t\) path.

Verification in Lean 4

The formalization is about 47,000 lines of Lean 4 and Mathlib. The algorithm decideHamPath and every definition that it and the main statement use are in one file of about 950 lines, lean/SolidGridHam/Algorithm.lean. decideHamPath is computable. No file contains sorry, the build has no warnings, and the main results use only propext, Classical.choice and Quot.sound.

TheoremStatement
decideHamPath_mainCorrectness and the step bound, for every solid \(V\) and distinct \(s, t \in V\).
stuck_minimalThe count behind the certificate for a stuck phase, with chained rows.
ulhc_mainHamiltonian cycles (Umans–Lenhart), correct in at most \(5 \cdot 10^8\,(|V|+1)^{12}\) steps of a step-counting monad.

Lean checks everything except the following, which a reader checks by eye.

  • The definitions in the statement, Pt, Edge, IsEdge, deg, IsFactor, dST, ncomp and Solid. Solid is cross-checked by computation against "every bounded face is a unit square", not proved equivalent in Lean.
  • The cost model. decideHamPathCost and the cost functions it calls are written beside the algorithm and follow its structure, but are not linked to it formally.
  • Fixed endpoints. The theorem is about paths between given \(s\) and \(t\). Paths with free endpoints follow by trying all pairs.

The correctness statement is registered with the Palomar registry as PALOMAR-2026-10-19-000001. A full build takes about half an hour on four cores. 

cd lean
lake exe cache get
lake build
cd .. && scripts/check.sh

Implementations

The repository has reference implementations in Python, C and JavaScript, each with a command-line front end, and all of them return the path on a "yes" answer. The Python reference mode ports each definition on the call path of decideHamPath as one function with the same name, control flow and iteration order. Its fast mode adds answer-preserving speedups, and the C and JavaScript implementations port the fast mode. The implementations are not verified. 

python3 lib/python/gen.py -n 60 --shape stamp | python3 lib/python/hpst_cli.py --draw

The input is an ASCII grid with . for points, # or a space for missing points, and s, t for the endpoints.

  • lib/README.md, the input format, the command lines and the tests.
  • lean/README.md, the Lean package.
  • The demo, which generates a random solid shape, lets you place \(s\) and \(t\), and solves it in the browser.

Sources

  • A. Itai, C. H. Papadimitriou and J. L. Szwarcfiter, Hamilton paths in grid graphs, SIAM J. Comput. 11 (1982), 676–686.
  • C. Umans and W. Lenhart, Hamiltonian cycles in solid grid graphs, Proc. 38th FOCS (1997), 496–505.
  • S. Sheffield, Computing and sampling restricted vertex degree subgraphs and Hamiltonian cycles, arXiv:math/0008231 (2000).

AI Disclosure

Nearly the entirety of the work for this project was done by Claude (Opus 5.5), including the algorithm, writing the paper, the reference implementations, the demo, the Lean 4 proof and the explainer video. The author contributed little more than the problem statement and guidance.