Abstract
The Hamiltonian cycle problem (HCP) is the problem of finding a spanning cycle in a given graph. HCP is NP-complete and has been known as an important problem due to its close relationship to the travelling salesman problem (TSP), which can be seen as an optimization variant of finding a minimum cost cycle. In a different viewpoint, HCP is a special case of TSP. In this paper, we propose an incremental SAT-based method for solving HCP. The number of clauses needed for a CNF encoding of HCP often prevents SAT-based methods from being scalable. Our method reduces that number of clauses by relaxing some constraints and by handling specifically cardinality constraints. Our approach has been implemented on top of the SAT solver Sat4j using Scarab. An experimental evaluation is carried out on several benchmark sets and compares our incremental SAT-based method against an existing eager SAT-based method and specialized methods for HCP.
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
Preview
Unable to display preview. Download preview PDF.
References
DIMACS Graph Coloring, http://mat.gsia.cmu.edu/COLOR/instances.html
DIMACS TSP Challnege, http://dimacs.rutgers.edu/Challenges/TSP/
TSPLIB, http://comopt.ifi.uni-heidelberg.de/software/TSPLIB95/ .
Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Stuckey, P.J.: To encode or to propagate? The best choice for each constraint in SAT. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 97–106. Springer, Heidelberg (2013)
Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1-4), 191–200 (2006)
Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4), 604–627 (2002)
Carpeneto, G., Toth, P.: Some new branching and bounding criteria for the asymmetric travelling salesman problem. Management Science 26(7), 736–743 (1980)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Dvorák, W., Järvisalo, M., Wallner, J.P., Woltran, S.: Complexity-sensitive decision procedures for abstract argumentation. Artif. Intell. 206, 53–78 (2014)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Eshragh, A., Filar, J.A., Haythorpe, M.: A hybrid simulation-optimization algorithm for the Hamiltonian cycle problem. Annals OR 189(1), 103–125 (2011)
Frisch, A.M., Giannaros, P.A.: SAT encodings of the at-most-k constraint: Some old, some new, some fast, some slow. In: Proceedings of the 9th International Workshop on Constraint Modelling and Reformulation, ModRef 2010 (2010)
Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)
Ganesh, V., O’Donnell, C.W., Soos, M., Devadas, S., Rinard, M.C., Solar-Lezama, A.: Lynx: A programmatic SAT solver for the rna-folding problem. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 143–156. Springer, Heidelberg (2012)
Gould, R.J.: Advances on the Hamiltonian problem - a survey. Graphs and Combinatorics 19(1), 7–52 (2003)
Gould, R.J.: Recent advances on the Hamiltonian problem: Survey III. Graphs and Combinatorics 30(1), 1–46 (2014)
Hnich, B., Walsh, T., Smith, B.M.: Dual modelling of permutation and injection problems. J. Artif. Intell. Res (JAIR) 21, 357–391 (2004)
Hoos, H.H.: SAT-encodings, search space structure, and local search performance. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI 1999), pp. 296–303 (1999)
Iwama, K., Miyazaki, S.: SAT-variable complexity of hard combinatorial problems. In: Proceedings of the IFIP 13th World Computer Congress, pp. 253–258 (1994)
Jäger, G., Zhang, W.: An effective algorithm for and phase transitions of the directed Hamiltonian cycle problem. J. Artif. Intell. Res. (JAIR) 39, 663–687 (2010)
Janota, M., Grigore, R., Marques-Silva, J.: Counterexample guided abstraction refinement algorithm for propositional circumscription. In: Janhunen, T., Niemelä, I. (eds.) JELIA 2010. LNCS (LNAI), vol. 6341, pp. 195–207. Springer, Heidelberg (2010)
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving qbf with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012)
Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations, pp. 85–103 (1972)
Kroning, D., Ouaknine, J., Seshia, S.A., Strichman, O.: Abstraction-based satisfiability solving of presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 308–320. Springer, Heidelberg (2004)
Laporte, G.: The traveling salesman problem: An overview of exact and approximate algorithms. European Journal of Operational Research 59(2), 231–247 (1992)
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7, 59–64 (2010)
Prestwich, S.D.: SAT problems with chains of dependent variables. Discrete Applied Mathematics 130(2), 329–350 (2003)
Marques-Silva, J., Lynce, I.: Towards robust CNF encodings of cardinality constraints. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 483–497. Springer, Heidelberg (2007)
Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005)
Soh, T., Tamura, N., Banbara, M.: Scarab: A rapid prototyping tool for SAT-based constraint programming systems. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 429–436. Springer, Heidelberg (2013)
Velev, M.N., Gao, P.: Efficient SAT techniques for relative encoding of permutations with constraints. In: Nicholson, A., Li, X. (eds.) AI 2009. LNCS (LNAI), vol. 5866, pp. 517–527. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Soh, T., Le Berre, D., Roussel, S., Banbara, M., Tamura, N. (2014). Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem. In: Fermé, E., Leite, J. (eds) Logics in Artificial Intelligence. JELIA 2014. Lecture Notes in Computer Science(), vol 8761. Springer, Cham. https://doi.org/10.1007/978-3-319-11558-0_52
Download citation
DOI: https://doi.org/10.1007/978-3-319-11558-0_52
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11557-3
Online ISBN: 978-3-319-11558-0
eBook Packages: Computer ScienceComputer Science (R0)