Ítem
Universitat de Girona. Departament d’Informàtica, Matemàtica Aplicada i Estadística | |
Zhou, Neng-Fa | |
3 setembre 2024 | |
Neng-Fa Zhou, from the City University of New York, 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 7781.mp4 7781.mp3 |
|
audio/mpeg video/mp4 |
|
http://hdl.handle.net/10256.1/7781 | |
eng | |
Universitat de Girona. Departament d’Informàtica, Matemàtica Aplicada i Estadística | |
30th International Conference on Principles and Practice of Constraint Programming | |
Attribution-NonCommercial-ShareAlike 4.0 International | |
http://creativecommons.org/licenses/by-nc-sa/4.0/ | |
Programació per restriccions (Informàtica) -- Congressos
Constraint programming (Computer science) -- Congresses |
|
Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination | |
info:eu-repo/semantics/lecture | |
DUGiMedia |