Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination (Short Paper)

Zhou, Neng-Fa

doi:10.4230/LIPIcs.CP.2024.40

File

LIPIcs.CP.2024.40.pdf

Filesize: 0.61 MB
8 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CP.2024.40
URN: urn:nbn:de:0030-drops-207258

Author Details

Neng-Fa Zhou

CUNY Brooklyn College and the Graduate Center, NY, USA

Acknowledgements

The author would like to thank Ruiwei Wang, Roland Yap Hock Chuan, and the anonymous reviewers for helpful comments.

Cite AsGet BibTex

Neng-Fa Zhou. Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination (Short Paper). In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 40:1-40:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.40

Abstract

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.

Subject Classification

ACM Subject Classification

Computing methodologies → Knowledge representation and reasoning
Computing methodologies → Planning and scheduling
Hardware → Theorem proving and SAT solving

Keywords

Graph constraints
the Hamiltonian cycle problem
SAT encoding
Vertex elimination
Graph synthesis

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

Nicolas Beldiceanu, Mats Carlsson, and Jean-Xavier Rampon. Global constraint catalog, 2021. URL: http://sofdem.github.io/gccat/gccat/.
Alexander Hertel, Philipp Hertel, and Alasdair Urquhart. Formalizing dangerous SAT encodings. In SAT, volume 4501, pages 159-172, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_18.
Marijn J. H. Heule. Chinese remainder encoding for hamiltonian cycles. In SAT, pages 216-224, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_15.
C. E. Miller, A. W. Tucker, and R. A. Zemlin. Integer programming formulation of traveling salesman problems. J. ACM, 7(4):326-329, 1960.
Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. MiniZinc: Towards a standard CP modelling language. In CP, pages 529-543, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_38.
Steven David Prestwich. SAT problems with chains of dependent variables. Discret. Appl. Math., 130(2):329-350, 2003. URL: https://doi.org/10.1016/S0166-218X(02)00410-9.
Masood Feyzbakhsh Rankooh and Jussi Rintanen. Propositional encodings of acyclicity and reachability by using vertex elimination. In Thirty-Sixth AAAI Conference, pages 5861-5868. AAAI Press, 2022. URL: https://ojs.aaai.org/index.php/AAAI/article/view/20530, URL: https://doi.org/10.1609/AAAI.V36I5.20530.
Donald J. Rose, Robert Endre Tarjan, and George S. Lueker. Algorithmic aspects of vertex elimination on graphs. SIAM J. Comput., 5(2):266-283, 1976. URL: https://doi.org/10.1137/0205021.
Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, and Naoyuki Tamura. Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem. In Logics in Artificial Intelligence (JELIA), pages 684-693, 2014.
Miroslav N. Velev and Ping Gao. Efficient SAT techniques for absolute encoding of permutation problems: Application to Hamiltonian cycles. In SARA. AAAI, 2009. URL: http://www.aaai.org/ocs/index.php/SARA/SARA09/paper/view/837.
Neng-Fa Zhou. In pursuit of an efficient SAT encoding for the Hamiltonian cycle problem. In CP, pages 585-602, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_34.
Neng-Fa Zhou and Håkan Kjellerstrand. Optimizing SAT encodings for arithmetic constraints. In CP, pages 671-686, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_43.
Neng-Fa Zhou, Ruiwei Wang, and Roland H. C. Yap. A comparison of SAT encodings for acyclicity of directed graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing, SAT, pages 30:1-30:9, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.30.