Abstract
The Hamiltonian Cycle Problem (HCP) consists of two constraints: i) each vertex contributes exactly two edges to the cycle; and ii) there is exactly one cycle. The former can be encoded naturally and compactly, while the encodings of the latter either lack arc consistency or require an exponential number of clauses. We present a new, small encoding for HCP based on the Chinese remainder theorem. We demonstrate the effectiveness of the encoding on challenging HCP instances.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The encoding and decoding tools together with the graphs are available on GitHub at https://github.com/marijnheule/ChineseRemainderEncoding.
References
Bomanson, J., Gebser, M., Janhunen, T., Kaufmann, B., Schaub, T.: Answer set programming modulo acyclicity. In: Calimeri, F., Ianni, G., Truszczynski, M. (eds.) Logic Programming and Nonmonotonic Reasoning. pp. 143–150. Springer International Publishing (2015)
Buratti, M., Del Fra, A.: Cyclic Hamiltonian cycle systems of the complete graph. Discrete Mathematics 279(1), 107–119 (2004), in Honour of Zhu Lie
Chiba, N., Nishizeki, T.: The Hamiltonian cycle problem is linear-time solvable for 4-connected planar graphs. Journal of Algorithms 10(2), 187–211 (1989)
Gent, I.P.: Arc consistency in SAT. In: Proceedings of the 15th European Conference on Artificial Intelligence. p. 121–125. ECAI’02, IOS Press, NLD (2002)
Golomb, S.W.: Shift Register Sequences. Aegean Park Press (1982)
Grebinski, V., Kucherov, G.: Reconstructing a Hamiltonian cycle by querying the graph: Application to DNA physical mapping. Discrete Applied Mathematics 88(1), 147–165 (1998), computational Molecular Biology DAM - CMB Series
Haythorpe, M.: FHCP challenge set: The first set of structurally difficult instances of the Hamiltonian cycle problem (2019), https://arxiv.org/abs/1902.10352v1
Haythorpe, M., Johnson, A.: Change ringing and Hamiltonian cycles: The search for Erin and Stedman triples. EJGTA 7, 61–75 (2019)
Hertel, A., Hertel, P., Urquhart, A.: Formalizing dangerous SAT encodings. In: Marques-Silva, J., Sakallah, K.A. (eds.) Theory and Applications of Satisfiability Testing – SAT 2007. pp. 159–172. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)
Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence. p. 853–858. IJCAI’03, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2003)
Prestwich, S.: SAT problems with chains of dependent variables. Discrete Appl. Math. 130(2), 329–350 (2003)
Soh, T., Le Berre, D., Roussel, S., Banbara, M., Tamura, N.: Incremental SAT-based method with native boolean cardinality handling for the Hamiltonian cycle problem. In: Fermé, E., Leite, J. (eds.) Logics in Artificial Intelligence. pp. 684–693. Springer International Publishing (2014)
Velev, M.N., Gao, P.: Efficient SAT techniques for absolute encoding of permutation problems: Application to hamiltonian cycles. In: Bulitko, V., Beck, J.C. (eds.) Eighth Symposium on Abstraction, Reformulation, and Approximation, SARA 2009, Lake Arrowhead, California, USA, 8–10 August 2009. AAAI (2009)
Zhou, N.F.: In pursuit of an efficient SAT encoding for the Hamiltonian cycle problem. In: Simonis, H. (ed.) Principles and Practice of Constraint Programming, pp. 585–602. Springer International Publishing, Cham (2020)
Acknowledgements
Supported by the NFS under grant CCF-2006363.
We thank Emre Yolcu and Neng-Fa Zhou for comments on an earlier draft.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Heule, M.J.H. (2021). Chinese Remainder Encoding for Hamiltonian Cycles. In: Li, CM., Manyà, F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science(), vol 12831. Springer, Cham. https://doi.org/10.1007/978-3-030-80223-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-80223-3_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-80222-6
Online ISBN: 978-3-030-80223-3
eBook Packages: Computer ScienceComputer Science (R0)