@InProceedings{zhou:LIPIcs.CP.2024.40, author = {Zhou, Neng-Fa}, title = {{Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination}}, booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)}, pages = {40:1--40:8}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-336-2}, ISSN = {1868-8969}, year = {2024}, volume = {307}, editor = {Shaw, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.40}, URN = {urn:nbn:de:0030-drops-207258}, doi = {10.4230/LIPIcs.CP.2024.40}, annote = {Keywords: Graph constraints, the Hamiltonian cycle problem, SAT encoding, Vertex elimination, Graph synthesis} }