Structure aware solver improves finding hamiltonian cycles in graphs
StructHCP: Structure-Aware SAT--CEGAR for the Hamiltonian Cycle Problem
Logic in Computer Science
Summary
Finding a Hamiltonian cycle means finding a path through a network that visits each point exactly once and returns to the start. Many existing solvers treat all graphs the same, but the authors developed StructHCP, a method that looks at the graph’s overall shape to choose better ways to search. This approach combines special handling for parts of the graph that are tricky with general methods for others, leading to solutions on more test problems and faster overall solving. Their system even found some solutions missing from previous known results, showing that picking the right way to represent the graph can help solve these problems more effectively.
What this means in practice
- •For graph algorithm engineers: Use structure-aware encoding choices to efficiently solve Hamiltonian cycle instances that traditional methods struggle with.
- •For network optimization teams: Integrate StructHCP’s approach to improve cycle detection in network designs with complex connectivity patterns.
Authors
Quan Van Vi, Tuyen Van Kieu, Khanh Van To
Abstract
Many exact Hamiltonian-cycle solvers use the same edge-level representation for every input, even when graph structure admits a smaller set of global decisions. We present StructHCP, a SAT--CEGAR pipeline that selects a representation through inexpensive structural recognizers. Specialized searches handle high-degree clusters and paired chains, while complete directed and undirected encodings handle cubic and general graphs. Every returned cycle is reconstructed when necessary and verified in the input graph. On the 1,001-instance FHCP Challenge Set, StructHCP solves 826 instances, compared with 741 when the same general SAT--CEGAR engine is applied directly to every unreduced input graph. Relative to this ablation, StructHCP reduces PAR-2 by 32.9 percent. Formulation selection solves 82 more instances than the contracted general encoding; high-degree-cluster and cubic graphs account for 81 of this difference. StructHCP also solves 34 of the 51 instances solved by neither HCup nor Cut-set CEGAR, raising the combined coverage of the three solvers from 950 to 984. Twelve of its solutions lie outside the union of published per-instance SAT results analyzed here, and six also lie outside the published exact result sets in our comparison. These results show that selecting the representation can complement connectivity refinement on structured HCP instances.