{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:09:53Z","timestamp":1767236993483,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030300470"},{"type":"electronic","value":"9783030300487"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30048-7_2","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:03:06Z","timestamp":1569178986000},"page":"20-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints"],"prefix":"10.1007","author":[{"given":"Carlos","family":"Ans\u00f3tegui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miquel","family":"Bofill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jordi","family":"Coll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nguyen","family":"Dang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan Luis","family":"Esteban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Miguel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Nightingale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s Z.","family":"Salamon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josep","family":"Suy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mateu","family":"Villaret","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-23219-5_1","volume-title":"Principles and Practice of Constraint Programming","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, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23219-5_1"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I. Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Mayer-Eichberger, V.: A new look at BDDs for pseudo-Boolean constraints. J. Artif. Intell. Res. 443\u2013480 (2012). \n                      https:\/\/doi.org\/10.1613\/jair.3653","journal-title":"Journal of Artificial Intelligence Research"},{"unstructured":"Ans\u00f3tegui, C.: Complete SAT solvers for Many-Valued CNF Formulas. Ph.D. thesis, University of Lleida (2004)","key":"2_CR3"},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1142\/S0218213018400018","volume":"27","author":"G Audemard","year":"2018","unstructured":"Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(1), 1\u201325 (2018). \n                      https:\/\/doi.org\/10.1142\/S0218213018400018","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-642-02777-2_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"O Bailleux","year":"2009","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into CNF. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 181\u2013194. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-02777-2_19"},{"unstructured":"Biere, A.: Lingeling. SAT Race (2010)","key":"2_CR6"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-09284-3_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Biere","year":"2014","unstructured":"Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285\u2013301. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-09284-3_22"},{"doi-asserted-by":"publisher","unstructured":"Bofill, M., Coll, J., Suy, J., Villaret, M.: Compact MDDs for pseudo-boolean constraints with at-most-one relations in resource-constrained scheduling problems. In: IJCAI, pp. 555\u2013562 (2017). \n                      https:\/\/doi.org\/10.24963\/ijcai.2017\/78","key":"2_CR8","DOI":"10.24963\/ijcai.2017\/78"},{"key":"2_CR9","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-10428-7_17"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0377-2217(98)00204-5","volume":"112","author":"P Brucker","year":"1999","unstructured":"Brucker, P., Drexl, A., M\u00f6hring, R., Neumann, K., Pesch, E.: Resource-constrained project scheduling: notation, classification, models, and methods. Eur. J. Oper. Res. 112(1), 3\u201341 (1999). \n                      https:\/\/doi.org\/10.1016\/S0377-2217(98)00204-5","journal-title":"Eur. J. Oper. Res."},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/11564751_59","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"S Darras","year":"2005","unstructured":"Darras, S., Dequen, G., Devendeville, L., Mazure, B., Ostrowski, R., Sa\u00efs, L.: Using Boolean Constraint Propagation for sub-clauses deduction. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 757\u2013761. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11564751_59"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10951-010-0211-z","volume":"14","author":"P Causmaecker De","year":"2011","unstructured":"De Causmaecker, P., Vanden Berghe, G.: A categorisation of nurse rostering problems. J. Sched. 14(1), 3\u201316 (2011). \n                      https:\/\/doi.org\/10.1007\/s10951-010-0211-z","journal-title":"J. Sched."},{"unstructured":"E\u00e9n, N., Sorensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2, 1\u201326 (2006). \n                      http:\/\/satassociation.org\/jsat\/index.php\/jsat\/article\/view\/18","key":"2_CR13"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-72397-4_6","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"O Fourdrinoy","year":"2007","unstructured":"Fourdrinoy, O., Gr\u00e9goire, \u00c9., Mazure, B., Sa\u00efs, L.: Eliminating redundant clauses in SAT instances. In: Van Hentenryck, P., Wolsey, L. (eds.) CPAIOR 2007. LNCS, vol. 4510, pp. 71\u201383. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-72397-4_6"},{"unstructured":"Gent, I.P., Jefferson, C., Miguel, I.: Minion: a fast scalable constraint solver. In: ECAI: European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol. 141, pp. 98\u2013102. IOS Press (2006). \n                      http:\/\/www.booksonline.iospress.nl\/Content\/View.aspx?piid=1654","key":"2_CR15"},{"issue":"1","key":"2_CR16","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/j.cor.2009.04.006","volume":"37","author":"B Han","year":"2010","unstructured":"Han, B., Leblet, J., Simon, G.: Hard multidimensional multiple choice knapsack problems, an empirical study. Comput. Oper. Res. 37(1), 172\u2013181 (2010). \n                      https:\/\/doi.org\/10.1016\/j.cor.2009.04.006","journal-title":"Comput. Oper. Res."},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-33347-7_10","volume-title":"KI 2012: Advances in Artificial Intelligence","author":"S H\u00f6lldobler","year":"2012","unstructured":"H\u00f6lldobler, S., Manthey, N., Steinke, P.: A compact encoding of pseudo-boolean constraints into SAT. In: Glimm, B., Kr\u00fcger, A. (eds.) KI 2012. LNCS (LNAI), vol. 7526, pp. 107\u2013118. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-33347-7_10"},{"key":"2_CR18","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-85958-1_10"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-319-23219-5_15","volume-title":"Principles and Practice of Constraint Programming","author":"S Joshi","year":"2015","unstructured":"Joshi, S., Martins, R., Manquinho, V.: Generalized totalizer encoding for pseudo-boolean constraints. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 200\u2013209. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23219-5_15"},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-540-24777-7_9","volume-title":"Knapsack Problems","author":"Hans Kellerer","year":"2004","unstructured":"Kellerer, H., Pferschy, U., Pisinger, D.: Multidimensional knapsack problems. In: Knapsack Problems, pp. 235\u2013283. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24777-7_9"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/S0377-2217(96)00170-1","volume":"96","author":"R Kolisch","year":"1997","unstructured":"Kolisch, R., Sprecher, A.: PSPLIB - a project scheduling problem library. Eur. J. Oper. Res. 96(1), 205\u2013216 (1997). \n                      https:\/\/doi.org\/10.1016\/S0377-2217(96)00170-1","journal-title":"Eur. J. Oper. Res."},{"doi-asserted-by":"crossref","unstructured":"Leyton-Brown, K., Shoham, Y.: A test suite for combinatorial auctions. In: Combinatorial Auctions, chap. 18, pp. 451\u2013478. The MIT Press (2006)","key":"2_CR22","DOI":"10.7551\/mitpress\/9780262033428.003.0019"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-319-09284-3_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"R Martins","year":"2014","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver\u2019. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438\u2013445. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-09284-3_33"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529\u2013543. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74970-7_38"},{"key":"2_CR25","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). \n                      https:\/\/doi.org\/10.1016\/j.artint.2017.07.001","journal-title":"Artif. Intell."},{"unstructured":"Nightingale, P., Rendl, A.: Essence\u2019 description. \n                      arXiv:1601.02865\n                      \n                     (2016)","key":"2_CR26"},{"unstructured":"Vanhoucke, M., Maenhout, B.: NSPLib: a nurse scheduling problem library: a tool to evaluate (meta-)heuristic procedures. In: Brailsford, S., Harper, P. (eds.) Operational research for health policy: making better decisions, pp. 151\u2013165. Peter Lang (2007)","key":"2_CR27"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-319-28228-2_4","volume-title":"Practical Aspects of Declarative Languages","author":"N-F Zhou","year":"2016","unstructured":"Zhou, N.-F., Kjellerstrand, H.: The Picat-SAT compiler. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016. LNCS, vol. 9585, pp. 48\u201362. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-28228-2_4"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30048-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T16:03:03Z","timestamp":1569427383000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30048-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030300470","9783030300487"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30048-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","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":"Stamford, CT","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cp2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cp2019.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":"118","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":"46","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":"39% - 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.2","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":"4","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)"}}]}}