{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:27:37Z","timestamp":1725863257233},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319449524"},{"type":"electronic","value":"9783319449531"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-44953-1_1","type":"book-chapter","created":{"date-parts":[[2016,8,22]],"date-time":"2016-08-22T15:12:23Z","timestamp":1471878743000},"page":"3-12","source":"Crossref","is-referenced-by-count":3,"title":["Exploiting Short Supports for Improved Encoding of Arbitrary Constraints into SAT"],"prefix":"10.1007","author":[{"given":"\u00d6zg\u00fcr","family":"Akg\u00fcn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian P.","family":"Gent","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christopher","family":"Jefferson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Miguel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter\u00a0","family":"Nightingale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,23]]},"reference":[{"key":"1_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-23219-5_1","volume-title":"CP 2015","author":"I Ab\u00edo","year":"2015","unstructured":"Ab\u00edo, I., Mayer-Eichberger, V., Stuckey, P.J.: Encoding linear constraints with implication chains to CNF. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 3\u201311. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-23219-5_1"},{"issue":"2","key":"1_CR2","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011). doi: 10.1007\/s10601-010-9105-0","journal-title":"Constraints"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-540-74970-7_12","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"F Bacchus","year":"2007","unstructured":"Bacchus, F.: GAC via unit propagation. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 133\u2013147. Springer, Heidelberg (2007)"},{"key":"1_CR4","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Proceedings of SAT Competition, pp. 51\u201352 (2013)"},{"key":"1_CR5","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/978-3-662-49122-5_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Brain","year":"2016","unstructured":"Brain, M., Hadarean, L., Kroening, D., Martins, R.: Automatic generation of propagation complete SAT encodings. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 536\u2013556. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49122-5_26"},{"issue":"2","key":"1_CR7","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s10601-009-9087-y","volume":"15","author":"KCK Cheng","year":"2010","unstructured":"Cheng, K.C.K., Yap, R.H.C.: An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints. Constraints 15(2), 265\u2013304 (2010)","journal-title":"Constraints"},{"issue":"1\u20134","key":"1_CR8","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1\u20134), 1\u201326 (2006). http:\/\/jsat.ewi.tudelft.nl\/content\/volume2\/JSAT2_1_Een.pdf","journal-title":"JSAT"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/978-3-642-15396-9_19","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2010","author":"IP Gent","year":"2010","unstructured":"Gent, I.P., Jefferson, C., Miguel, I., Nightingale, P.: Generating special-purpose stateless propagators for arbitrary constraints. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 206\u2013220. Springer, Heidelberg (2010)"},{"key":"1_CR10","unstructured":"Gent, I.P., Nightingale, P.: A new encoding of alldifferent into SAT. In: Proceedings 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (ModRef 2004), pp. 95\u2013110 (2004)"},{"key":"1_CR11","doi-asserted-by":"crossref","first-page":"1407","DOI":"10.1016\/j.artint.2010.07.001","volume":"174","author":"C Jefferson","year":"2010","unstructured":"Jefferson, C., Moore, N., Nightingale, P., Petrie, K.E.: Implementing logical connectives in constraint programming. Artif. Intell. 174, 1407\u20131429 (2010)","journal-title":"Artif. Intell."},{"key":"1_CR12","unstructured":"Jefferson, C., Nightingale, P.: Extending simple tabular reduction with short supports. In: Proceedings of 23rd International Joint Conference on Artificial Intelligence (IJCAI), pp. 573\u2013579 (2013)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Katsirelos, G., Walsh, T.: A compression algorithm for large arity extensional constraints. In: Proceedings of the CP 2007, pp. 379\u2013393 (2007)","DOI":"10.1007\/978-3-540-74970-7_28"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-319-18008-3_19","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"J-B Mairy","year":"2015","unstructured":"Mairy, J.-B., Deville, Y., Lecoutre, C.: The smart table constraint. In: Michel, L. (ed.) CPAIOR 2015. LNCS, vol. 9075, pp. 271\u2013287. Springer, Heidelberg (2015)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.: Practical applications of boolean satisfiability. In: 9th International Workshop on Discrete Event Systems (WODES 2008), pp. 74\u201380 (2008)","DOI":"10.1109\/WODES.2008.4605925"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1007\/978-3-319-10428-7_43","volume-title":"Principles and Practice of Constraint Programming","author":"P Nightingale","year":"2014","unstructured":"Nightingale, P., Akg\u00fcn, \u00d6., Gent, I.P., Jefferson, C., Miguel, I.: Automatically improving constraint models in savile row through associative-commutative common subexpression elimination. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 590\u2013605. Springer, Heidelberg (2014)"},{"key":"1_CR18","unstructured":"Nightingale, P., Gent, I.P., Jefferson, C., Miguel, I.: Exploiting short supports for generalised arc consistency for arbitrary constraints. In: Proceedings of the IJCAI 2011, pp. 623\u2013628 (2011)"},{"key":"1_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1613\/jair.3749","volume":"46","author":"P Nightingale","year":"2013","unstructured":"Nightingale, P., Gent, I.P., Jefferson, C., Miguel, I.: Short and long supports for constraint propagation. J. Artif. Intell. Res. 46, 1\u201345 (2013)","journal-title":"J. Artif. Intell. Res."},{"key":"1_CR20","unstructured":"Nightingale, P., Rendl, A.: Essence\u2019 description (2016). arXiv:1601.02865 [cs.AI]"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1007\/978-3-319-23219-5_23","volume-title":"Principles and Practice of Constraint Programming","author":"P Nightingale","year":"2015","unstructured":"Nightingale, P., Spracklen, P., Miguel, I.: Automatically improving SAT encoding of constraint problems through common subexpression elimination in savile row. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 330\u2013340. Springer, Heidelberg (2015)"},{"key":"1_CR22","unstructured":"R\u00e9gin, J.: Improving the expressiveness of table constraints. In: The 10th International Workshop on Constraint Modelling and Reformulation (ModRef 2011) (2011)"},{"issue":"1","key":"1_CR23","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1023\/A:1008287028851","volume":"12","author":"Y Shang","year":"1998","unstructured":"Shang, Y., Wah, B.W.: A discrete Lagrangian-based global-search method for solving satisfiability problems. J. Glob. Optimi. 12(1), 61\u201399 (1998)","journal-title":"J. Glob. Optimi."},{"key":"1_CR24","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. 4741, pp. 483\u2013497. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74970-7_35"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Simonis, H., O\u2019Sullivan, B.: Search strategies for rectangle packing. In: Proceedings of the CP 2008, pp. 52\u201366 (2008)","DOI":"10.1007\/978-3-540-85958-1_4"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/978-3-642-38171-3_18","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"PJ Stuckey","year":"2013","unstructured":"Stuckey, P.J., Tack, G.: MiniZinc with functions. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 268\u2013283. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44953-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T21:12:12Z","timestamp":1568322732000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44953-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319449524","9783319449531"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44953-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}