{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:11:58Z","timestamp":1767237118987},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661575"},{"type":"electronic","value":"9783319661582"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66158-2_5","type":"book-chapter","created":{"date-parts":[[2017,8,22]],"date-time":"2017-08-22T07:24:38Z","timestamp":1503386678000},"page":"71-79","source":"Crossref","is-referenced-by-count":2,"title":["An Efficient SMT Approach to Solve MRCPSP\/max Instances with Tight Constraints on Resources"],"prefix":"10.1007","author":[{"given":"Miquel","family":"Bofill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":[[2017,8,23]]},"reference":[{"key":"5_CR1","unstructured":"Ans\u00f3tegui, C., Bofill, M., Palah\u00ed, M., Suy, J., Villaret, M.: Satisfiability modulo theories: an efficient approach for the resource-constrained project scheduling problem. In: Proceedings of the Ninth Symposium on Abstraction, Reformulation, and Approximation (SARA), pp. 2\u20139. AAAI (2011)"},{"key":"5_CR2","volume-title":"Resource-Constrained Project Scheduling: Models, Algorithms, Extensions and Applications","author":"C Artigues","year":"2013","unstructured":"Artigues, C., Demassey, S., Neron, E.: Resource-Constrained Project Scheduling: Models, Algorithms, Extensions and Applications. Wiley, Hoboken (2013)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bofill, M., Coll, J., Suy, J., Villaret, M.: Solving the multi-mode resource-constrained project scheduling problem with SMT. In: 28th International Conference on Tools with Artificial Intelligence (ICTAI), pp. 239\u2013246. IEEE (2016)","DOI":"10.1109\/ICTAI.2016.0045"},{"key":"5_CR4","doi-asserted-by":"crossref","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: International Joint Conference on Artificial Intelligence (IJCAI) (2017, to appear)","DOI":"10.24963\/ijcai.2017\/78"},{"issue":"1","key":"5_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0377-2217(98)00204-5","volume":"112","author":"P Brucker","year":"1999","unstructured":"Brucker, P., Drexl, A., Mhring, R., Neumann, K., Pesch, E.: Resource-constrained project scheduling: notation, classification, models, and methods. Eur. J. Oper. Res. 112(1), 3\u201341 (1999)","journal-title":"Eur. J. Oper. Res."},{"key":"5_CR6","unstructured":"Dutertre, B., de Moura, L.: The yices SMT solver. Technical report, Computer Science Laboratory, SRI International (2006). http:\/\/yices.csl.sri.com"},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., Sorensson, N.: Translating pseudo-Boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2, 1\u201326 (2006)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"5_CR8","series-title":"International Series in Operations Research & Management Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-1-4615-5533-9_1","volume-title":"Project Scheduling","author":"W Herroelen","year":"1999","unstructured":"Herroelen, W., Demeulemeester, E., Reyck, B.: A classification scheme for project scheduling. In: Weglarz, J. (ed.) Project Scheduling. International Series in Operations Research & Management Science, vol. 14, pp. 1\u201326. Springer, New York (1999). doi: 10.1007\/978-1-4615-5533-9_1"},{"issue":"1","key":"5_CR9","doi-asserted-by":"crossref","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)","journal-title":"Eur. J. Oper. Res."},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"5_CR11","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1287\/mnsc.16.1.93","volume":"16","author":"AAB Pritsker","year":"1969","unstructured":"Pritsker, A.A.B., Waiters, L.J., Wolfe, P.M.: Multiproject scheduling with limited resources: a zero-one programming approach. Manag. Sci. 16, 93\u2013108 (1969)","journal-title":"Manag. Sci."},{"issue":"2","key":"5_CR12","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s00291-015-0419-6","volume":"38","author":"A Schnell","year":"2016","unstructured":"Schnell, A., Hartl, R.F.: On the efficient modeling and solution of the multi-mode resource-constrained project scheduling problem with generalized precedence relations. OR Spectr. 38(2), 283\u2013303 (2016)","journal-title":"OR Spectr."},{"key":"5_CR13","unstructured":"Schutt, A., Feydy, T., Stuckey, P.J., Wallace, M.G.: Solving the resource constrained project scheduling problem with generalized precedences by lazy clause generation. CoRR abs\/1009.0347 (2010). http:\/\/arxiv.org\/abs\/1009.0347"},{"key":"5_CR14","unstructured":"Schwindt, C.: Generation of resource constrained project scheduling problems subject to temporal constraints. Inst. f\u00fcr Wirtschaftstheorie und Operations-Research (1998)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-31365-3_38","volume-title":"Automated Reasoning","author":"R Sebastiani","year":"2012","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with $${\\cal{LA}}(\\mathbb{Q})$$ LA ( Q ) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 484\u2013498. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_38"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-319-44953-1_31","volume-title":"Principles and Practice of Constraint Programming","author":"R Szeredi","year":"2016","unstructured":"Szeredi, R., Schutt, A.: Modelling and solving multi-mode resource-constrained project scheduling. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 483\u2013492. Springer, Cham (2016). doi: 10.1007\/978-3-319-44953-1_31"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/978-3-319-18008-3_30","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"P Vil\u00edm","year":"2015","unstructured":"Vil\u00edm, P., Laborie, P., Shaw, P.: Failure-directed search for constraint-based scheduling. In: Michel, L. (ed.) CPAIOR 2015. LNCS, vol. 9075, pp. 437\u2013453. Springer, Cham (2015). doi: 10.1007\/978-3-319-18008-3_30"}],"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-66158-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,15]],"date-time":"2020-10-15T23:53:40Z","timestamp":1602806020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66158-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661575","9783319661582"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66158-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}