{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T22:48:16Z","timestamp":1777502896964,"version":"3.51.4"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,5,26]],"date-time":"2012-05-26T00:00:00Z","timestamp":1337990400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1007\/s10601-012-9123-1","type":"journal-article","created":{"date-parts":[[2012,5,25]],"date-time":"2012-05-25T09:00:09Z","timestamp":1337936409000},"page":"273-303","source":"Crossref","is-referenced-by-count":32,"title":["Solving constraint satisfaction problems with SAT modulo theories"],"prefix":"10.1007","volume":"17","author":[{"given":"Miquel","family":"Bofill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miquel","family":"Palah\u00ed","sequence":"additional","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","published-online":{"date-parts":[[2012,5,26]]},"reference":[{"key":"9123_CR1","unstructured":"Ackermann, W. (1954). Solvable cases of the decision problem. Studies in logic and the foundations of mathematics. North-Holland, Amsterdam."},{"key":"9123_CR2","volume-title":"Constraint logic programming using eclipse","author":"KR Apt","year":"2007","unstructured":"Apt, K. R., & Wallace, M. (2007). Constraint logic programming using eclipse. New York: Cambridge University Press."},{"key":"9123_CR3","unstructured":"Bankovi\u0107, M., & Mari\u0107, F. (2010). An Alldifferent constraint solver in SMT. In Proceedings of the 8th international workshop on satisfiability modulo theories."},{"key":"9123_CR4","unstructured":"Barrett, C., Stump, A., & Tinelli, C. (2010). The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/www.SMT-LIB.org . Accessed 16 May 2012."},{"key":"9123_CR5","unstructured":"Barrett, C., Stump, A., & Tinelli, C. (2010). The SMT-LIB standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories."},{"key":"9123_CR6","doi-asserted-by":"crossref","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., & Rubio, A. (2008). The Barcelogic SMT solver. In CAV, LNCS (Vol. 5123, pp. 294\u2013298). Springer.","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"9123_CR7","unstructured":"Bofill, M., Palah\u00ed, M., Suy, J., & Villaret, M. (2009). SIMPLY: A compiler from a CSP modeling language to the SMT-LIB format. In Proceedings of the 8th international workshop on constraint modelling and reformulation (pp. 30\u201344)."},{"key":"9123_CR8","doi-asserted-by":"crossref","unstructured":"Bofill, M., Suy, J., & Villaret, M. (2010). A system for solving constraint satisfaction problems with SMT. In SAT, LNCS (Vol. 6175, pp. 300\u2013305). Springer.","DOI":"10.1007\/978-3-642-14186-7_25"},{"issue":"10","key":"9123_CR9","doi-asserted-by":"crossref","first-page":"1493","DOI":"10.1016\/j.ic.2005.05.011","volume":"204","author":"M Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T. A., Ranise, S., van Rossum, P., et al. (2006). Efficient theory combination via Boolean search. Information and Computation, 204(10), 1493\u20131525.","journal-title":"Information and Computation"},{"key":"9123_CR10","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Santuari, A., & Sebastiani, R. (2006). To Ackermann-ize or not to Ackermann-ize? On efficiently handling uninterpreted function symbols in $\\mathit{SMT}(\\mathcal{EUF \\cup T})$ . In LPAR, LNCS (Vol. 4246, pp. 557\u2013571). Springer.","DOI":"10.1007\/11916277_38"},{"key":"9123_CR11","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., & Sebastiani, R. (2008). The MathSAT 4 SMT solver. In CAV, LNCS (Vol. 5123, pp. 299\u2013303). Springer.","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"9123_CR12","doi-asserted-by":"crossref","unstructured":"Cadoli, M., Mancini, T., & Patrizi, F. (2006). SAT as an effective solving technology for constraint problems. In ISMIS, LNCS (Vol. 4203, pp. 540\u2013549). Springer.","DOI":"10.1007\/11875604_61"},{"key":"9123_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., & Stenico, C. (2010). Satisfiability modulo the theory of costs: Foundations and applications. In TACAS, LNCS (Vol. 6015, pp. 99\u2013113). Springer.","DOI":"10.1007\/978-3-642-12002-2_8"},{"key":"9123_CR14","doi-asserted-by":"crossref","unstructured":"de Moura, L. M. (2011). Orchestrating satisfiability engines. In CP, LNCS (Vol. 6876, p. 1). Springer.","DOI":"10.1007\/978-3-642-23786-7_1"},{"key":"9123_CR15","doi-asserted-by":"crossref","unstructured":"de Moura, L. M., & Bj\u00f8rner, N. (2008). Z3: An efficient SMT solver. In TACAS, LNCS (Vol. 4963, pp. 337\u2013340). Springer.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9123_CR16","unstructured":"Dutertre, B., & de Moura, L. (2006). The Yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf . Accessed 16 May 2012."},{"key":"9123_CR17","doi-asserted-by":"crossref","unstructured":"Dutertre, B., & de Moura, L. M. (2006). A fast linear-arithmetic solver for DPLL(T). In CAV, LNCS (Vol. 4144, pp. 81\u201394). Springer.","DOI":"10.1007\/11817963_11"},{"issue":"3","key":"9123_CR18","doi-asserted-by":"crossref","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. (2008). Essence: A constraint language for specifying combinatorial problems. Constraints, 13(3), 268\u2013306.","journal-title":"Constraints"},{"key":"9123_CR19","doi-asserted-by":"crossref","unstructured":"Huang, J. (2008). Universal Booleanization of constraint models. In CP, LNCS (Vol. 5202, pp. 144\u2013158). Springer.","DOI":"10.1007\/978-3-540-85958-1_10"},{"key":"9123_CR20","unstructured":"JaCoP Java Constraint Programming Solver (2010). http:\/\/jacop.osolpro.com . Accessed 16 May 2012."},{"key":"9123_CR21","unstructured":"Minizinc + Flatzinc (2010). http:\/\/www.g12.csse.unimelb.edu.au\/minizinc\/ . Accessed 16 May 2012."},{"issue":"2","key":"9123_CR22","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., & Oppen, D. C. (1979). Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, TOPLAS, 1(2), 245\u2013257.","journal-title":"ACM Transactions on Programming Languages and Systems, TOPLAS"},{"key":"9123_CR23","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Stuckey, P. J., Becket, R., Brand, S., Duck, G. J., & Tack, G. (2007). MiniZinc: Towards a standard CP modelling language. In CP, LNCS (Vol. 4741, pp. 529\u2013543). Springer.","DOI":"10.1007\/978-3-540-74970-7_38"},{"key":"9123_CR24","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., & Oliveras, A. (2006). On SAT modulo theories and optimization problems. In SAT, LNCS (Vol. 4121, pp. 156\u2013169). Springer.","DOI":"10.1007\/11814948_18"},{"key":"9123_CR25","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., & Rubio, A. (2007). Challenges in satisfiability modulo theories. In RTA, LNCS (Vol. 4533, pp. 2\u201318). Springer.","DOI":"10.1007\/978-3-540-73449-9_2"},{"issue":"6","key":"9123_CR26","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). Journal of the ACM, 53(6), 937\u2013977.","journal-title":"Journal of the ACM"},{"issue":"3","key":"9123_CR27","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P. J., & Codish, M. (2009). Propagation via Lazy clause generation. Constraints, 14(3), 357\u2013391.","journal-title":"Constraints"},{"key":"9123_CR28","unstructured":"Ranise, S., & Tinelli, C. (2006). The SMT-LIB standard: Version 1.2. Technical report, Dept. of Comp. Science, University of Iowa. Available at www.SMT-LIB.org . Accessed 16 May 2012."},{"key":"9123_CR29","unstructured":"Schulte, C., Lagerkvist, M., & Tack, G. (2010). Gecode. http:\/\/www.gecode.org . Accessed 16 May 2012."},{"key":"9123_CR30","unstructured":"SCIP, Solving constraint integer programs (2010). http:\/\/scip.zib.de\/scip.shtml . Accessed 16 May 2012."},{"issue":"3\u20134","key":"9123_CR31","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R. (2007). Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation, 3(3\u20134), 141\u2013224.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9123_CR32","doi-asserted-by":"crossref","unstructured":"Sheini, H. M., & Sakallah, K. A. (2006). From propositional satisfiability to satisfiability modulo theories. In SAT, LNCS (Vol. 4121, pp. 1\u20139). Springer.","DOI":"10.1007\/11814948_1"},{"issue":"1","key":"9123_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R. E. (1984). Deciding combinations of theories. Journal of the ACM, 31(1), 1\u201312.","journal-title":"Journal of the ACM"},{"key":"9123_CR34","unstructured":"SICStus Prolog (2010). http:\/\/www.sics.se\/sicstus . Accessed 16 May 2012."},{"key":"9123_CR35","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/s10601-010-9093-0","volume":"15","author":"PJ Stuckey","year":"2010","unstructured":"Stuckey, P. J., Becket, R., & Fischer, J. (2010). Philosophy of the minizinc challenge. Constraints, 15, 307\u2013316.","journal-title":"Constraints"},{"issue":"2","key":"9123_CR36","doi-asserted-by":"crossref","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. (2009). Compiling finite linear CSP into SAT. Constraints, 14(2), 254\u2013272.","journal-title":"Constraints"},{"key":"9123_CR37","unstructured":"Van Hentenryck, P. (1999). The OPL Optimization Programming Language. MIT Press."},{"key":"9123_CR38","doi-asserted-by":"crossref","unstructured":"Walsh, T. (2000). SAT v CSP. In CP, LNCS (Vol. 1894, pp. 441\u2013456). Springer.","DOI":"10.1007\/3-540-45349-0_32"},{"key":"9123_CR39","unstructured":"Zhang, L., & Malik, S. (2002). The quest for efficient Boolean satisfiability solvers. In CAV, LNCS (Vol. 2404, pp. 17\u201336). Springer."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-012-9123-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-012-9123-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-012-9123-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T02:58:46Z","timestamp":1594177126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-012-9123-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,26]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["9123"],"URL":"https:\/\/doi.org\/10.1007\/s10601-012-9123-1","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5,26]]}}}