{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T10:23:57Z","timestamp":1772792637733,"version":"3.50.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319653396","type":"print"},{"value":"9783319653402","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","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":[[2017]]},"DOI":"10.1007\/978-3-319-65340-2_54","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T11:49:29Z","timestamp":1502192969000},"page":"657-669","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Logic-Based Encodings for Ricochet Robots"],"prefix":"10.1007","author":[{"given":"Filipe","family":"Gouveia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro T.","family":"Monteiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"54_CR1","first-page":"1","volume-title":"Theory and Applications of Satisfiability Testing","author":"Carlos Ans\u00f3tegui","year":"2005","unstructured":"Ans\u00f3tegui, C., Many\u00e0, F.: Mapping problems with finite-domain variables into problems with Boolean variables. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 1\u201315 (2004)"},{"key":"54_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39071-5_23"},{"key":"54_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-09284-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Audemard","year":"2014","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197\u2013205. Springer, Cham (2014). doi:10.1007\/978-3-319-09284-3_15"},{"key":"54_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543357","volume-title":"Knowledge Representation, Reasoning and Declarative Problem Solving","author":"C Baral","year":"2003","unstructured":"Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2003)"},{"key":"54_CR5","doi-asserted-by":"crossref","unstructured":"Bart\u00e1k, R., Dovier, A., Zhou, N.F.: Multiple-origin-multiple-destination path finding with minimal arc usage: complexity and models. In: International Conference on Tools with Artificial Intelligence (ICTAI), pp. 91\u201397. IEEE (2016)","DOI":"10.1109\/ICTAI.2016.0024"},{"key":"54_CR6","unstructured":"Butko, N., Lehmann, K.A., Ramenzoni, V.: Ricochet robots-a case study for human complex problem solving. Project thesis from the Complex System Summer School, Santa Fe Institute (2006)"},{"key":"54_CR7","unstructured":"Chen, J.: A new SAT encoding of the at-most-one constraint. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2010)"},{"key":"54_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"key":"54_CR9","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24605-3_37"},{"key":"54_CR10","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.endm.2006.06.062","volume":"25","author":"B Engels","year":"2006","unstructured":"Engels, B., Kamphans, T.: Randolphs robot game is NP-hard!. Electron. Notes Discret. Math. 25, 49\u201353 (2006)","journal-title":"Electron. Notes Discret. Math."},{"issue":"1\u20133","key":"54_CR11","first-page":"143","volume":"35","author":"AM Frisch","year":"2005","unstructured":"Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.: Solving non-Boolean satisfiability problems with stochastic local search: a comparison of encodings. J. Autom. Reason. 35(1\u20133), 143\u2013179 (2005)","journal-title":"J. Autom. Reason."},{"key":"54_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-40564-8_35","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M Gebser","year":"2013","unstructured":"Gebser, M., Jost, H., Kaminski, R., Obermeier, P., Sabuncu, O., Schaub, T., Schneider, M.: Ricochet robots: a transverse ASP benchmark. In: Cabalar, P., Son, T.C. (eds.) LPNMR 2013. LNCS, vol. 8148, pp. 348\u2013360. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40564-8_35"},{"key":"54_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-14726-0_2","volume-title":"Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation","author":"M Gebser","year":"2015","unstructured":"Gebser, M., Kaminski, R., Obermeier, P., Schaub, T.: Ricochet Robots reloaded: a case-study in multi-shot ASP solving. In: Eiter, T., Strass, H., Truszczy\u0144ski, M., Woltran, S. (eds.) Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation. LNCS, vol. 9060, pp. 17\u201332. Springer, Cham (2015). doi:10.1007\/978-3-319-14726-0_2"},{"key":"54_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-72200-7_23","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M Gebser","year":"2007","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: a conflict-driven answer set solver. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS, vol. 4483, pp. 260\u2013265. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-72200-7_23"},{"key":"54_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-72200-7_24","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M Gebser","year":"2007","unstructured":"Gebser, M., Schaub, T., Thiele, S.: GrinGo: a new grounder for answer set programming. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS, vol. 4483, pp. 266\u2013271. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-72200-7_24"},{"key":"54_CR16","unstructured":"Gent, I.P., Nightingale, P.: A new encoding of All different into SAT. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2004)"},{"key":"54_CR17","unstructured":"Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from N objects. In: International Workshop on Constraints in Formal Verification (2007)"},{"key":"54_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531\u2013548. Springer, Cham (2014). doi:10.1007\/978-3-319-10428-7_39"},{"key":"54_CR19","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). doi:10.1007\/978-3-540-74970-7_38"},{"key":"54_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-72788-0_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S Prestwich","year":"2007","unstructured":"Prestwich, S.: Variable dependency in local search: prevention is better than cure. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 107\u2013120. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-72788-0_14"},{"key":"54_CR21","volume-title":"Artificial Intelligence - A Modern Approach","author":"SJ Russell","year":"2010","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence - A Modern Approach, 3rd edn. Pearson Education, London (2010)","edition":"3"},{"key":"54_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-642-34487-9_54","volume-title":"Neural Information Processing","author":"A Sharma","year":"2012","unstructured":"Sharma, A., Sharma, D.: An incremental approach to solving dynamic constraint satisfaction problems. In: Huang, T., Zeng, Z., Li, C., Leung, C.S. (eds.) ICONIP 2012. LNCS, vol. 7665, pp. 445\u2013455. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-34487-9_54"},{"key":"54_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44798-9_4","volume-title":"Correct Hardware Design and Verification Methods","author":"O Shtrichman","year":"2001","unstructured":"Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58\u201370. Springer, Heidelberg (2001). doi:10.1007\/3-540-44798-9_4"},{"key":"54_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-319-13650-9_36","volume-title":"Nature-Inspired Computation and Machine Learning","author":"P Surynek","year":"2014","unstructured":"Surynek, P.: Simple direct propositional encoding of cooperative path finding simplified yet more. In: Gelbukh, A., Espinoza, F.C., Galicia-Haro, S.N. (eds.) MICAI 2014. LNCS, vol. 8857, pp. 410\u2013425. Springer, Cham (2014). doi:10.1007\/978-3-319-13650-9_36"}],"container-title":["Lecture Notes in Computer Science","Progress in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-65340-2_54","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T07:51:53Z","timestamp":1772783513000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-65340-2_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319653396","9783319653402"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-65340-2_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"9 August 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"EPIA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"EPIA Conference on Artificial Intelligence","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 September 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"epia2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/web.fe.up.pt\/~epia2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}