Skip to main content
Register
Springer Professional
SEARCH
Menu 1 2 3 4
Top

Hint

Swipe to navigate through the chapters of this book

Published in:
Explaining Black-Box Models Using Interpretable Surrogates Read chapter Read first chapter

2019 | OriginalPaper | Chapter

Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems

Authors : Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu

Published in: PRICAI 2019: Trends in Artificial Intelligence

Publisher: Springer International Publishing

Login to get access
share
SHARE

Abstract

In real-time systems where tasks have timing requirements, once the workload exceeds the system’s capacity, missed deadlines may incur system overload. Finding optimal scheduling in overloaded real-time systems is critical in both theory and practice. To this end, existing works have encoded scheduling problems as a set of first-order formulas that might be tackled by the Satisfiability Modulo Theory (SMT) solver. In this paper, we move one step forward by formulating the scheduling dilemma in overloaded real-time systems as a Maximum Satisfiability (MaxSAT) problem. In the MaxSAT formulation, scheduling features are encoded as hard constraints and the task deadlines are considered soft ones. An off-the-shelf MaxSAT solver is employed to satisfy as many deadlines as possible, provided that all the hard constraints are met. Our experimental results show that our proposed MaxSAT-based method found optimal scheduling significantly more efficiently than previous works.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now
previous chapter A Strategy-Proof Model-Based Online Auction for Ad Reservation
next chapter A Cognitive Model of Human Bias in Matching
Footnotes
1
Note that an off-line algorithm does not contradict with a real-time system. An off-line scheduling allows a scheduler to make decision based on the total knowledge of the problem, while a real-time system assigns each task with a specific deadline.
 
Literature
1.
Abeni, L., Buttazzo, G., Superiore, S., Anna, S.: Integrating multimedia applications in hard real-time systems. In: IEEE Real-time Systems Symposium (1998)
2.
Aguero, C.E., et al.: Inside the virtual robotics challenge: simulating real-time robotic disaster response. IEEE Trans. Autom. Sci. Eng. 12(2), 494–506 (2015) CrossRef
3.
Gorbenko, A., Popov, V.: Task-resource scheduling problem. Int. J. Autom. Comput. 9(4), 429–441 (2012) CrossRef
4.
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–180 (1999) MathSciNetMATHCrossRef
5.
Baruah, S., Haritsa, J.: Scheduling for overload in real-time systems. IEEE Trans. Comput. 46(9), 1034–1039 (1997) MathSciNetCrossRef
6.
Baulier, G.D., et al.: Real-time event processing system for telecommunications and other applications (2002)
7.
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–1023 (2014)
8.
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–937 (2015)
9.
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–194 (2016)
10.
Cheng, Z., Zhang, H.: SMT-based scheduling for overloaded real-time systems. IEICE Trans. Inf. Syst. E100–D(5), 1055–1066 (2017) CrossRef
11.
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–7 (2016)
12.
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–1097 (1994)
13.
14.
Er, S.B., Smith, R.E.: Method and apparatus for monitoring and displaying lead impedance in real-time for an implantable medical device (1999)
15.
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–326 (1979) MathSciNetMATHCrossRef
16.
Haritsa, J., Carey, M., Livny, M.: On being optimistic about real-time constraints. In: ACM Principles of Database Systems Symposium, pp. 331–343. ACM (1990)
17.
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–42 (2011)
18.
Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Solving open job-shop scheduling problems by SAT encoding. IEICE Trans. Inf. Syst. E93–D(8), 2316–2318 (2010) CrossRef
19.
Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. J. Satisf. Boolean Model. Comput. 8, 95–100 (2012) MathSciNetMATH
20.
Kuchcinski, K.: Constraints-driven scheduling and resource assignment. ACM Trans. Des. Autom. Electron. Syst. 8(3), 355–383 (2003) CrossRef
21.
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–754 (2013)
22.
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–133 (1990) MathSciNetMATHCrossRef
23.
Leung, J.Y.T.: Online scheduling. In: Handbook of Scheduling, pp. 328–371. Chapman and Hall/CRC (2004)
24.
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–1389 (2011) CrossRef
25.
Malik, A., Walker, C., O’Sullivan, M., Sinnen, O.: Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay. Comput. Oper. Res. 89, 113–126 (2018) MathSciNetMATHCrossRef
26.
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–464. IEEE (2008)
27.
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–158 (2006)
28.
29.
Moore, J.M.: An n job, one machine sequencing algorithm for minimizing the number of late jobs. Manag. Sci. 15(1), 102–109 (1968) MATHCrossRef
30.
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–358 (2007)
31.
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–410 (2009) MathSciNetMATHCrossRef
32.
Venugopalan, S., Sinnen, O.: ILP formulations for optimal task scheduling with communication delays on parallel systems. IEEE Trans. Parallel Distrib. Syst. 26(1), 142–151 (2014) CrossRef
33.
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–63 (2015) CrossRef
Metadata
Title
Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems
Authors
Xiaojuan Liao
Hui Zhang
Miyuki Koshimura
Rong Huang
Wenxin Yu
Copyright Year
2019
Book
PRICAI 2019: Trends in Artificial Intelligence

Print ISBN: 978-3-030-29907-1

Electronic ISBN: 978-3-030-29908-8

Copyright Year: 2019

DOI
https://doi.org/10.1007/978-3-030-29908-8_49

Premium Partner

Neuer Inhalt
    Image Credits