2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/33166For arbitrary undirected graph $G$, we are designing SATISFIABILITY problem (SAT) for HCP, using tools of Boolean algebra only. The obtained SAT be the logic formulation of conditions for Hamiltonian cycle existence, and use $m$ Boolean variables, where $m$ is the number of graph edges. This Boolean expression is true if and only if an initial graph is Hamiltonian. That is, each satisfying assignment of the Boolean variables determines a Hamiltonian cycle of $G$, and each Hamiltonian cycle of $G$ corresponds to a satisfying assignment of the Boolean variables. In common case, the obtained Boolean expression may has an exponential length (the number of Boolean literals).7 pages, 1 figures. It has sent to 6th Twente Workshop on Graphs and Combinatorial OptimizationLogic in Computer ScienceF.4.1;G.2.1;G.2.2text