{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T22:18:19Z","timestamp":1768515499624,"version":"3.49.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,11,13]],"date-time":"2012-11-13T00:00:00Z","timestamp":1352764800000},"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":[[2013,4]]},"DOI":"10.1007\/s10601-012-9131-1","type":"journal-article","created":{"date-parts":[[2012,11,12]],"date-time":"2012-11-12T01:56:21Z","timestamp":1352685381000},"page":"236-268","source":"Crossref","is-referenced-by-count":9,"title":["Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories"],"prefix":"10.1007","volume":"18","author":[{"given":"Carlos","family":"Ans\u00f3tegui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miquel","family":"Bofill","sequence":"additional","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,11,13]]},"reference":[{"key":"9131_CR1","unstructured":"Ans\u00f3tegui, C., Bofill, M., Palah\u00ed, M., Suy, J., Villaret, M. (2011). A proposal for solving Weighted CSPs with SMT. In Proceedings of the 10th international workshop on constraint modelling and reformulation (ModRef 2011) (pp. 5\u201319)."},{"key":"9131_CR2","unstructured":"Ans\u00f3tegui, C., Bofill, M., Palah\u00ed, M., Suy, J., Villaret, M. (2011). Satisfiability modulo theories: An efficient approach for the resource-constrained project scheduling problem. In Proceedings of the 9th symposium on abstraction, reformulation and approximation (SARA 2011) (pp. 2\u20139)."},{"key":"9131_CR3","unstructured":"Ans\u00f3tegui, C., Bofill, M., Palah\u00ed, M., Suy, J., Villaret, M. (2011). W-MiniZinc: A proposal for modeling weighted CSP with MiniZinc. In Proceedings of the 1st international workshop on MiniZinc (MZN 2011)."},{"key":"9131_CR4","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In Proceedings of the twelfth international conference on theory and applications of satisfiability testing (SAT 2009). LNCS (Vol. 5584, pp. 427\u2013440). Springer.","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"9131_CR5","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"C Barrett","year":"2010","unstructured":"Barrett, C., Stump, A., Tinelli, C. (2010). The SMT-LIB standard: Version 2.0. In A. Gupta, & D. Kroening (Eds.), Proceedings of the 8th international workshop on satisfiability modulo theories. UK: Edinburgh."},{"issue":"2\u20134","key":"9131_CR6","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A. (2008). Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4(2\u20134), 75\u201397.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9131_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 eighth international workshop on constraint Modelling and Reformulation (ModRef 2009) (pp. 30\u201344)."},{"issue":"3","key":"9131_CR8","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/s10601-012-9123-1","volume":"17","author":"M Bofill","year":"2012","unstructured":"Bofill, M., Palah\u00ed, M., Suy, J., Villaret, M. (2012). Solving constraint satisfaction problems with SAT modulo theories. Constraints, 17(3), 273\u2013303.","journal-title":"Constraints"},{"issue":"6","key":"9131_CR9","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1023\/B:JOSH.0000046076.75950.0b","volume":"7","author":"EK Burke","year":"2004","unstructured":"Burke, E.K., Causmaecker, P.D., Berghe, G.V., Landeghem, H.V. (2004). The state of the art of nurse rostering. Journal of Scheduling, 7(6), 441\u2013499.","journal-title":"Journal of Scheduling"},{"key":"9131_CR10","unstructured":"Castro, C., & Manzano, S. (2001). Variable and value ordering when solving balanced academic curriculum problems. In 6th annual workshop of the ERCIM working group on constraints."},{"key":"9131_CR11","unstructured":"Cooper, M.C., DeGivry, S., Schiex, T. (2007). Optimal soft arc consistency. In Proceedings of the 20th international joint conference on artificial intelligence (IJCAI 2007) (pp. 68\u201373)."},{"key":"9131_CR12","unstructured":"deGivry, S., Zytnicki, M., Heras, F., Larrosa, J. (2005). Existential arc consistency: Getting closer to full arc consistency in weighted CSPs. In Proceedings of the 19th international joint conference on artificial intelligence (IJCAI 2005) (pp. 84\u201389)."},{"key":"9131_CR13","doi-asserted-by":"crossref","unstructured":"Dutertre, B., & deMoura, L. (2006). A fast linear-arithmetic solver for DPLL(T). In Proceedings of the 18th international conference on computer aided verification, CAV\u201906. LNCS (Vol. 4144, pp. 81\u201394). Springer.","DOI":"10.1007\/11817963_11"},{"key":"9131_CR14","unstructured":"Dutertre, B., & deMoura, L. (2006). The Yices SMT solver. Tool paper available at http:\/\/yices.csl.sri.com\/tool-paper.pdf ."},{"key":"9131_CR15","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2003). An extensible sat-solver. In E. Giunchiglia, & A. Tacchella (Eds.), SAT. Lecture notes in computer science (Vol. 2919, pp. 502\u2013518). Springer."},{"issue":"1\u20133","key":"9131_CR16","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/0004-3702(92)90004-H","volume":"58","author":"EC Freuder","year":"1992","unstructured":"Freuder, E.C., & Wallace, R.J. (1992). Partial constraint satisfaction. Artificial Intelligence, 58(1\u20133), 21\u201370.","journal-title":"Artificial Intelligence"},{"issue":"3","key":"9131_CR17","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/s10601-008-9047-y","volume":"13","author":"AM Frisch","year":"2008","unstructured":"Frisch, A.M., 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":"9131_CR18","unstructured":"Gent, I., Miguel, I., Rendl, A. (2010). Optimising quantified expressions in constraint models. In Proceedings of the 9th international workshop on constraint modelling and reformulation (ModRef 2010)."},{"key":"9131_CR19","unstructured":"Hnich, B., Kiziltan, Z., Walsh, T. (2002). Modelling a balanced academic curriculum problem. In Proceedings of the fourth international workshop on integration of AI and OR techniques in constraint programming for combinatorial optimisation problems (CPAIOR 2002) (pp. 121\u2013131)."},{"key":"9131_CR20","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1023\/A:1020510611031","volume":"7","author":"J Larrosa","year":"2002","unstructured":"Larrosa, J., & Meseguer, P. (2002). Partition-based lower bound for max-CSP. Constraints, 7, 407\u2013419.","journal-title":"Constraints"},{"issue":"1","key":"9131_CR21","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0004-3702(98)00108-8","volume":"107","author":"J Larrosa","year":"1999","unstructured":"Larrosa, J., Meseguer, P., Schiex, T. (1999). Maintaining reversible DAC for max-CSP. Artificial Intelligence, 107(1), 149\u2013163.","journal-title":"Artificial Intelligence"},{"issue":"1\u20132","key":"9131_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2004.05.004","volume":"159","author":"J Larrosa","year":"2004","unstructured":"Larrosa, J., & Schiex, T. (2004). Solving weighted CSP by maintaining arc-consistency. Artificial Intelligence, 159(1\u20132), 1\u201326.","journal-title":"Artificial Intelligence"},{"key":"9131_CR23","unstructured":"Mahajan, Y.S., Fu, Z., Malik, S. (2004). Zchaff2004: An efficient SAT solver. In H.H. Hoos, & D.G. Mitchell (Eds.), Proceedings of the 7th international conference on theory and applications of satisfiability testing (SAT 2004). LNCS (Vol. 3542, pp. 360\u2013375). Springer."},{"key":"9131_CR24","doi-asserted-by":"crossref","unstructured":"Manquinho, V.M., Silva, J.P.M., Planes, J. (2009). Algorithms for weighted Boolean optimization. In Proceedings of the twelfth international conference on theory and applications of satisfiability testing (SAT 2009). LNCS (Vol. 5584, pp. 495\u2013508). Springer.","DOI":"10.1007\/978-3-642-02777-2_45"},{"key":"9131_CR25","doi-asserted-by":"crossref","unstructured":"Meseguer, P., Rossi, F., Schiex, T. (2006). Soft constraints. In F. Rossi, P. van Beek, T. Walsh (Eds.), Handbook of constraint programming (chapter 9). Elsevier.","DOI":"10.1016\/S1574-6526(06)80013-1"},{"key":"9131_CR26","doi-asserted-by":"crossref","unstructured":"M\u00e9tivier, J.-P., Boizumault, P., Loudni, S. (2009). Solving nurse rostering problems using soft global constraints. In Proceedings of the 15th international conference on principles and practice of constraint programming (CP 2009). LNCS (Vol. 5732, pp. 73\u201387). Springer.","DOI":"10.1007\/978-3-642-04244-7_9"},{"key":"9131_CR27","doi-asserted-by":"crossref","first-page":"2357","DOI":"10.1016\/j.cor.2008.08.014","volume":"36","author":"L Michel","year":"2009","unstructured":"Michel, L., See, A., VanHentenryck, P. (2009). Parallel and distributed local search in COMET. Computers and Operations Research, 36, 2357\u20132375.","journal-title":"Computers and Operations Research"},{"key":"9131_CR28","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 Proceedings of the 13th international conference on principles and practice of constraint programming (CP 2007). LNCS (Vol. 4741, pp. 529\u2013543). Springer.","DOI":"10.1007\/978-3-540-74970-7_38"},{"key":"9131_CR29","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., & Oliveras, A. (2006). On SAT modulo theories and optimization problems. In Proceedings of the 9th international conference on theory and applications of satisfiability testing (SAT 2006). LNCS (Vol. 4121, pp. 156\u2013169). Springer.","DOI":"10.1007\/11814948_18"},{"issue":"6","key":"9131_CR30","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"},{"key":"9131_CR31","unstructured":"Palah\u00ed, M. (2010). Eines basades en la l\u00f2gica per a modelatges i resoluci\u00f3 de problemes combinatoris. Master\u2019s thesis, Universitat de Girona\/Universitat Polit\u00e8cnica de Catalunya, Spain."},{"key":"9131_CR32","doi-asserted-by":"crossref","unstructured":"Petit, T., Regin, J.C., Bessiere, C. (2000). Meta-constraints on violations for over constrained problems. In 12th IEEE international conference on tools with artificial intelligence (ICTAI 2000) (pp. 358\u2013365).","DOI":"10.1109\/TAI.2000.889894"},{"key":"9131_CR33","unstructured":"Roussel, O., & Lecoutre, C. (2009). XML representation of constraint networks: format XCSP 2.1. Computing Research Repository, abs\/0902.2362. http:\/\/arxiv.org\/abs\/0902.2362 ."},{"issue":"3\u20134","key":"9131_CR34","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R. (2007). Lazy satisability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation, 3(3\u20134), 141\u2013224.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9131_CR35","unstructured":"Vanhoucke, M., & Maenhout, B. (2007). NSPLib\u2014a nurse scheduling problem library: A tool to evaluate (meta-) heuristic procedures. In Operational research for health policy making better decisions (pp. 151\u2013165)."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-012-9131-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-012-9131-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-9131-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,16]],"date-time":"2020-07-16T00:10:33Z","timestamp":1594858233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-012-9131-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,13]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["9131"],"URL":"https:\/\/doi.org\/10.1007\/s10601-012-9131-1","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"value":"1383-7133","type":"print"},{"value":"1572-9354","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,13]]}}}