2026-07-28T00:29:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20725 2024-08-29T08:52:53Z ddc:004 open_access

Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination (Short Paper) Zhou, Neng-Fa Graph constraints the Hamiltonian cycle problem SAT encoding Vertex elimination Graph synthesis This paper presents a SAT encoding, called vertex elimination encoding (VEE), for the Hamiltonian Cycle Problem (HCP). The encoding maps a Hamiltonian cycle in the reduced graph after vertex elimination to a Hamiltonian cycle in the original graph. While VEE is not competitive for large dense graphs due to its large encoding sizes, it can be utilized to reduce graphs when they are sparse. This paper compares VEE with the distance encoding, and shows that the hybridization of these two encodings is effective for the benchmarks. For the knight’s tour problem, in particular, the hybrid encoding solves some middle-sized instances that were beyond the reach for previous eager SAT encodings. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Neng-Fa Zhou 2024 Is Part Of LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2024.40 urn:nbn:de:0030-drops-207258 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.40 eng https://creativecommons.org/licenses/by/4.0/legalcode