{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T02:52:48Z","timestamp":1772765568939,"version":"3.50.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T00:00:00Z","timestamp":1581984000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T00:00:00Z","timestamp":1581984000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100008722","name":"Universitat de Girona","doi-asserted-by":"publisher","award":["MPCUdG2016\/055"],"award-info":[{"award-number":["MPCUdG2016\/055"]}],"id":[{"id":"10.13039\/100008722","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008722","name":"Universitat de Girona","doi-asserted-by":"publisher","award":["MPCUdG2016\/055"],"award-info":[{"award-number":["MPCUdG2016\/055"]}],"id":[{"id":"10.13039\/100008722","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008722","name":"Universitat de Girona","doi-asserted-by":"publisher","award":["MPCUdG2016\/055"],"award-info":[{"award-number":["MPCUdG2016\/055"]}],"id":[{"id":"10.13039\/100008722","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008722","name":"Universitat de Girona","doi-asserted-by":"publisher","award":["MPCUdG2016\/055"],"award-info":[{"award-number":["MPCUdG2016\/055"]}],"id":[{"id":"10.13039\/100008722","id-type":"DOI","asserted-by":"publisher"}]},{"name":"MINECO\/FEDER, UE","award":["TIN2015-66293-R"],"award-info":[{"award-number":["TIN2015-66293-R"]}]},{"name":"MINECO\/FEDER, UE","award":["TIN2015-66293-R"],"award-info":[{"award-number":["TIN2015-66293-R"]}]},{"name":"MINECO\/FEDER, UE","award":["TIN2015-66293-R"],"award-info":[{"award-number":["TIN2015-66293-R"]}]},{"name":"MINECO\/FEDER, UE","award":["TIN2015-66293-R"],"award-info":[{"award-number":["TIN2015-66293-R"]}]},{"name":"MINECO and FSE, Ayudas para Contratos Predoctorales","award":["BES-2016-076867"],"award-info":[{"award-number":["BES-2016-076867"]}]},{"name":"MICINN\/FEDER, UE","award":["RTI2018-095609-B-I00"],"award-info":[{"award-number":["RTI2018-095609-B-I00"]}]},{"name":"MICINN\/FEDER, UE","award":["RTI2018-095609-B-I00"],"award-info":[{"award-number":["RTI2018-095609-B-I00"]}]},{"name":"MICINN\/FEDER, UE","award":["RTI2018-095609-B-I00"],"award-info":[{"award-number":["RTI2018-095609-B-I00"]}]},{"name":"MICINN\/FEDER, UE","award":["RTI2018-095609-B-I00"],"award-info":[{"award-number":["RTI2018-095609-B-I00"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Artif Intell Rev"],"published-print":{"date-parts":[[2020,10]]},"DOI":"10.1007\/s10462-020-09817-6","type":"journal-article","created":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T07:02:40Z","timestamp":1582009360000},"page":"5157-5188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations"],"prefix":"10.1007","volume":"53","author":[{"given":"Miquel","family":"Bofill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9385-5723","authenticated-orcid":false,"given":"Jordi","family":"Coll","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":[[2020,2,18]]},"reference":[{"key":"9817_CR1","doi-asserted-by":"crossref","unstructured":"Ab\u00edo I, Stuckey PJ (2014) Encoding linear constraints into SAT. In: International conference on principles and practice of constraint programming (CP), lecture notes in computer science, vol 8656, pp 75\u201391","DOI":"10.1007\/978-3-319-10428-7_9"},{"key":"9817_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 (2012) A new look at BDDs for pseudo-Boolean constraints. J Artif Intell Res 45:443\u2013480","journal-title":"J Artif Intell Res"},{"key":"9817_CR3","doi-asserted-by":"crossref","unstructured":"Ab\u00edo I, Mayer-Eichberger V, Stuckey PJ (2015) Encoding linear constraints with implication chains to CNF. In: International conference on principles and practice of constraint programming (CP), lecture notes in computer science, vol 9255, Springer, pp 3\u201311","DOI":"10.1007\/978-3-319-23219-5_1"},{"key":"9817_CR4","doi-asserted-by":"crossref","unstructured":"Ab\u00edo I, Gange G, Mayer-Eichberger V, Stuckey PJ (2016) On CNF encodings of decision diagrams. In: 13th International conference on integration of AI and OR techniques in constraint programming (CPAIOR), lecture notes in computer science, vol 9676, pp 1\u201317","DOI":"10.1007\/978-3-319-33954-2_1"},{"key":"9817_CR5","unstructured":"Bacchus F, Winter J (2003) Effective preprocessing with hyper-resolution and equality reduction. In: International conference on theory and applications of satisfiability testing (SAT), lecture notes in computer science, vol 2919, pp 341\u2013355"},{"key":"9817_CR6","first-page":"191","volume":"2","author":"O Bailleux","year":"2006","unstructured":"Bailleux O, Boufkhad Y, Roussel O (2006) A translation of pseudo-boolean constraints to SAT. J Satisf Boolean Model Comput 2:191\u2013200","journal-title":"J Satisf Boolean Model Comput"},{"key":"9817_CR7","doi-asserted-by":"crossref","unstructured":"Bailleux O, Boufkhad Y, Roussel O (2009) New encodings of pseudo-boolean constraints into CNF. In: International conference on theory and applications of satisfiability testing (SAT), lecture notes in computer science, vol 5584, pp 181\u2013194","DOI":"10.1007\/978-3-642-02777-2_19"},{"issue":"2","key":"9817_CR8","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/s10601-012-9130-2","volume":"18","author":"M Bofill","year":"2013","unstructured":"Bofill M, Busquets D, Mu\u00f1oz V, Villaret M (2013) Reformulation based MaxSAT robustness. Constraints 18(2):202\u2013235","journal-title":"Constraints"},{"key":"9817_CR9","doi-asserted-by":"publisher","unstructured":"Bofill M, Palah\u00ed M, Suy J, Villaret M (2014) Solving intensional weighted CSPs by incremental optimization with BDDs. In: Prodeedings of the 20th international conference on principles and practice of constraint programming, CP2014, pp 207\u2013223. https:\/\/doi.org\/10.1007\/978-3-319-10428-7_17","DOI":"10.1007\/978-3-319-10428-7_17"},{"key":"9817_CR10","doi-asserted-by":"crossref","unstructured":"Bofill M, Coll J, Suy J, Villaret M (2016) Solving the multi-mode resource-constrained project scheduling problem with SMT. In: 28th IEEE international conference on tools with artificial intelligence (ICTAI), pp 239\u2013246","DOI":"10.1109\/ICTAI.2016.0045"},{"key":"9817_CR11","doi-asserted-by":"crossref","unstructured":"Bofill M, Coll J, Suy J, Villaret M (2017) Compact MDDs for pseudo-Boolean constraints with at-most-one relations in resource-constrained scheduling problems. In: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI), pp 555\u2013562","DOI":"10.24963\/ijcai.2017\/78"},{"key":"9817_CR12","doi-asserted-by":"publisher","unstructured":"Bofill M, Coll J, Suy J, Villaret M (2019) SAT encodings of pseudo-Boolean constraints with at-most-one relations. In: Proceedings of the 16th international conference of integration of constraint programming, artificial intelligence, and operations reserarch (CPAIOR), pp 112\u2013128. https:\/\/doi.org\/10.1007\/978-3-030-19212-9_8","DOI":"10.1007\/978-3-030-19212-9_8"},{"issue":"1","key":"9817_CR13","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 (1999) Resource-constrained project scheduling: notation, classification, models, and methods. Eur J Oper Res 112(1):3\u201341","journal-title":"Eur J Oper Res"},{"issue":"1","key":"9817_CR14","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1287\/mnsc.6.1.80","volume":"6","author":"GB Dantzig","year":"1959","unstructured":"Dantzig GB, Ramser JH (1959) The truck dispatching problem. Manag Sci 6(1):80\u201391","journal-title":"Manag Sci"},{"issue":"3","key":"9817_CR15","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1287\/ijoc.15.3.284.16077","volume":"15","author":"S De Vries","year":"2003","unstructured":"De Vries S, Vohra RV (2003) Combinatorial auctions: a survey. INFORMS J Comput 15(3):284\u2013309","journal-title":"INFORMS J Comput"},{"key":"9817_CR16","unstructured":"Dutertre B, de\u00a0Moura L (2006) The Yices SMT solver. Tech. rep., Computer Science Laboratory, SRI International, available at http:\/\/yices.csl.sri.com"},{"key":"9817_CR17","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: International conference on theory and applications of satisfiability testing (SAT), lecture notes in computer science, vol 3569, pp 61\u201375","DOI":"10.1007\/11499107_5"},{"key":"9817_CR18","first-page":"1","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n N, Sorensson N (2006) Translating pseudo-boolean constraints into SAT. J Satisf Boolean Model Comput 2:1\u201326","journal-title":"J Satisf Boolean Model Comput"},{"issue":"1\u20132","key":"9817_CR19","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/s10696-012-9141-8","volume":"25","author":"S Hartmann","year":"2013","unstructured":"Hartmann S (2013) Project scheduling with resource capacities and requests varying with time: a case study. Flex Serv Manuf J 25(1\u20132):74\u201393","journal-title":"Flex Serv Manuf J"},{"key":"9817_CR20","doi-asserted-by":"crossref","unstructured":"H\u00f6lldobler S, Manthey N, Steinke P (2012) A compact encoding of pseudo-Boolean constraints into SAT. In: KI 2012: advances in artificial intelligence 35th annual german conference on artificial intelligence, lecture notes in computer science, vol 7526, pp 107\u2013118","DOI":"10.1007\/978-3-642-33347-7_10"},{"key":"9817_CR21","doi-asserted-by":"crossref","unstructured":"Hosaka K, Takenaga Y, Yajima S (1994) On the size of ordered binary decision diagrams representing threshold functions. In: 5th International symposium on algorithms and computation (ISAAC), lecture notes in computer science, vol 834, pp 584\u2013592","DOI":"10.1007\/3-540-58325-4_226"},{"key":"9817_CR22","doi-asserted-by":"crossref","unstructured":"Joshi S, Martins R, Manquinho VM (2015) Generalized totalizer encoding for pseudo-boolean constraints. In: Principles and practice of constraint programming\u2014CP 2015, 21st international conference, LNCS, vol 9255, Springer, pp 200\u2013209","DOI":"10.1007\/978-3-319-23219-5_15"},{"key":"9817_CR23","doi-asserted-by":"publisher","unstructured":"Kellerer H, Pferschy U, Pisinger D (2004) Multidimensional knapsack problems. In: Knapsack problems, Springer, Berlin, pp 235\u2013283. https:\/\/doi.org\/10.1007\/978-3-540-24777-7_9","DOI":"10.1007\/978-3-540-24777-7_9"},{"issue":"1","key":"9817_CR24","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 (1997) PSPLIB: a project scheduling problem library. Eur J Oper Res 96(1):205\u2013216","journal-title":"Eur J Oper Res"},{"issue":"3","key":"9817_CR25","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1016\/0377-2217(92)90192-C","volume":"59","author":"G Laporte","year":"1992","unstructured":"Laporte G (1992) The vehicle routing problem: an overview of exact and approximate algorithms. Eur J Oper Res 59(3):345\u2013358","journal-title":"Eur J Oper Res"},{"key":"9817_CR26","unstructured":"Leyton-Brown K, Shoham Y (2006) A test suite for combinatorial auctions. In: Combinatorial auctions, The MIT Press, chap 18, pp 451\u2013478"},{"issue":"4","key":"9817_CR27","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1145\/321043.321046","volume":"7","author":"CE Miller","year":"1960","unstructured":"Miller CE, Tucker AW, Zemlin RA (1960) Integer programming formulation of traveling salesman problems. J ACM 7(4):326\u2013329","journal-title":"J ACM"},{"key":"9817_CR28","doi-asserted-by":"crossref","unstructured":"Philipp T, Steinke P (2015) PBLib\u2013a library for encoding pseudo-boolean constraints into CNF. In: International conference on theory and applications of satisfiability testing (SAT), lecture notes in computer science, vol 9340, pp 9\u201316","DOI":"10.1007\/978-3-319-24318-4_2"},{"key":"9817_CR29","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1287\/mnsc.16.1.93","volume":"16","author":"AAB Pritsker","year":"1996","unstructured":"Pritsker AAB, Waiters LJ, Wlofe PM (1996) Multiproject scheduling with limited resources: a zero-one programming approach. Manag Sci 16:93\u2013108","journal-title":"Manag Sci"},{"key":"9817_CR30","doi-asserted-by":"crossref","unstructured":"Srinivasan A, Ham T, Malik S, Brayton RK (1990) Algorithms for discrete function manipulation. In: IEEE international conference on computer-aided design (ICCAD), IEEE, pp 92\u201395","DOI":"10.1109\/ICCAD.1990.129849"},{"key":"9817_CR31","doi-asserted-by":"crossref","unstructured":"Tamura N, Banbara M, Soh T (2013) Compiling pseudo-boolean constraints to SAT with order encoding. In: 25th IEEE international conference on tools with artificial intelligence (ICTAI), pp 1020\u20131027","DOI":"10.1109\/ICTAI.2013.153"},{"issue":"1","key":"9817_CR32","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.ejor.2013.10.012","volume":"235","author":"V Van Peteghem","year":"2014","unstructured":"Van Peteghem V, Vanhoucke M (2014) An experimental investigation of metaheuristics for the multi-mode resource-constrained project scheduling problem on new dataset instances. Eur J Oper Res 235(1):62\u201372","journal-title":"Eur J Oper Res"}],"container-title":["Artificial Intelligence Review"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10462-020-09817-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10462-020-09817-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10462-020-09817-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,19]],"date-time":"2021-02-19T13:55:47Z","timestamp":1613742947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10462-020-09817-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,18]]},"references-count":32,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["9817"],"URL":"https:\/\/doi.org\/10.1007\/s10462-020-09817-6","relation":{},"ISSN":["0269-2821","1573-7462"],"issn-type":[{"value":"0269-2821","type":"print"},{"value":"1573-7462","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,18]]},"assertion":[{"value":"18 February 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}