{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T13:06:08Z","timestamp":1745413568964,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319232638"},{"type":"electronic","value":"9783319232645"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23264-5_10","type":"book-chapter","created":{"date-parts":[[2015,9,14]],"date-time":"2015-09-14T06:29:48Z","timestamp":1442212188000},"page":"112-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming"],"prefix":"10.1007","author":[{"given":"Mutsunori","family":"Banbara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Gebser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katsumi","family":"Inoue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Max","family":"Ostrowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Peano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Torsten","family":"Schaub","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takehide","family":"Soh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoyuki","family":"Tamura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Weise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,15]]},"reference":[{"key":"10_CR1","unstructured":"Banbara, M., Gebser, M., Inoue, K., Schaub, T., Soh, T., Tamura, N., Weise, M.: Aspartame: solving CSPs with ASP. In: ASPOCP, abs\/1312.6113, CoRR (2013)"},{"volume-title":"Handbook of Constraint Programming","year":"2006","key":"10_CR2","unstructured":"Rossi, F., v Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming. Elsevier, Melbourne (2006)"},{"volume-title":"Handbook of Satisfiability","year":"2009","key":"10_CR3","unstructured":"Biere, A., Heule, M., v Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS, Amsterdam (2009)"},{"key":"10_CR4","unstructured":"Crawford, J., Baker, A.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: AAAI, pp. 1092\u20131097. AAAI Press (1994)"},{"key":"10_CR5","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, 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"10_CR6","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":"10_CR7","volume-title":"Answer Set Solving in Practice","author":"M Gebser","year":"2012","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Morgan and Claypool Publishers, San Rafael (2012)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-23786-7_4","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"N Beldiceanu","year":"2011","unstructured":"Beldiceanu, N., Simonis, H.: A constraint seeker: finding and ranking global constraints from examples. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 12\u201326. Springer, Heidelberg (2011)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Tamura, N., Banbara, M., Soh, T.: Compiling pseudo-boolean constraints to SAT with order encoding. In: ICTAI, pp. 1020\u20131027. IEEE (2013)","DOI":"10.1109\/ICTAI.2013.153"},{"key":"10_CR10","unstructured":"Gent, I., Nightingale, P.: A new encoding of alldifferent into SAT. In: Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2004)"},{"key":"10_CR11","unstructured":"Bessiere, C., Katsirelos, G., Narodytska, N., Quimper, C., Walsh, T.: Decompositions of all different, global cardinality and related constraints. In: IJCAI, pp. 419\u2013424 (2009)"},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"467","DOI":"10.3233\/FI-2010-314","volume":"102","author":"T Soh","year":"2010","unstructured":"Soh, T., Inoue, K., Tamura, N., Banbara, M., Nabeshima, H.: A SAT-based method for solving the two-dimensional strip packing problem. Fund. Informaticae 102, 467\u2013487 (2010)","journal-title":"Fund. Informaticae"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-02846-5_22","volume-title":"Logic Programming","author":"M Gebser","year":"2009","unstructured":"Gebser, M., Ostrowski, M., Schaub, T.: Constraint answer set solving. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 235\u2013249. Springer, Heidelberg (2009)"},{"key":"10_CR14","unstructured":"Balduccini, M.: Representing constraint satisfaction problems in answer set programming. In: ASPOCP, pp. 16\u201330 (2009)"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1017\/S1471068410000220","volume":"10","author":"C Drescher","year":"2010","unstructured":"Drescher, C., Walsh, T.: A translational approach to constraint answer set solving. Theor. Pract. Logic Program. 10, 465\u2013480 (2010)","journal-title":"Theor. Pract. Logic Program."},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1017\/S1471068412000142","volume":"12","author":"M Ostrowski","year":"2012","unstructured":"Ostrowski, M., Schaub, T.: ASP modulo CSP: the clingcon system. Theor. Pract. Logic Program. 12, 485\u2013503 (2012)","journal-title":"Theor. Pract. Logic Program."},{"key":"10_CR17","unstructured":"Prestwich, S.: CNF encodings. In: [3], pp. 75\u201397"},{"key":"10_CR18","unstructured":"de Kleer, J.: A comparison of ATMS and CSP techniques. In: IJCAI, pp. 290\u2013296 (1989)"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Walsh, T.: SAT v CSP. In: CP, pp. 441\u2013456 (2000)","DOI":"10.1007\/3-540-45349-0_32"},{"key":"10_CR20","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0004-3702(90)90009-O","volume":"45","author":"S Kasif","year":"1990","unstructured":"Kasif, S.: On the parallel complexity of discrete relaxation in constraint satisfaction networks. Artif. Intell. 45, 275\u2013286 (1990)","journal-title":"Artif. Intell."},{"key":"10_CR21","unstructured":"Gent, I.: Arc consistency in SAT. In: ECAI, pp. 121\u2013125 (2002)"},{"key":"10_CR22","unstructured":"Iwama, K., Miyazaki, S.: SAT-variable complexity of hard combinatorial problems. In: IFIP, pp. 253\u2013258 (1994)"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.dam.2006.07.016","volume":"156","author":"A Van Gelder","year":"2008","unstructured":"Van Gelder, A.: Another look at graph coloring via propositional satisfiability. Discrete Appl. Math. 156, 230\u2013243 (2008)","journal-title":"Discrete Appl. Math."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-31612-8_37","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"T Tanjo","year":"2012","unstructured":"Tanjo, T., Tamura, N., Banbara, M.: Azucar: A SAT-based CSP solver using compact order encoding. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 456\u2013462. Springer, Heidelberg (2012)"},{"key":"10_CR25","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1613\/jair.3809","volume":"46","author":"A Metodi","year":"2013","unstructured":"Metodi, A., Codish, M., Stuckey, P.: Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems. J. Artif. Intell. Res. 46, 303\u2013341 (2013)","journal-title":"J. Artif. Intell. Res."},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P., Codish, M.: Propagation via lazy clause generation. Constraints 14, 357\u2013391 (2009)","journal-title":"Constraints"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-16242-8_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Banbara","year":"2010","unstructured":"Banbara, M., Matsunaka, H., Tamura, N., Inoue, K.: Generating combinatorial test cases by efficient SAT encodings suitable for CDCL sat solvers. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 112\u2013126. Springer, Heidelberg (2010)"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10601-010-9092-1","volume":"15","author":"C Lecoutre","year":"2010","unstructured":"Lecoutre, C., Roussel, O., van Dongen, M.: Promoting robust black-box solvers through competitions. Constraints 15, 317\u2013326 (2010)","journal-title":"Constraints"},{"key":"10_CR29","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1017\/S1471068412000130","volume":"12","author":"A Metodi","year":"2012","unstructured":"Metodi, A., Codish, M.: Compiling finite domain constraints to SAT with BEE. Theor. Pract. Logic Program. 12, 465\u2013483 (2012)","journal-title":"Theor. Pract. Logic Program."},{"key":"10_CR30","unstructured":"Zhou, N.: The SAT compiler in B-prolog. The ALP Newsletter, March 2013"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Nonmonotonic Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23264-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T13:29:58Z","timestamp":1674566998000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23264-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319232638","9783319232645"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23264-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"15 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}