Vaibhav Tulsyan

cs.DS — Data Structures and Algorithms

Counting Hamiltonian cycles in sparse graphs in subexponential time, assuming the new #SAT algorithms

Contributed by Vaibhav Tulsyan

In October 2026 two manuscripts claimed refutations of the Exponential Time Hypothesis by deterministic algorithms for $\#k$-SAT, each with a Lean formalisation of its top-level statement. Neither result applies directly to connectivity problems such as Hamiltonicity, because no linear-size CNF encoding of "this edge set is a single cycle" is known. This paper derives a corollary of the Anthropic manuscript: assuming three of its internal results (a network-to-clique reduction, an algorithm for cliques of all levels, and the existence of its "pieces"), the number of Hamiltonian cycles of a graph with $n$ vertices and at most $Dn$ edges can be computed exactly and deterministically in time $O(2^{\delta n})$ for every $\delta>0$, and in time $2^{O(\max(m,n)/\sqrt{\log n})}$ for a graph with $m$ edges. A rank-encoded variant of the construction gives $2^{O(n\log\bar d/\sqrt{\log n})}$ for average degree $\bar d$. Deterministic decision, search and Hamiltonian-path counting follow, and so do exact sparse TSP with polynomially bounded weights, exact counting of directed Hamiltonian cycles, and ATSP. The result is not a standalone breakthrough; it stands or falls with the claimed refutation. The ingredients are known: the folklore matrix-tree identity on $2$-factors, the fermionic (Berezin) matrix-tree theorem of Caracciolo, Jacobsen, Saleur, Sokal and Sportiello, and the blob partitions of Cut&Count. What is new is the observation that connectivity can be encoded with $O(1)$ bits per edge through a Grassmann determinant whose only non-local part is a sign, and that this sign costs only $O(g^3)$ bits for $g$ blobs, so the whole construction is a network in the sense of the manuscript, whose value is $n\cdot\#\mathrm{HC}(G)$. Every theorem we claim is formally verified in Lean, end to end, on top of the manuscript's own Lean development: the three counting theorems, the decision, search and path corollaries, sparse TSP, directed Hamiltonian cycles and ATSP, using only the standard axioms, with fresh kernel replays. The Lean sources are at https://github.com/xennygrimmato/eth-hamiltonicity. We also record weaker results that rest only on the machine-checked top-level theorems: the parity of $\#\mathrm{HC}(G)$ for every graph in time $2^{O((m+n)/\sqrt{\log(m+n)})}$ (machine-checked in Lean, with the hypotheses discharged by the labs' own Lean proofs), and one-sided randomized decision. We describe what is proved, what is checked numerically, what is formalised, what is assumed, and what the limitations are.