{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T00:45:33Z","timestamp":1743122733529,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319232188"},{"type":"electronic","value":"9783319232195"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23219-5_23","type":"book-chapter","created":{"date-parts":[[2015,8,12]],"date-time":"2015-08-12T10:17:33Z","timestamp":1439374653000},"page":"330-340","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Automatically Improving SAT Encoding of Constraint Problems Through Common Subexpression Elimination in Savile Row"],"prefix":"10.1007","author":[{"given":"Peter","family":"Nightingale","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Spracklen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Miguel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,13]]},"reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-540-85958-1_23","volume-title":"Principles and Practice of Constraint Programming","author":"I Araya","year":"2008","unstructured":"Araya, I., Neveu, B., Trombettoni, G.: Exploiting common subexpressions in numerical CSPs. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 342\u2013357. Springer, Heidelberg (2008)"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning sat solvers. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"23_CR4","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press (2009)"},{"issue":"7","key":"23_CR5","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/390013.808480","volume":"5","author":"J Cocke","year":"1970","unstructured":"Cocke, J.: Global common subexpression elimination. ACM Sigplan Notices 5(7), 20\u201324 (1970)","journal-title":"ACM Sigplan Notices"},{"key":"23_CR6","unstructured":"Dincbas, M., Simonis, H., Van Hentenryck, P.: Solving the car-sequencing problem in constraint logic programming. In: Proceedings of the 8th European Conference on Artificial Intelligence (ECAI 1988), pp. 290\u2013295 (1988)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"23_CR8","unstructured":"Gent, I.P.: Arc consistency in SAT. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002), pp. 121\u2013125 (2002)"},{"issue":"3","key":"23_CR9","first-page":"211","volume":"20","author":"IP Gent","year":"2007","unstructured":"Gent, I.P., Jefferson, C., Kelsey, T., Lynce, I., Miguel, I., Nightingale, P., Smith, B.M., Tarim, S.A.: Search in the patience game \u2018black hole\u2019. AI Communications 20(3), 211\u2013226 (2007)","journal-title":"AI Communications"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Gent, I.P., Miguel, I., Rendl, A.: Tailoring solver-independent constraint models: a case study with Essence\n                                        $$^\\prime $$ and Minion. In: Miguel, I., Ruml, W. (eds.) SARA 2007. LNCS (LNAI), vol. 4612, pp. 184\u2013199. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73580-9_16"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-04244-7_7","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"S Huczynska","year":"2009","unstructured":"Huczynska, S., McKay, P., Miguel, I., Nightingale, P.: Modelling equidistant frequency permutation arrays: an application of constraints to mathematics. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 50\u201364. Springer, Heidelberg (2009)"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"23_CR13","unstructured":"Leo, K., Tack, G.: Multi-pass high-level presolving. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI) (to appear, 2015)"},{"key":"23_CR14","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":"23_CR15","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":"23_CR16","unstructured":"Nightingale, P.: CSPLib problem 056: Synchronous optical networking (SONET) problem. http:\/\/www.csplib.org\/Problems\/prob056"},{"issue":"2","key":"23_CR17","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1016\/j.artint.2010.10.005","volume":"175","author":"P Nightingale","year":"2011","unstructured":"Nightingale, P.: The extended global cardinality constraint: An empirical survey. Artificial Intelligence 175(2), 586\u2013614 (2011)","journal-title":"Artificial Intelligence"},{"key":"23_CR18","unstructured":"Nightingale, P.: Savile Row, a constraint modelling assistant (2015). http:\/\/savilerow.cs.st-andrews.ac.uk\/"},{"key":"23_CR19","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":"23_CR20","unstructured":"Rendl, A.: Effective Compilation of Constraint Models. Ph.D. thesis, University of St Andrews (2010)"},{"key":"23_CR21","unstructured":"Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming. Elsevier (2006)"},{"issue":"1","key":"23_CR22","doi-asserted-by":"publisher","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. Journal of Global Optimization 12(1), 61\u201399 (1998)","journal-title":"Journal of Global Optimization"},{"key":"23_CR23","unstructured":"Shlyakhter, I., Sridharan, M., Seater, R., Jackson, D.: Exploiting subformula sharing in automatic analysis of quantified formulas. In: Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003) (2003), poster"},{"key":"23_CR24","unstructured":"Smith, B.: CSPLib problem 001: Car sequencing. http:\/\/www.csplib.org\/Problems\/prob001"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/11493853_25","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"BM Smith","year":"2005","unstructured":"Smith, B.M.: Symmetry and search in a network design problem. In: Bart\u00e1k, R., Milano, M. (eds.) CPAIOR 2005. LNCS, vol. 3524, pp. 336\u2013350. Springer, Heidelberg (2005)"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/11527695_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"S Subbarayan","year":"2005","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"issue":"2","key":"23_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 14(2), 254\u2013272 (2009)","journal-title":"Constraints"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Yan, Y., Gutierrez, C., Jeriah, J.C., Bao, F.S., Zhang, Y.: Accelerating SAT solving by common subclause elimination. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI 2015), pp. 4224\u20134225 (2015)","DOI":"10.1609\/aaai.v29i1.9732"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23219-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T13:49:29Z","timestamp":1674568169000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23219-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319232188","9783319232195"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23219-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"13 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}