1999/03/05 by Anatoly D. Plotnikov, Plotnikov, Anatoly D.
Computer Science · #Advanced Graph Theory Research #Complexity and Algorithms in Graphs #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #G.2.1 #G.2.2 #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/9903006
7 pages, 1 figures. It has sent to 6th Twente Workshop on Graphs and Combinatorial Optimization
arxiv created 1999/03/05 · openalex publication_date 1999/03/05 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
For 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).