{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:04Z","timestamp":1725551944758},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642122507"},{"type":"electronic","value":"9783642122514"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_3","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T19:32:42Z","timestamp":1270841562000},"page":"19-23","source":"Crossref","is-referenced-by-count":2,"title":["Solving Constraint Satisfaction Problems with SAT Technology"],"prefix":"10.1007","author":[{"given":"Naoyuki","family":"Tamura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomoya","family":"Tanjo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mutsunori","family":"Banbara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Frontiers in Artificial Intelligence and Applications (FAIA)","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications (FAIA), vol.\u00a0185. IOS Press, Amsterdam (2009)"},{"key":"3_CR2","unstructured":"de Kleer, J.: A comparison of ATMS and CSP techniques. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI 1989), pp. 290\u2013296 (1989)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-45349-0_32","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"T. Walsh","year":"2000","unstructured":"Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 441\u2013456. Springer, Heidelberg (2000)"},{"key":"3_CR4","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. Artificial Intelligence\u00a045, 275\u2013286 (1990)","journal-title":"Artificial Intelligence"},{"key":"3_CR5","unstructured":"Gent, I.P.: Arc consistency in SAT. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002), pp. 121\u2013125 (2002)"},{"key":"3_CR6","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":"3_CR7","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.dam.2006.07.016","volume":"156","author":"A.V. Gelder","year":"2008","unstructured":"Gelder, A.V.: Another look at graph coloring via propositional satisfiability. Discrete Applied Mathematics\u00a0156, 230\u2013243 (2008)","journal-title":"Discrete Applied Mathematics"},{"key":"3_CR8","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.\u00a04741, pp. 815\u2013822. Springer, Heidelberg (2007)"},{"key":"3_CR9","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\u00a014, 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"3_CR10","unstructured":"Crawford, J.M., Baker, A.B.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), pp. 1092\u20131097 (1994)"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"2291","DOI":"10.1016\/j.dam.2006.04.015","volume":"154","author":"K. Inoue","year":"2006","unstructured":"Inoue, K., Soh, T., Ueda, S., Sasaura, Y., Banbara, M., Tamura, N.: A competitive and cooperative approach to propositional satisfiability. Discrete Applied Mathematics\u00a0154, 2291\u20132306 (2006)","journal-title":"Discrete Applied Mathematics"},{"key":"3_CR12","unstructured":"Nabeshima, H., Soh, T., Inoue, K., Iwanuma, K.: Lemma reusing for SAT based planning and scheduling. In: Proceedings of the International Conference on Automated Planning and Scheduling 2006 (ICAPS 2006), pp. 103\u2013112 (2006)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Soh, T., Inoue, K., Tamura, N., Banbara, M., Nabeshima, H.: A SAT-based method for solving the two-dimensional strip packing problem. Journal of Algorithms in Cognition, Informatics and Logic (2009) (to appear)","DOI":"10.3233\/FI-2010-314"},{"key":"3_CR14","unstructured":"Tamura, N., Banbara, M.: Sugar: a CSP to SAT translator based on order encoding. In: Proceedings of the 2nd International CSP Solver Competition, pp. 65\u201369 (2008)"},{"key":"3_CR15","unstructured":"Tamura, N., Tanjo, T., Banbara, M.: System description of a SAT-based CSP solver Sugar. In: Proceedings of the 3rd International CSP Solver Competition, pp. 71\u201375 (2008)"},{"key":"3_CR16","unstructured":"Tanjo, T., Tamura, N., Banbara, M.: Sugar++: a SAT-based Max-CSP\/COP solver. In: Proceedings of the 3rd International CSP Solver Competition, pp. 77\u201382 (2008)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"3_CR18","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation\u00a04, 75\u201397 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,25]],"date-time":"2024-03-25T13:34:47Z","timestamp":1711373687000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}