{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T06:49:39Z","timestamp":1743058179827,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319070452"},{"type":"electronic","value":"9783319070469"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07046-9_18","type":"book-chapter","created":{"date-parts":[[2014,5,12]],"date-time":"2014-05-12T02:07:28Z","timestamp":1399860448000},"page":"251-267","source":"Crossref","is-referenced-by-count":6,"title":["Representative Encodings to Translate Finite CSPs into SAT"],"prefix":"10.1007","author":[{"given":"Pedro","family":"Barahona","sequence":"first","affiliation":[]},{"given":"Steffen","family":"H\u00f6lldobler","sequence":"additional","affiliation":[]},{"given":"Van-Hau","family":"Nguyen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Ans\u00f3tegui, C., del Val, A., Dot\u00fa, I., Fern\u00e1ndez, C., Many\u00e0, F.: Modeling Choices in Quasigroup Completion: SAT vs. CSP. In: McGuinness, D.L., Ferguson, G. (eds.) Proceedings of the 19th National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, pp. 137\u2013142. AAAI Press \/ The MIT Press (2004)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O. Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean Cardinality Constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, pp. 108\u2013122. Springer, Heidelberg (2003)"},{"key":"18_CR3","unstructured":"Barahona, P., H\u00f6lldobler, S., Nguyen, V.H.: Efficient SAT-Encoding of Linear CSP Constraints. In: 13rd International Symposium on Artificial Intelligence and Mathematics - ISAIM, Fort Lauderdale, Florida, USA, January 6-8 (2014)"},{"key":"18_CR4","unstructured":"Berre, D.L., Lynce, I.: CSP2SAT4J: A Simple CSP to SAT Translator. In: van Dongen, M., Lecotre, C., Rossel, O. (eds.) Proceedings of the Second International CSP Solver Competition, pp. 43\u201354 (2006)"},{"key":"18_CR5","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013. In: Adrian Balint, A.B., Heule, M., J\u00e4rvisalo, M. (eds.) Proceedings of SAT Competition 2013, pp. 51\u201352 (2013)"},{"issue":"1-2","key":"18_CR6","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.artint.2004.01.006","volume":"162","author":"M. Cadoli","year":"2005","unstructured":"Cadoli, M., Schaerf, A.: Compiling Problem Specifications into SAT. Artificial Intelligence\u00a0162(1-2), 89\u2013120 (2005)","journal-title":"Artificial Intelligence"},{"key":"18_CR7","unstructured":"Crawford, J.M., Baker, A.B.: Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems. In: Hayes-Roth, B., Korf, R.E. (eds.) Proceedings of the 12th National Conference on Artificial Intelligence, vol.\u00a02, pp. 1092\u20131097. AAAI Press \/ The MIT Press (1994)"},{"key":"18_CR8","unstructured":"Frisch, A.M., Giannoros, P.A.: SAT Encodings of the At-Most-k Constraint. Some Old, Some New, Some Fast, Some Slow. In: Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation (2010)"},{"key":"18_CR9","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":"18_CR10","doi-asserted-by":"crossref","unstructured":"Gebser, M., Kaufmann, B., Schaub, T.: The Conflict-Driven Answer Set Solver clasp: Progress Report. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol.\u00a05753, pp. 509\u2013514. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-04238-6_50"},{"key":"18_CR11","unstructured":"Gent, I.P.: Arc Consistency in SAT. In: van Harmelen, F. (ed.) Proceedings of the 15th Eureopean Conference on Artificial Intelligence, ECAI 2002, pp. 121\u2013125. IOS Press (2002)"},{"key":"18_CR12","unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V., Steinke, P.: Solving Hidokus Using SAT Solvers. In: Proc. INFOCOM-5, pp. 208\u2013212 (2012) ISSN 2219-293X"},{"key":"18_CR13","unstructured":"H\u00f6lldobler, S., Nguyen, V.H.: On SAT-Encodings of the At-Most-One Constraint. In: Katsirelos, G., Quimper, C.G. (eds.) Proc. Twelfth International Workshop on Constraint Modelling and Reformulation, Uppsala, Sweden, September 16-20, pp. 1\u201317 (2013)"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1613\/jair.3531","volume":"43","author":"P. Jeavons","year":"2012","unstructured":"Jeavons, P., Petke, J.: Local Consistency and SAT-Solvers. J. Artif. Intell. Res (JAIR)\u00a043, 329\u2013351 (2012)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"1514","DOI":"10.1016\/j.dam.2006.10.004","volume":"155","author":"H. Kautz","year":"2007","unstructured":"Kautz, H., Selman, B.: The State of SAT. Discrete Appl. Math.\u00a0155, 1514\u20131524 (2007)","journal-title":"Discrete Appl. Math."},{"key":"18_CR16","unstructured":"de Kleer, J.: A Comparison of ATMS and CSP Techniques. In: IJCAI, pp. 290\u2013296 (1989)"},{"key":"18_CR17","unstructured":"Manthey, N.: The SAT Solver RISS3G at SC 2013. Department of Computer Science Series of Publications B, vol. B-2013-1, pp. 72\u201373. University of Helsinki, Helsinki, Finland (2013)"},{"issue":"4-5","key":"18_CR18","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1017\/S1471068412000130","volume":"12","author":"A. Metodi","year":"2012","unstructured":"Metodi, A., Codish, M.: Compiling Finite Domain Constraints to SAT with BEE. Theory and Practice of Logic Programming\u00a012(4-5), 465\u2013483 (2012)","journal-title":"Theory and Practice of Logic Programming"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Nguyen, V.H., Velev, M.N., Barahona, P.: Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. In: Brodsky, A. (ed.) Proc. 2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI 2013), Special Track on SAT and CSP. pp. 1028\u20131035. Conference Publishing Services (2013)","DOI":"10.1109\/ICTAI.2013.154"},{"issue":"3","key":"18_CR20","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O. Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P., Codish, M.: Propagation via Lazy Clause Generation. Constraints\u00a014(3), 357\u2013391 (2009)","journal-title":"Constraints"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-30201-8_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"S.D. Prestwich","year":"2004","unstructured":"Prestwich, S.D.: Full Dynamic Substitutability by SAT Encoding. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 512\u2013526. Springer, Heidelberg (2004)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-540-24605-3_9","volume-title":"Theory and Applications of Satisfiability Testing","author":"S.D. Prestwich","year":"2004","unstructured":"Prestwich, S.D.: Local Search on SAT-encoded Colouring Problems. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 105\u2013119. Springer, Heidelberg (2004)"},{"key":"18_CR23","unstructured":"Prestwich, S.D.: CNF Encodings, ch.\u00a02, pp. 75\u201398. IOS Press (2009)"},{"key":"18_CR24","volume-title":"Handbook of Constraint Programming (Foundations of Artificial Intelligence)","author":"F. Rossi","year":"2006","unstructured":"Rossi, F., Beek, P.V., Walsh, T.: Handbook of Constraint Programming (Foundations of Artificial Intelligence). Elsevier Science Inc., New York (2006)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-74970-7_35","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"J. Marques-Silva","year":"2007","unstructured":"Marques-Silva, J., Lynce, I.: Towards Robust CNF Encodings of Cardinality Constraints. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 483\u2013497. Springer, Heidelberg (2007)"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C. Sinz","year":"2005","unstructured":"Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 827\u2013831. Springer, Heidelberg (2005)"},{"key":"18_CR27","unstructured":"Taillard, \u00c9.: \n                    http:\/\/mistic.heig-vd.ch\/taillard\/problemes.dir\/ordonnancement.dir\/ordonnancement.html"},{"issue":"2","key":"18_CR28","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(2), 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-21581-0_36","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"T. Tanjo","year":"2011","unstructured":"Tanjo, T., Tamura, N., Banbara, M.: A Compact and Efficient SAT-Encoding of Finite Domain CSP. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 375\u2013376. Springer, Heidelberg (2011)"},{"key":"18_CR30","unstructured":"Trick, M.: DIMACS Graph-Coloring Problems, \n                    http:\/\/mat.gsia.cmu.edu\/COLOR\/instances.html"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Exploiting Hierarchy and Structure to Efficiently Solve Graph Coloring as SAT. In: International Conference on Computer-Aided Design (ICCAD 2007), San Jose, CA, USA, pp. 135\u2013142. IEEE (2007)","DOI":"10.1109\/ICCAD.2007.4397256"},{"key":"18_CR32","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)"}],"container-title":["Lecture Notes in Computer Science","Integration of AI and OR Techniques in Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07046-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,29]],"date-time":"2020-12-29T01:23:16Z","timestamp":1609204996000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-07046-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319070452","9783319070469"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07046-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}