{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T20:35:54Z","timestamp":1773693354570,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030584740","type":"print"},{"value":"9783030584757","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-58475-7_9","type":"book-chapter","created":{"date-parts":[[2020,9,6]],"date-time":"2020-09-06T20:02:35Z","timestamp":1599422555000},"page":"143-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Effective Encodings of Constraint Programming Models to SMT"],"prefix":"10.1007","author":[{"given":"Ewan","family":"Davidson","sequence":"first","affiliation":[]},{"given":"\u00d6zg\u00fcr","family":"Akg\u00fcn","sequence":"additional","affiliation":[]},{"given":"Joan","family":"Espasa","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Nightingale","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,2]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Akg\u00fcn, \u00d6., Gent, I.P., Jefferson, C., Miguel, I., Nightingale, P.: Exploiting short supports for improved encoding of arbitrary constraints into SAT. In: Principles and Practice of Constraint Programming - 22nd International Conference, CP, Toulouse, France, pp. 3\u201312 (2016)","DOI":"10.1007\/978-3-319-44953-1_1"},{"issue":"1","key":"9_CR2","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1017\/S1471068417000205","volume":"18","author":"R Amadini","year":"2018","unstructured":"Amadini, R., Gabbrielli, M., Mauro, J.: SUNNY-CP and the MiniZinc challenge. Theory Pract. Log. Programm. 18(1), 81\u201396 (2018). https:\/\/doi.org\/10.1017\/S1471068417000205","journal-title":"Theory Pract. Log. Programm."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bacchus, F.: GAC via unit propagation. In: Principles and Practice of Constraint Programming, 13th International Conference, CP Providence, RI, USA, pp. 133\u2013147 (2007)","DOI":"10.1007\/978-3-540-74970-7_12"},{"key":"9_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-44953-1_4","volume-title":"Principles and Practice of Constraint Programming","author":"G Belov","year":"2016","unstructured":"Belov, G., Stuckey, P.J., Tack, G., Wallace, M.: Improved linearization of constraint programming models. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 49\u201365. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-44953-1_4"},{"key":"9_CR6","unstructured":"Bofill, M., Palah\u0131, M., Suy, J., Villaret, M.: SIMPLY: a compiler from a CSP modeling language to the SMT-LIB format. In: Proceedings of the 8th International Workshop on Constraint Modelling and Reformulation, pp. 30\u201344 (2009)"},{"issue":"3","key":"9_CR7","doi-asserted-by":"publisher","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.: Solving constraint satisfaction problems with SAT modulo theories. Constraints 17(3), 273\u2013303 (2012). https:\/\/doi.org\/10.1007\/s10601-012-9123-1","journal-title":"Constraints"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-10428-7_17","volume-title":"Principles and Practice of Constraint Programming","author":"M Bofill","year":"2014","unstructured":"Bofill, M., Palah\u00ed, M., Suy, J., Villaret, M.: Solving intensional weighted CSPs by incremental optimization with BDDs. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 207\u2013223. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10428-7_17"},{"key":"9_CR9","unstructured":"Contaldo, F., Trentin, P., Sebastiani, R.: From minizinc to optimization modulo theories, and back (extended version). CoRR abs\/1912.01476 (2019). http:\/\/arxiv.org\/abs\/1912.01476"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Davidson, E., Akg\u00fcn, \u00d6., Espasa, J., Nightingale, P.: Experiments for CP2020 SR-SMT paper (2020). https:\/\/doi.org\/10.5281\/zenodo.3953600","DOI":"10.5281\/zenodo.3953600"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Computer Aided Verification - 26th International Conference, CAV Vienna, Austria, pp. 737\u2013744 (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Computer Aided Verification, 18th International Conference, CAV Seattle, WA, USA, pp. 81\u201394 (2006)","DOI":"10.1007\/11817963_11"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Hadarean, L., Bansal, K., Jovanovic, D., Barrett, C.W., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Computer Aided Verification - 26th International Conference, CAV Vienna, Austria, pp. 680\u2013695 (2014)","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-85958-1_10","volume-title":"Principles and Practice of Constraint Programming","author":"J Huang","year":"2008","unstructured":"Huang, J.: Universal booleanization of constraint models. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 144\u2013158. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85958-1_10"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-50497-0","DOI":"10.1007\/978-3-662-50497-0"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS, Budapest, Hungary, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessiere, C. (ed.) Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, Providence, RI, USA, vol. 4741, pp. 529\u2013543 (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_38","DOI":"10.1007\/978-3-540-74970-7_38"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Formal Techniques in Real-Time and Fault-Tolerant Systems, 7th International Symposium, FTRTFT Oldenburg, Germany, pp. 225\u2013244 (2002)","DOI":"10.1007\/3-540-45739-9_15"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector 3.0. In: Computer Aided Verification - 30th International Conference, CAV Oxford, UK, pp. 587\u2013595 (2018)","DOI":"10.1007\/978-3-319-96145-3_32"},{"issue":"6","key":"9_CR20","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","journal-title":"J. ACM"},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.artint.2017.07.001","volume":"251","author":"P Nightingale","year":"2017","unstructured":"Nightingale, P., Akg\u00fcn, \u00d6., Gent, I.P., Jefferson, C., Miguel, I., Spracklen, P.: Automatically improving constraint models in Savile Row. Artif. Intell. 251, 35\u201361 (2017). https:\/\/doi.org\/10.1016\/j.artint.2017.07.001","journal-title":"Artif. Intell."},{"key":"9_CR22","unstructured":"Nightingale, P., Rendl, A.: Essence\u2019 description. Computing Research Repository (CoRR) abs\/1601.02865 (2016), http:\/\/arxiv.org\/abs\/1601.02865"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23219-5_23"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Computer Aided Verification - 27th International Conference, CAV, San Francisco, CA, USA, pp. 447\u2013454 (2015)","DOI":"10.1007\/978-3-319-21690-4_27"},{"key":"9_CR25","unstructured":"Van Hentenryck, P.: The OPL Optimization Programming Language. MIT Press (1999)"}],"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-030-58475-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T05:32:02Z","timestamp":1619242322000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-58475-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030584740","9783030584757"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58475-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"2 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Principles and Practice of Constraint Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Louvain-la-Neuve","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Belgium","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cp2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cp2020.a4cp.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"122","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"45% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.13","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.47","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}