Document Open Access Logo

SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints

Authors Ryoga Ohashi , Takehide Soh , Daniel Le Berre , Hidetomo Nabeshima , Mutsunori Banbara , Katsumi Inoue , Naoyuki Tamura

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.24.pdf
  • Filesize: 0.83 MB
  • 10 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.24.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Discrete space search
Keywords
  • Hamiltonian Cycle Problem
  • SAT Encoding
  • CEGAR

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.

Cite As Get BibTex

Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura. SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.24

Author Details

Ryoga Ohashi
  • Kobe University, Kobe, Japan
Takehide Soh
  • Kobe University, Kobe, Japan
Daniel Le Berre
  • Univ. Artois, CNRS, UMR 8188 CRIL, Lens, France
Hidetomo Nabeshima
  • Yamanashi University, Kofu, Japan
Mutsunori Banbara
  • Nagoya University, Nagoya, Japan
Katsumi Inoue
  • National Institute of Informatics, Tokyo, Japan
Naoyuki Tamura
  • Kobe University, Kobe, Japan

Funding

This work was financially supported by JSPS KAKENHI (23K11047), and by ROIS NII Open Collaborative Research 2024 (24FP04).
  • Soh, Takehide: JSPS KAKENHI Grant Number 23K11047.
  • Banbara, Mutsunori: JSPS KAKENHI Grant Number 25K03097.
  • Inoue, Katsumi: JSPS KAKENHI Grant Number JP25K03190, JST CREST Grant Number JPMJCR22D3.

Supplementary Materials

References

  1. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  2. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  3. Georges A Croes. A method for solving traveling-salesman problems. Operations Research, 6(6):791-812, 1958. Google Scholar
  4. George B. Dantzig, Delbert R. Fulkerson, and Selmer M. Johnson. Solution of a large-scale traveling-salesman problem. Journal of the Operations Research Society of America, 2(4):393-410, 1954. URL: https://doi.org/10.1287/OPRE.2.4.393.
  5. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. Satisfiability modulo user propagators. J. Artif. Intell. Res., 81:989-1017, 2024. URL: https://doi.org/10.1613/JAIR.1.16163.
  6. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT competition 2020. Artif. Intell., 301:103572, 2021. URL: https://doi.org/10.1016/J.ARTINT.2021.103572.
  7. Michael Haythorpe. FHCP Challenge Set: The first set of structurally difficult instances of the Hamiltonian cycle problem, 2019. URL: https://arxiv.org/abs/1902.10352.
  8. Marijn J. H. Heule. Chinese remainder encoding for Hamiltonian cycles. In Chu-Min Li and Felip Manyà, editors, Proc of 24th International Conference on Theory and Applications of Satisfiability Testing (SAT 2021), volume 12831 of LNCS, pages 216-224. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_15.
  9. Christoph Jabs. RustSAT: A library for SAT solving in Rust. In Proc of 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025), volume 341 of LIPIcs, pages 15:1-15:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.15.
  10. Richard M. Karp. Reducibility among Combinatorial Problem, pages 85-103. Springer, Boston, MA, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  11. Steven D. 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.
  12. Carsten Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In Peter van Beek, editor, Proc. of 10th International Conference on Principles and Practice of Constraint Programming (CP 2005), pages 827-831, Berlin, Heidelberg, 2005. Springer. URL: https://doi.org/10.1007/11564751_73.
  13. 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 Eduardo Fermé and João Leite, editors, Proc. of 14th European Conference on Logics in Artificial Intelligence, pages 684-693. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11558-0_52.
  14. Miroslav N. Velev and Ping Gao. Efficient SAT techniques for absolute encoding of permutation problems: Application to Hamiltonian cycles. In Vadim Bulitko and J. Christopher Beck, editors, Proc. of 8th Symposium on Abstraction, Reformulation, and Approximation (SARA 2009). AAAI, 2009. URL: http://www.aaai.org/ocs/index.php/SARA/SARA09/paper/view/837.
  15. Neng-Fa Zhou. In pursuit of an efficient SAT encoding for the Hamiltonian cycle problem. In Helmut Simonis, editor, Proc. of 26th International Conference on Principles and Practice of Constraint Programming (CP 2020), volume 12333 of Lecture Notes in Computer Science, pages 585-602. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_34.
  16. Neng-Fa Zhou. Encoding the Hamiltonian cycle problem into SAT based on vertex elimination (short paper). In Paul Shaw, editor, Proc. of 30th International Conference on Principles and Practice of Constraint Programming (CP 2024), volume 307 of LIPIcs, pages 40:1-40:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.CP.2024.40.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact