{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:42:19Z","timestamp":1767339739847},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141850"},{"type":"electronic","value":"9783642141867"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","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-14186-7_25","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:20:37Z","timestamp":1278627637000},"page":"300-305","source":"Crossref","is-referenced-by-count":11,"title":["A System for Solving Constraint Satisfaction Problems with SMT"],"prefix":"10.1007","author":[{"given":"Miquel","family":"Bofill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josep","family":"Suy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mateu","family":"Villaret","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Bofill, M., Palahi, M., Suy, J., Villaret, M.: SIMPLY: a Compiler from a CSP Modeling Language to the SMT-LIB Format. In: Proceedings of the 8th Intl. Workshop on Constraint Modelling and Reformulation, pp. 30\u201344 (2009)"},{"key":"25_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/11875604_61","volume-title":"Foundations of Intelligent Systems","author":"M. Cadoli","year":"2006","unstructured":"Cadoli, M., Mancini, T., Patrizi, F.: SAT as an Effective Solving Technology for Constraint Problems. In: Esposito, F., Ra\u015b, Z.W., Malerba, D., Semeraro, G. (eds.) ISMIS 2006. LNCS (LNAI), vol.\u00a04203, pp. 540\u2013549. Springer, Heidelberg (2006)"},{"key":"25_CR3","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver (August 2006), Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"issue":"3","key":"25_CR4","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/s10601-008-9047-y","volume":"13","author":"A. Frisch","year":"2008","unstructured":"Frisch, A., Harvey, W., Jefferson, C., Mart\u00ednez-Hern\u00e1ndez, B., Miguel, I.: Essence: A Constraint Language for Specifying Combinatorial Problems. Constraints\u00a013(3), 268\u2013306 (2008)","journal-title":"Constraints"},{"key":"25_CR5","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.\u00a05202, pp. 144\u2013158. Springer, Heidelberg (2008)"},{"key":"25_CR6","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., Becket, R., Brand, S., Duck, G., Tack, G.: MiniZinc: Towards a Standard CP Modelling Language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 529\u2013543. Springer, Heidelberg (2007)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 156\u2013169. Springer, Heidelberg (2006)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73449-9_2","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Challenges in Satisfiability Modulo Theories. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 2\u201318. Springer, Heidelberg (2007)"},{"issue":"6","key":"25_CR9","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an Abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland Procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"25_CR10","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Tech. rep., Dept. of Comp. Science, University of Iowa (2006), http:\/\/www.SMT-LIB.org"},{"issue":"3-4","key":"25_CR11","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation\u00a03(3-4), 141\u2013224 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11814948_1","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"H. Sheini","year":"2006","unstructured":"Sheini, H., Sakallah, K.: From Propositional Satisfiability to Satisfiability Modulo Theories. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 1\u20139. Springer, Heidelberg (2006)"},{"key":"25_CR13","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 vs CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 441\u2013456. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14186-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T19:42:18Z","timestamp":1591472538000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14186-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141850","9783642141867"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14186-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}