{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,21]],"date-time":"2025-04-21T19:23:12Z","timestamp":1745263392814,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030299071"},{"type":"electronic","value":"9783030299088"}],"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-29908-8_49","type":"book-chapter","created":{"date-parts":[[2019,8,23]],"date-time":"2019-08-23T01:03:32Z","timestamp":1566522212000},"page":"618-631","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems"],"prefix":"10.1007","author":[{"given":"Xiaojuan","family":"Liao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miyuki","family":"Koshimura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rong","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenxin","family":"Yu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,8,23]]},"reference":[{"key":"49_CR1","unstructured":"Abeni, L., Buttazzo, G., Superiore, S., Anna, S.: Integrating multimedia applications in hard real-time systems. In: IEEE Real-time Systems Symposium (1998)"},{"issue":"2","key":"49_CR2","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1109\/TASE.2014.2368997","volume":"12","author":"CE Aguero","year":"2015","unstructured":"Aguero, C.E., et al.: Inside the virtual robotics challenge: simulating real-time robotic disaster response. IEEE Trans. Autom. Sci. Eng. 12(2), 494\u2013506 (2015)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"4","key":"49_CR3","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s11633-012-0664-y","volume":"9","author":"A Gorbenko","year":"2012","unstructured":"Gorbenko, A., Popov, V.: Task-resource scheduling problem. Int. J. Autom. Comput. 9(4), 429\u2013441 (2012)","journal-title":"Int. J. Autom. Comput."},{"issue":"4","key":"49_CR4","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0167-6377(98)00045-5","volume":"24","author":"P Baptiste","year":"1999","unstructured":"Baptiste, P.: An O (n4) algorithm for preemptive scheduling of a single machine to minimize the number of late jobs. Oper. Res. Lett. 24(4), 175\u2013180 (1999)","journal-title":"Oper. Res. Lett."},{"issue":"9","key":"49_CR5","doi-asserted-by":"publisher","first-page":"1034","DOI":"10.1109\/12.620484","volume":"46","author":"S Baruah","year":"1997","unstructured":"Baruah, S., Haritsa, J.: Scheduling for overload in real-time systems. IEEE Trans. Comput. 46(9), 1034\u20131039 (1997)","journal-title":"IEEE Trans. Comput."},{"key":"49_CR6","doi-asserted-by":"crossref","unstructured":"Baulier, G.D., et al.: Real-time event processing system for telecommunications and other applications (2002)","DOI":"10.1002\/bltj.2089"},{"key":"49_CR7","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Zhang, H., Tan, Y., Lim, A.O.: DPSC: a novel scheduling strategy for overloaded real-time systems. In: IEEE International Conference on Computational Science and Engineering, pp. 1017\u20131023 (2014)","DOI":"10.1109\/CSE.2014.202"},{"key":"49_CR8","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Zhang, H., Tan, Y., Lim, A.O.: Greedy scheduling with feedback control for overloaded real-time systems. In: IFIP\/IEEE International Symposium on Integrated Network Management, pp. 934\u2013937 (2015)","DOI":"10.1109\/INM.2015.7140413"},{"key":"49_CR9","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Zhang, H., Tan, Y., Lim, Y.: Scheduling overload for real-time systems using SMT solver. In: IEEE\/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel\/distributed Computing, pp. 189\u2013194 (2016)","DOI":"10.1109\/SNPD.2016.7515899"},{"issue":"5","key":"49_CR10","doi-asserted-by":"publisher","first-page":"1055","DOI":"10.1587\/transinf.2016EDP7374","volume":"E100\u2013D","author":"Z Cheng","year":"2017","unstructured":"Cheng, Z., Zhang, H.: SMT-based scheduling for overloaded real-time systems. IEICE Trans. Inf. Syst. E100\u2013D(5), 1055\u20131066 (2017)","journal-title":"IEICE Trans. Inf. Syst."},{"key":"49_CR11","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Zhang, H., Tan, Y., Lim, Y.: SMT-based scheduling for multiprocessor real-time systems. In: IEEE\/ACIS International Conference on Computer and Information Science, pp. 1\u20137 (2016)","DOI":"10.1109\/ICIS.2016.7550822"},{"key":"49_CR12","unstructured":"Crawford, J.M., Baker, A.B.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: Twelfth AAAI National Conference on Artificial Intelligence, pp. 1092\u20131097 (1994)"},{"key":"49_CR13","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 de Moura","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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"49_CR14","unstructured":"Er, S.B., Smith, R.E.: Method and apparatus for monitoring and displaying lead impedance in real-time for an implantable medical device (1999)"},{"issue":"1","key":"49_CR15","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/S0167-5060(08)70356-X","volume":"5","author":"RL Graham","year":"1979","unstructured":"Graham, R.L., Lawler, E.L., Lenstra, J.K., Kan, A.H.G.R.: Optimization and approximation in deterministic sequencing and scheduling: a survey. Ann. Discret. Math. 5(1), 287\u2013326 (1979)","journal-title":"Ann. Discret. Math."},{"key":"49_CR16","doi-asserted-by":"crossref","unstructured":"Haritsa, J., Carey, M., Livny, M.: On being optimistic about real-time constraints. In: ACM Principles of Database Systems Symposium, pp. 331\u2013343. ACM (1990)","DOI":"10.1145\/298514.298585"},{"key":"49_CR17","doi-asserted-by":"crossref","unstructured":"Khalilzad, N.M., Nolte, T., Behnam, M.: Towards adaptive hierarchical scheduling of overloaded real-time systems. In: IEEE International Symposium on Industrial Embedded Systems, pp. 39\u201342 (2011)","DOI":"10.1109\/ETFA.2011.6059019"},{"issue":"8","key":"49_CR18","doi-asserted-by":"publisher","first-page":"2316","DOI":"10.1587\/transinf.E93.D.2316","volume":"E93\u2013D","author":"M Koshimura","year":"2010","unstructured":"Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Solving open job-shop scheduling problems by SAT encoding. IEICE Trans. Inf. Syst. E93\u2013D(8), 2316\u20132318 (2010)","journal-title":"IEICE Trans. Inf. Syst."},{"key":"49_CR19","first-page":"95","volume":"8","author":"M Koshimura","year":"2012","unstructured":"Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. J. Satisf. Boolean Model. Comput. 8, 95\u2013100 (2012)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"3","key":"49_CR20","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1145\/785411.785416","volume":"8","author":"K Kuchcinski","year":"2003","unstructured":"Kuchcinski, K.: Constraints-driven scheduling and resource assignment. ACM Trans. Des. Autom. Electron. Syst. 8(3), 355\u2013383 (2003)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"49_CR21","doi-asserted-by":"crossref","unstructured":"Kumar, P., Chokshi, D.B., Thiele, L.: A satisfiability approach to speed assignment for distributed real-time systems. In: Design, Automation and Test in Europe Conference and Exhibition, pp. 749\u2013754 (2013)","DOI":"10.7873\/DATE.2013.160"},{"issue":"1","key":"49_CR22","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF02248588","volume":"26","author":"EL Lawler","year":"1990","unstructured":"Lawler, E.L.: A dynamic programming algorithm for preemptive scheduling of a single machine to minimize the number of late jobs. Ann. Oper. Res. 26(1), 125\u2013133 (1990)","journal-title":"Ann. Oper. Res."},{"key":"49_CR23","doi-asserted-by":"crossref","unstructured":"Leung, J.Y.T.: Online scheduling. In: Handbook of Scheduling, pp. 328\u2013371. Chapman and Hall\/CRC (2004)","DOI":"10.1201\/9780203489802"},{"issue":"8","key":"49_CR24","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/TPDS.2010.204","volume":"22","author":"W Liu","year":"2011","unstructured":"Liu, W., Gu, Z., Xu, J., Wu, X., Ye, Y.: Satisfiability modulo graph theory for task mapping and scheduling on multiprocessor systems. IEEE Trans. Parallel Distrib. Syst. 22(8), 1382\u20131389 (2011)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"49_CR25","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.cor.2017.08.012","volume":"89","author":"A Malik","year":"2018","unstructured":"Malik, A., Walker, C., O\u2019Sullivan, M., Sinnen, O.: Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay. Comput. Oper. Res. 89, 113\u2013126 (2018)","journal-title":"Comput. Oper. Res."},{"key":"49_CR26","doi-asserted-by":"crossref","unstructured":"Marchand, M., Chetto, M.: Dynamic scheduling of periodic skippable tasks in an overloaded real-time system. In: IEEE\/ACS International Conference on Computer Systems and Applications, pp. 456\u2013464. IEEE (2008)","DOI":"10.1109\/AICCSA.2008.4493573"},{"key":"49_CR27","doi-asserted-by":"crossref","unstructured":"Metzner, A., Herde, C.: RTSAT- an optimal and efficient approach to the task allocation problem in distributed architectures. In: IEEE International Real-Time Systems Symposium, pp. 147\u2013158 (2006)","DOI":"10.1109\/IPDPS.2006.1639420"},{"key":"49_CR28","unstructured":"Microsoft, R.: Z3-optimization (2018). https:\/\/www.rise4fun.com\/Z3\/tutorial\/optimization"},{"issue":"1","key":"49_CR29","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1287\/mnsc.15.1.102","volume":"15","author":"JM Moore","year":"1968","unstructured":"Moore, J.M.: An n job, one machine sequencing algorithm for minimizing the number of late jobs. Manag. Sci. 15(1), 102\u2013109 (1968)","journal-title":"Manag. Sci."},{"key":"49_CR30","doi-asserted-by":"crossref","unstructured":"Tres, C., Becker, L.B., Nett, E.: Real-time tasks scheduling with value control to predict timing faults during overload. In: IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing, pp. 354\u2013358 (2007)","DOI":"10.1109\/ISORC.2007.52"},{"issue":"6","key":"49_CR31","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1016\/j.orl.2009.09.003","volume":"37","author":"N Vakhania","year":"2009","unstructured":"Vakhania, N.: Scheduling jobs with release times preemptively on a single machine to minimize the number of late jobs. Oper. Res. Lett. 37(6), 405\u2013410 (2009)","journal-title":"Oper. Res. Lett."},{"issue":"1","key":"49_CR32","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1109\/TPDS.2014.2308175","volume":"26","author":"S Venugopalan","year":"2014","unstructured":"Venugopalan, S., Sinnen, O.: ILP formulations for optimal task scheduling with communication delays on parallel systems. IEEE Trans. Parallel Distrib. Syst. 26(1), 142\u2013151 (2014)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"5","key":"49_CR33","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.apenergy.2015.01.010","volume":"144","author":"DP Xenos","year":"2015","unstructured":"Xenos, D.P., Cicciotti, M., Kopanos, G.M., Bouaswaig, A.E.F., Kahrs, O., Martinez-Botas, R., Thornhill, N.F.: Optimization of a network of compressors in parallel: real time optimization (RTO) of compressors in chemical plants - an industrial case study. Appl. Energy 144(5), 51\u201363 (2015)","journal-title":"Appl. Energy"}],"container-title":["Lecture Notes in Computer Science","PRICAI 2019: Trends in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29908-8_49","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T15:25:38Z","timestamp":1709825138000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29908-8_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030299071","9783030299088"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29908-8_49","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 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PRICAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pacific Rim International Conference on Artificial Intelligence","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cuvu, Yanuka Island","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Fiji","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":"26 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"pricai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.pricai.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}