{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T19:35:54Z","timestamp":1774380954798,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030584740","type":"print"},{"value":"9783030584757","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-58475-7_34","type":"book-chapter","created":{"date-parts":[[2020,9,6]],"date-time":"2020-09-06T20:02:35Z","timestamp":1599422555000},"page":"585-602","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["In Pursuit of an Efficient SAT Encoding for the Hamiltonian Cycle Problem"],"prefix":"10.1007","author":[{"given":"Neng-Fa","family":"Zhou","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,2]]},"reference":[{"key":"34_CR1","doi-asserted-by":"crossref","unstructured":"Bart\u00e1k, R., Zhou, N.F., Stern, R., Boyarski, E., Surynek, P.: Modeling and solving the multi-agent pathfinding problem in Picat. In: 29th IEEE International Conference on Tools with Artificial Intelligence, pp. 959\u2013966 (2017)","DOI":"10.1109\/ICTAI.2017.00147"},{"key":"34_CR2","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Toby, W.: Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Bomanson, J., Gebser, M., Janhunen, T., Kaufmann, B., Schaub, T.: Answer set programming modulo acyclicity. In: Logic Programming and Nonmonotonic Reasoning (LPNMR), pp. 143\u2013150 (2015)","DOI":"10.1007\/978-3-319-23264-5_13"},{"issue":"4","key":"34_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1177352.1177354","volume":"38","author":"L Bordeaux","year":"2006","unstructured":"Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: a comparative survey. ACM Comput. Surv. 38(4), 1\u201354 (2006)","journal-title":"ACM Comput. Surv."},{"key":"34_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-2821-6","volume-title":"Logic Minimization Algorithms for VLSI Synthesis","author":"RK Brayton","year":"1984","unstructured":"Brayton, R.K., Hachtel, G.D., McMullen, C., Sangiovanni-Vincentelli, A.: Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, Amsterdam (1984)"},{"issue":"12","key":"34_CR6","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., Truszczy\u0144ski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92\u2013103 (2011)","journal-title":"Commun. ACM"},{"key":"34_CR7","unstructured":"Chen, J.: A new SAT encoding of the at-most-one constraint. In: Proceedings of the International, Workshop of Constraint Modeling and Reformulation (2010)"},{"issue":"2","key":"34_CR8","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0166-218X(92)00170-Q","volume":"50","author":"A Conrad","year":"1994","unstructured":"Conrad, A., Hindrichs, T., Morsy, H., Wegener, I.: Solution of the knight\u2019s Hamiltonian path problem on chessboards. Disc. Appl. Math. 50(2), 125\u2013134 (1994)","journal-title":"Disc. Appl. Math."},{"key":"34_CR9","unstructured":"Cook, W.J.: In Pursuit of the Traveling Salesman: Mathematics at the Limits of Computation. Princeton University Press, Princeton (2012)"},{"key":"34_CR10","first-page":"393","volume":"2","author":"GB Dantzig","year":"1954","unstructured":"Dantzig, G.B., Fulkerson, R., Johnson, S.: Solution of a large-scale traveling-salesman problem. Oper. Res. 2, 393\u2013410 (1954)","journal-title":"Oper. Res."},{"key":"34_CR11","unstructured":"de Kleer, J.: A comparison of ATMS and CSP techniques. In: IJCAI, pp. 290\u2013296 (1989)"},{"key":"34_CR12","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability. W.H. Freeman and Co., New York City (1979)"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1007\/978-3-540-74970-7_59","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"M Gavanelli","year":"2007","unstructured":"Gavanelli, M.: The log-support encoding of CSP into SAT. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 815\u2013822. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_59"},{"key":"34_CR14","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In: IJCAI, pp. 386-392 (2007)"},{"issue":"1","key":"34_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00373-013-1377-x","volume":"30","author":"RJ Gould","year":"2014","unstructured":"Gould, R.J.: Recent advances on the Hamiltonian problem: survey III. Graphs Comb. 30(1), 1\u201346 (2014)","journal-title":"Graphs Comb."},{"key":"34_CR16","series-title":"Combinatorial Optimization","doi-asserted-by":"publisher","DOI":"10.1007\/b101971","volume-title":"The Traveling Salesman Problem and Its Variations","author":"G Gutin","year":"2007","unstructured":"Gutin, G., Punnen, A.P.: The Traveling Salesman Problem and Its Variations. Combinatorial Optimization. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/b101971"},{"issue":"1","key":"34_CR17","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1112\/jlms\/s1-10.37.26","volume":"10","author":"P Hall","year":"1935","unstructured":"Hall, P.: Representatives of subsets. J. London Math. Soc. 10(1), 26\u201330 (1935)","journal-title":"J. London Math. Soc."},{"issue":"1","key":"34_CR18","doi-asserted-by":"publisher","first-page":"61","DOI":"10.5614\/ejgta.2019.7.1.5","volume":"7","author":"M Haythorpe","year":"2019","unstructured":"Haythorpe, M., Johnson, A.: Change ringing and Hamiltonian cycles: The search for Erin and Stedman triples. EJGTA 7(1), 61\u201375 (2019)","journal-title":"EJGTA"},{"key":"34_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-540-72788-0_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A Hertel","year":"2007","unstructured":"Hertel, A., Hertel, P., Urquhart, A.: Formalizing dangerous SAT encodings. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 159\u2013172. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72788-0_18"},{"key":"34_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-85958-1_10","volume-title":"Principles and Practice of Constraint Programming","author":"J Huang","year":"2008","unstructured":"Huang, J.: Universal booleanization of constraint models. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 144\u2013158. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85958-1_10"},{"key":"34_CR21","first-page":"253","volume":"1","author":"K Iwama","year":"1994","unstructured":"Iwama, K., Miyazaki, S.: SAT-variable complexity of hard combinatorial problems. IFIP Congr. 1, 253\u2013258 (1994)","journal-title":"IFIP Congr."},{"key":"34_CR22","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1613\/jair.3531","volume":"43","author":"P Jeavons","year":"2012","unstructured":"Jeavons, P., Petke, J.: Local consistency and SAT-solvers. JAIR 43, 329\u2013351 (2012)","journal-title":"JAIR"},{"key":"34_CR23","unstructured":"Johnson, A.: Quasi-linear reduction of Hamiltonian cycle problem (HCP) to satisfiability problem (SAT), 2014. Disclosure Number IPCOM000237123D, IP.com, Fairport, NY, June 2014. https:\/\/priorart.ip.com\/IPCOM\/000237123"},{"key":"34_CR24","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359\u2013363 (1992)"},{"key":"34_CR25","unstructured":"Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from n objects. In: The Fourth Workshop on Constraints in Formal Verification (CFV) (2007)"},{"key":"34_CR26","unstructured":"Knuth, D.: The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison-Wesley (2015)"},{"key":"34_CR27","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2004)"},{"key":"34_CR28","unstructured":"Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: IJCAI, pp. 853\u2013858 (2003)"},{"issue":"6","key":"34_CR29","doi-asserted-by":"publisher","first-page":"1417","DOI":"10.1002\/j.1538-7305.1956.tb03835.x","volume":"35","author":"EJ McCluskey","year":"1956","unstructured":"McCluskey, E.J.: Minimization of Boolean functions. Bell Syst. Tech. J. 35(6), 1417\u20131444 (1956)","journal-title":"Bell Syst. Tech. J."},{"issue":"4","key":"34_CR30","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1145\/321043.321046","volume":"7","author":"CE Miller","year":"1960","unstructured":"Miller, C.E., Tucker, A.W., Zemlin, R.A.: Integer programming formulation of traveling salesman problems. J. ACM 7(4), 326\u2013329 (1960)","journal-title":"J. ACM"},{"key":"34_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529\u2013543. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_38"},{"key":"34_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-540-30201-8_36","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G Pesant","year":"2004","unstructured":"Pesant, G.: A regular language membership constraint for finite sequences of variables. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 482\u2013495. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30201-8_36"},{"key":"34_CR33","series-title":"Artificial Intelligence: Foundations, Theory, and Algorithms","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21810-6","volume-title":"Bridging Constraint Satisfaction and Boolean Satisfiability","author":"J Petke","year":"2015","unstructured":"Petke, J.: Bridging Constraint Satisfaction and Boolean Satisfiability. AIFTA. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21810-6"},{"key":"34_CR34","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/363427.363463","volume":"10","author":"I Pohl","year":"1967","unstructured":"Pohl, I.: A method for finding Hamilton paths and knight\u2019s tours. Commun. ACM 10, 446\u2013449 (1967)","journal-title":"Commun. ACM"},{"issue":"2","key":"34_CR35","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0166-218X(02)00410-9","volume":"130","author":"SD Prestwich","year":"2003","unstructured":"Prestwich, S.D.: SAT problems with chains of dependent variables. Disc. Appl. Math. 130(2), 329\u2013350 (2003)","journal-title":"Disc. Appl. Math."},{"issue":"8","key":"34_CR36","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1080\/00029890.1952.11988183","volume":"59","author":"WVO Quine","year":"1952","unstructured":"Quine, W.V.O., Quine, W.V.: The problem of simplifying truth functions. Am. Math. Mon. 59(8), 521\u2013531 (1952)","journal-title":"Am. Math. Mon."},{"key":"34_CR37","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.artint.2012.08.001","volume":"193","author":"J Rintanen","year":"2012","unstructured":"Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45\u201386 (2012)","journal-title":"Artif. Intell."},{"key":"34_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1007\/978-3-319-11558-0_52","volume-title":"Logics in Artificial Intelligence","author":"T Soh","year":"2014","unstructured":"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\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 684\u2013693. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11558-0_52"},{"issue":"4","key":"34_CR39","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/s10601-014-9165-7","volume":"19","author":"M Stojadinovi\u0107","year":"2014","unstructured":"Stojadinovi\u0107, M., Mari\u0107, F.: meSAT: multiple encodings of CSP to SAT. Constraints 19(4), 380\u2013403 (2014). https:\/\/doi.org\/10.1007\/s10601-014-9165-7","journal-title":"Constraints"},{"issue":"2","key":"34_CR40","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/s10601-008-9061-0","volume":"14","author":"N Tamura","year":"2009","unstructured":"Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"34_CR41","unstructured":"Velev, M.N., Gao, P.: Efficient SAT techniques for absolute encoding of permutation problems: application to Hamiltonian cycles. In: Eighth Symposium on Abstraction, Reformulation, and Approximation (SARA) (2009)"},{"key":"34_CR42","unstructured":"Zhou, N.F.: Yet another comparison of SAT encodings for the at-most-k constraint. ArXiv, abs\/2005.06274 (2020)"},{"key":"34_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1007\/978-3-319-66158-2_43","volume-title":"Principles and Practice of Constraint Programming","author":"N-F Zhou","year":"2017","unstructured":"Zhou, N.-F., Kjellerstrand, H.: Optimizing SAT encodings for arithmetic constraints. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 671\u2013686. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66158-2_43"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58475-7_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T05:36:24Z","timestamp":1619242584000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-58475-7_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030584740","9783030584757"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58475-7_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"2 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Principles and Practice of Constraint Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Louvain-la-Neuve","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Belgium","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cp2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cp2020.a4cp.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"122","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"45% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.13","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.47","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}