{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:28:40Z","timestamp":1766136520245,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319115573"},{"type":"electronic","value":"9783319115580"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11558-0_52","type":"book-chapter","created":{"date-parts":[[2014,9,16]],"date-time":"2014-09-16T02:22:39Z","timestamp":1410834159000},"page":"684-693","source":"Crossref","is-referenced-by-count":11,"title":["Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem"],"prefix":"10.1007","author":[{"given":"Takehide","family":"Soh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Le Berre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phanie","family":"Roussel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mutsunori","family":"Banbara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoyuki","family":"Tamura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"52_CR1","unstructured":"DIMACS Graph Coloring, \n                      http:\/\/mat.gsia.cmu.edu\/COLOR\/instances.html"},{"key":"52_CR2","unstructured":"DIMACS TSP Challnege, \n                      http:\/\/dimacs.rutgers.edu\/Challenges\/TSP\/"},{"key":"52_CR3","unstructured":"LKH, \n                      http:\/\/www.akira.ruc.dk\/~keld\/research\/LKH\/"},{"key":"52_CR4","unstructured":"TSPLIB, \n                      http:\/\/comopt.ifi.uni-heidelberg.de\/software\/TSPLIB95\/\n                    ."},{"key":"52_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-40627-0_10","volume-title":"Principles and Practice of Constraint Programming","author":"I. Ab\u00edo","year":"2013","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-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.\u00a08124, pp. 97\u2013106. Springer, Heidelberg (2013)"},{"issue":"1-4","key":"52_CR6","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/SAT190021","volume":"2","author":"O. Bailleux","year":"2006","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: A translation of pseudo boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation\u00a02(1-4), 191\u2013200 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"4","key":"52_CR7","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1145\/566385.566390","volume":"3","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log.\u00a03(4), 604\u2013627 (2002)","journal-title":"ACM Trans. Comput. Log."},{"issue":"7","key":"52_CR8","doi-asserted-by":"publisher","first-page":"736","DOI":"10.1287\/mnsc.26.7.736","volume":"26","author":"G. Carpeneto","year":"1980","unstructured":"Carpeneto, G., Toth, P.: Some new branching and bounding criteria for the asymmetric travelling salesman problem. Management Science\u00a026(7), 736\u2013743 (1980)","journal-title":"Management Science"},{"key":"52_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"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.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"52_CR10","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.artint.2013.10.001","volume":"206","author":"W. Dvor\u00e1k","year":"2014","unstructured":"Dvor\u00e1k, W., J\u00e4rvisalo, M., Wallner, J.P., Woltran, S.: Complexity-sensitive decision procedures for abstract argumentation. Artif. Intell.\u00a0206, 53\u201378 (2014)","journal-title":"Artif. Intell."},{"key":"52_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"1","key":"52_CR12","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s10479-009-0565-9","volume":"189","author":"A. Eshragh","year":"2011","unstructured":"Eshragh, A., Filar, J.A., Haythorpe, M.: A hybrid simulation-optimization algorithm for the Hamiltonian cycle problem. Annals OR\u00a0189(1), 103\u2013125 (2011)","journal-title":"Annals OR"},{"key":"52_CR13","unstructured":"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)"},{"key":"52_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"52_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-31612-8_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"V. Ganesh","year":"2012","unstructured":"Ganesh, V., O\u2019Donnell, 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.\u00a07317, pp. 143\u2013156. Springer, Heidelberg (2012)"},{"issue":"1","key":"52_CR16","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s00373-002-0492-x","volume":"19","author":"R.J. Gould","year":"2003","unstructured":"Gould, R.J.: Advances on the Hamiltonian problem - a survey. Graphs and Combinatorics\u00a019(1), 7\u201352 (2003)","journal-title":"Graphs and Combinatorics"},{"issue":"1","key":"52_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00373-013-1377-x","volume":"30","author":"R.J. Gould","year":"2014","unstructured":"Gould, R.J.: Recent advances on the Hamiltonian problem: Survey III. Graphs and Combinatorics\u00a030(1), 1\u201346 (2014)","journal-title":"Graphs and Combinatorics"},{"key":"52_CR18","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1613\/jair.1351","volume":"21","author":"B. Hnich","year":"2004","unstructured":"Hnich, B., Walsh, T., Smith, B.M.: Dual modelling of permutation and injection problems. J. Artif. Intell. Res (JAIR)\u00a021, 357\u2013391 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"52_CR19","unstructured":"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\u2013303 (1999)"},{"key":"52_CR20","unstructured":"Iwama, K., Miyazaki, S.: SAT-variable complexity of hard combinatorial problems. In: Proceedings of the IFIP 13th World Computer Congress, pp. 253\u2013258 (1994)"},{"key":"52_CR21","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1613\/jair.3109","volume":"39","author":"G. J\u00e4ger","year":"2010","unstructured":"J\u00e4ger, G., Zhang, W.: An effective algorithm for and phase transitions of the directed Hamiltonian cycle problem. J. Artif. Intell. Res. (JAIR)\u00a039, 663\u2013687 (2010)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"52_CR22","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-15675-5_18","volume-title":"Logics in Artificial Intelligence","author":"M. Janota","year":"2010","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: Counterexample guided abstraction refinement algorithm for propositional circumscription. In: Janhunen, T., Niemel\u00e4, I. (eds.) JELIA 2010. LNCS (LNAI), vol.\u00a06341, pp. 195\u2013207. Springer, Heidelberg (2010)"},{"key":"52_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M. Janota","year":"2012","unstructured":"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.\u00a07317, pp. 114\u2013128. Springer, Heidelberg (2012)"},{"key":"52_CR24","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations, pp. 85\u2013103 (1972)","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"52_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroning","year":"2004","unstructured":"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.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"issue":"2","key":"52_CR26","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0377-2217(92)90138-Y","volume":"59","author":"G. Laporte","year":"1992","unstructured":"Laporte, G.: The traveling salesman problem: An overview of exact and approximate algorithms. European Journal of Operational Research\u00a059(2), 231\u2013247 (1992)","journal-title":"European Journal of Operational Research"},{"key":"52_CR27","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D. Le Berre","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 59\u201364 (2010)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"2","key":"52_CR28","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0166-218X(02)00410-9","volume":"130","author":"S.D. Prestwich","year":"2003","unstructured":"Prestwich, S.D.: SAT problems with chains of dependent variables. Discrete Applied Mathematics\u00a0130(2), 329\u2013350 (2003)","journal-title":"Discrete Applied Mathematics"},{"key":"52_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-74970-7_35","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"J. Marques-Silva","year":"2007","unstructured":"Marques-Silva, J., Lynce, I.: Towards robust CNF encodings of cardinality constraints. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 483\u2013497. Springer, Heidelberg (2007)"},{"key":"52_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C. Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"key":"52_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-642-39071-5_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"T. Soh","year":"2013","unstructured":"Soh, T., Tamura, N., Banbara, M.: Scarab: A rapid prototyping tool for SAT-based constraint programming systems. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 429\u2013436. Springer, Heidelberg (2013)"},{"key":"52_CR32","series-title":"LNCS (LNAI)","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1007\/978-3-642-10439-8_52","volume-title":"AI 2009: Advances in Artificial Intelligence","author":"M.N. Velev","year":"2009","unstructured":"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.\u00a05866, pp. 517\u2013527. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11558-0_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T03:27:21Z","timestamp":1675826841000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-11558-0_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319115573","9783319115580"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11558-0_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}