{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:10:46Z","timestamp":1748751046622,"version":"3.41.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,11,16]],"date-time":"2015-11-16T00:00:00Z","timestamp":1447632000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10601-015-9232-8","type":"journal-article","created":{"date-parts":[[2015,11,16]],"date-time":"2015-11-16T05:44:43Z","timestamp":1447652683000},"page":"463-494","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Extending SMT solvers with support for finite domain alldifferent constraint"],"prefix":"10.1007","volume":"21","author":[{"given":"Milan","family":"Bankovi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,16]]},"reference":[{"key":"9232_CR1","unstructured":"Bankovic, M., & Maric, F. (2010). An Alldifferent constraint solver in SMT. In 8th International Workshop on Satisfiability Modulo Theories."},{"key":"9232_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., & Tinelli, C. (2009). Satisfiability Modulo Theories. In Handbook of Satisfiability, chap. 26, pp. 825\u2013885. IOS Press.","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"9232_CR3","unstructured":"Barrett, C., Stump, A., & Tinelli, C. (2010). The SMT-LIB Standard: Version 2.0, http:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.0-r12.09.09.pdf ."},{"key":"9232_CR4","unstructured":"Berge, C. (1970). Graphes et hypergraphes."},{"issue":"3","key":"9232_CR5","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"},{"key":"9232_CR6","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Van Rossum, P., Schulz, S., & Sebastiani, R. (2005). An incremental and layered procedure for the satisfiability of linear arithmetic logic. In Tools and Algorithms for the Construction and Analysis of Systems, pp. 317\u2013333. Springer.","DOI":"10.1007\/978-3-540-31980-1_21"},{"issue":"7","key":"9232_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5 (7), 394\u2013397. doi: 10.1145\/368273.368557","journal-title":"Communications of the ACM"},{"key":"9232_CR8","unstructured":"Downing, N., Feydy, T., & Stuckey, P.J. (2012). Explaining alldifferent. In Proceedings of the Thirty-fifth Australasian Computer Science Conference-Volume 122, pp. 115\u2013124. Australian Computer Society, Inc."},{"key":"9232_CR9","doi-asserted-by":"crossref","unstructured":"Downing, N., Feydy, T., & Stuckey, P.J. (2012). Explaining flow-based propagation. In Integration of AI and OR Techniques in Contraint Programming for Combinatorial Optimzation Problems, pp. 146\u2013162. Springer.","DOI":"10.1007\/978-3-642-29828-8_10"},{"key":"9232_CR10","unstructured":"Dutertre, B., & De Moura, L. (2006). The Yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf2 , Vol. 2."},{"issue":"3","key":"9232_CR11","doi-asserted-by":"crossref","first-page":"399","DOI":"10.4153\/CJM-1956-045-5","volume":"8","author":"LR Ford","year":"1956","unstructured":"Ford, L.R., & Fulkerson, D.R. (1956). Maximal flow through a network. Canadian Journal Mathematics, 8(3), 399\u2013404.","journal-title":"Canadian Journal Mathematics"},{"key":"9232_CR12","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2004). DPLL(T): Fast Decision Procedures. In CAV, Lecture Notes in Computer Science, vol. 3114, pp. 175\u2013188. Springer.","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"9232_CR13","unstructured":"Gent, I.P., Jefferson, C., & Miguel, I. (2006). Minion: A fast scalable constraint solver. In ECAI, vol. 141, pp. 98\u2013102."},{"key":"9232_CR14","unstructured":"Gent, I.P., & Lynce, I. (2005). A SAT encoding for the social golfer problem. Modelling and Solving Problems with Constraints, 2."},{"key":"9232_CR15","doi-asserted-by":"crossref","unstructured":"Gent, I.P., Miguel, I., & Moore, N.C. (2010). Lazy explanations for constraint propagators. In Practical Aspects of Declarative Languages, pp. 217\u2013233. Springer.","DOI":"10.1007\/978-3-642-11503-5_19"},{"issue":"18","key":"9232_CR16","doi-asserted-by":"crossref","first-page":"1973","DOI":"10.1016\/j.artint.2008.10.006","volume":"172","author":"IP Gent","year":"2008","unstructured":"Gent, I.P., Miguel, I., & Nightingale, P. (2008). Generalised arc consistency for the alldifferent constraint: An empirical survey. Artificial Intelligence, 172(18), 1973\u20132000.","journal-title":"Artificial Intelligence"},{"key":"9232_CR17","unstructured":"Gomes, C., & Shmoys, D. (2002). Completing quasigroups or latin squares: A structured graph coloring problem. In proceedings of the Computational Symposium on Graph Coloring and Generalizations, pp. 22\u201339."},{"key":"9232_CR18","unstructured":"van Hoeve, W.J. (2001). The alldifferent constraint: A survey. arXiv: preprintcs\/0105015 ."},{"key":"9232_CR19","unstructured":"Janicic, P. (2010). Uniform Reduction to SAT Vol. 8."},{"key":"9232_CR20","unstructured":"Janicic, P. (2010). Maric, F., Uniform reduction to SMT."},{"key":"9232_CR21","volume-title":"Nogood processing in CSPs","author":"G Katsirelos","year":"2008","unstructured":"Katsirelos, G. (2008). Nogood processing in CSPs. Ph.D. thesis: University of Toronto."},{"key":"9232_CR22","doi-asserted-by":"crossref","unstructured":"Krstic, S., & Goel, A. (2007). Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. In FroCoS, Lecture Notes in Computer Science, vol. 4720, pp. 1\u201327. Springer.","DOI":"10.1007\/978-3-540-74621-8_1"},{"issue":"4","key":"9232_CR23","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/s10732-007-9012-8","volume":"13","author":"R Lewis","year":"2007","unstructured":"Lewis, R. (2007). Metaheuristics can solve sudoku puzzles. Journal of Heuristics, 13(4), 387\u2013401.","journal-title":"Journal of Heuristics"},{"key":"9232_CR24","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Lynce, I., & Malik, S. (2009). Conflict-Driven Clause Learning SAT Solvers. In Handbook of Satisfiability, chap. 4, pp. 131\u2013155. IOS Press.","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"9232_CR25","volume-title":"Improving the efficiency of learning CSP solvers","author":"N Moore","year":"2011","unstructured":"Moore, N. (2011). Improving the efficiency of learning CSP solvers. Ph.D. thesis: University of St Andrews."},{"key":"9232_CR26","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R. (2009). Sat modulo theories: Enhancing SAT with special-purpose algorithms. In Theory and Applications of Satisfiability Testing-SAT 2009, pp. 1\u20131. Springer.","DOI":"10.1007\/978-3-642-02777-2_1"},{"key":"9232_CR27","unstructured":"Nieuwenhuis, R., & Oliveras, A. (2007). Rodr\u00edguez-Carbonell, E., Rubio, A.: Challenges in satisfiability modulo theories. In Term Rewriting and Applications, pp. 2\u201318. Springer."},{"issue":"3","key":"9232_CR28","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":"9232_CR29","doi-asserted-by":"crossref","unstructured":"Petke, J., & Jeavons, P. (2011). The order encoding: from tractable CSP to tractable SAT. In Theory and Applications of Satisfiability Testing-SAT 2011, pp. 371\u2013372. Springer.","DOI":"10.1007\/978-3-642-21581-0_34"},{"key":"9232_CR30","unstructured":"R\u00e9gin, J.C. (1994). A filtering algorithm for constraints of difference in CSPs. In AAAI, vol. 94, pp. 362\u2013367."},{"key":"9232_CR31","unstructured":"R\u00e9gin, J.C. (1996). Generalized arc consistency for global cardinality constraint. In Proceedings of the thirteenth national conference on Artificial intelligence-Volume 1, pp. 209\u2013215. AAAI Press."},{"key":"9232_CR32","unstructured":"Rochart, G., Jussien, N., & Laburthe, F. (2003). Challenging explanations for global constraints. In CP03 Workshop on User-Interaction in Constraint Satisfaction (UICS03), pp. 31\u201343."},{"key":"9232_CR33","unstructured":"Rossi, F., Van Beek, P., & Walsh, T. (2006). Handbook of constraint programming: Elsevier."},{"key":"9232_CR34","doi-asserted-by":"crossref","unstructured":"Schulte, C., & Stuckey, P.J. (2004). Speeding up constraint propagation. In Principles and Practice of Constraint Programming\u2013CP 2004, pp. 619\u2013633. Springer.","DOI":"10.1007\/978-3-540-30201-8_45"},{"issue":"3","key":"9232_CR35","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1145\/1065887.1065889","volume":"27","author":"C Schulte","year":"2005","unstructured":"Schulte, C., & Stuckey, P.J. (2005). When do bounds and domain propagation lead to the same search space. ACM Transactions on Programming Languages and Systems (TOPLAS), 27(3), 388\u2013425.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"9232_CR36","doi-asserted-by":"crossref","unstructured":"Sellmann, M., & Kadioglu, S. (2008). Dichotomic search protocols for constrained optimization. In Principles and Practice of Constraint Programming, pp. 251\u2013265. Springer.","DOI":"10.1007\/978-3-540-85958-1_17"},{"key":"9232_CR37","unstructured":"Simonis, H. (2008). Kakuro as a constraint problem. In Proc. seventh Int. Works on Constraint Modelling and Reformulation."},{"key":"9232_CR38","doi-asserted-by":"crossref","unstructured":"Stojadinovi\u0107, M., & Mari\u0107, F. (2014). meSAT: multiple encodings of CSP to SAT. Constraints, 1\u201324.","DOI":"10.1007\/s10601-014-9165-7"},{"key":"9232_CR39","doi-asserted-by":"crossref","unstructured":"Stuckey, P.J. (2010). Lazy clause generation: Combining the power of SAT and CP (and MIP?) solving. In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pp. 5\u20139. Springer.","DOI":"10.1007\/978-3-642-13520-0_3"},{"issue":"2","key":"9232_CR40","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"},{"issue":"2","key":"9232_CR41","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R. (1972). Depth-first search and linear graph algorithms. SIAM Journal Computing, 1(2), 146\u2013160.","journal-title":"SIAM Journal Computing"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-015-9232-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-015-9232-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-015-9232-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-015-9232-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T12:00:34Z","timestamp":1748692834000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-015-9232-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,16]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["9232"],"URL":"https:\/\/doi.org\/10.1007\/s10601-015-9232-8","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"type":"print","value":"1383-7133"},{"type":"electronic","value":"1572-9354"}],"subject":[],"published":{"date-parts":[[2015,11,16]]}}}