Solving the Hamiltonian Problem in Graph Theory Education with Z3 and the Keçeci Layout

Mehmet Keçeci ORCID: https://orcid.org/0000-0001-9937-9839

Received: 08.21.2025

Abstract: Whilst graph theory constitutes a cornerstone of computer science and mathematics education, the abstract nature of NP-complete problems, such as the Hamiltonian cycle problem, presents a significant conceptual challenge for students. An intuitive grasp of such problems often requires the analytical inspection of complex and non-standard graph structures. Traditional pedagogical methods can prove insufficient in effectively conveying this complexity, potentially diminishing student engagement. In response to these pedagogical challenges, this paper introduces a novel, integrated computational and visual tool designed for the exploration and analysis of the Hamiltonian cycle problem. The developed framework synergises two core technologies: Z3, a high-performance Satisfiability Modulo Theories (SMT) solver from Microsoft Research, and the Keçeci Layout, a novel graph layout algorithm developed by the authors, which is optimised for sequential structures. The foundation of our approach lies in reformulating the Hamiltonian cycle problem not as a search for an algorithmic solution, but as a constraint satisfaction problem. This declarative model, which defines the mathematical rules a valid cycle must obey, is submitted to the Z3 solver to automatically prove whether a given graph contains a Hamiltonian cycle. Compared to conventional trial-and-error or brute-force algorithms, this method offers a more efficient and formally verified approach, mathematically guaranteeing the correctness of the result. When Z3 finds a solution (SAT), it produces a model representing that solution; if no solution exists (UNSAT), it definitively reports the absence of a cycle. The principal educational innovation of this work, however, emerges during the visualisation of these abstract logical results. Standard graph layout algorithms, such as the Fruchterman-Reingold method, whilst often aesthetically optimised, can produce intricate and unpredictable outputs that make tracing a sequential path or cycle difficult. In contrast, our proposed Keçeci Layout algorithm positions nodes in a sequential, zigzag pattern along a primary axis, thereby revealing the graph's intrinsic path structure with clarity. When the Hamiltonian cycle found by Z3 is highlighted upon this layout, students can intuitively follow, step-by-step, how the cycle traverses the entire graph, visits each node exactly once, and returns to its origin. This visual lucidity has been tested and demonstrated on classical examples, including the Dodecahedral graph (Hamiltonian) and the Herschel graph (non-Hamiltonian). In conclusion, this integrated tool stands out as a powerful pedagogical resource, bridging the gap between abstract logic and tangible visual evidence in the teaching of challenging topics like NP-complete problems, and thus possessing the potential to significantly enhance student comprehension and engagement.

Keywords: Hamiltonian Cycle, Z3 Theorem Prover, Z3, SMT Solver, Constraint Satisfaction Problem, CSP, Graph Theory, Graph Visualization, Graph Layout Algorithms, Keçeci Layout, Declarative Programming, Symbolic Computation, NP-Complete Problems, Computational Logic, Automated Reasoning, Data Visualization.