Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationPRICAI 2019
Subtitle of host publicationTrends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Proceedings
EditorsAbhaya C. Nayak, Alok Sharma
PublisherSpringer Verlag
Pages618-631
Number of pages14
ISBN (Print)9783030299071
DOIs
Publication statusPublished - Jan 1 2019
Event16th Pacific Rim International Conference on Artificial Intelligence, PRICAI 2019 - Yanuka Island, Fiji
Duration: Aug 26 2019Aug 30 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11670 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th Pacific Rim International Conference on Artificial Intelligence, PRICAI 2019
CountryFiji
CityYanuka Island
Period8/26/198/30/19

Fingerprint

Optimal Scheduling
Real time systems
Scheduling
Real-time
Deadline
Formulation
Dilemma
Satisfiability Problem
Overload
Workload
Scheduling Problem
Modulo
Timing
Exceed
First-order
Requirements
Experimental Results

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Liao, X., Zhang, H., Koshimura, M., Huang, R., & Yu, W. (2019). Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems. In A. C. Nayak, & A. Sharma (Eds.), PRICAI 2019: Trends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Proceedings (pp. 618-631). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11670 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-030-29908-8_49

Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems. / Liao, Xiaojuan; Zhang, Hui; Koshimura, Miyuki; Huang, Rong; Yu, Wenxin.

PRICAI 2019: Trends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Proceedings. ed. / Abhaya C. Nayak; Alok Sharma. Springer Verlag, 2019. p. 618-631 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11670 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Liao, X, Zhang, H, Koshimura, M, Huang, R & Yu, W 2019, Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems. in AC Nayak & A Sharma (eds), PRICAI 2019: Trends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11670 LNAI, Springer Verlag, pp. 618-631, 16th Pacific Rim International Conference on Artificial Intelligence, PRICAI 2019, Yanuka Island, Fiji, 8/26/19. https://doi.org/10.1007/978-3-030-29908-8_49
Liao X, Zhang H, Koshimura M, Huang R, Yu W. Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems. In Nayak AC, Sharma A, editors, PRICAI 2019: Trends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Proceedings. Springer Verlag. 2019. p. 618-631. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-29908-8_49
Liao, Xiaojuan ; Zhang, Hui ; Koshimura, Miyuki ; Huang, Rong ; Yu, Wenxin. / Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems. PRICAI 2019: Trends in Artificial Intelligence - 16th Pacific Rim International Conference on Artificial Intelligence, Proceedings. editor / Abhaya C. Nayak ; Alok Sharma. Springer Verlag, 2019. pp. 618-631 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{e86cb551c1c248a59970dde18b6f7723,
title = "Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems",
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.",
author = "Xiaojuan Liao and Hui Zhang and Miyuki Koshimura and Rong Huang and Wenxin Yu",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-29908-8_49",
language = "English",
isbn = "9783030299071",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "618--631",
editor = "Nayak, {Abhaya C.} and Alok Sharma",
booktitle = "PRICAI 2019",
address = "Germany",

}

TY - GEN

T1 - Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems

AU - Liao, Xiaojuan

AU - Zhang, Hui

AU - Koshimura, Miyuki

AU - Huang, Rong

AU - Yu, Wenxin

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85072862482&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85072862482&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-29908-8_49

DO - 10.1007/978-3-030-29908-8_49

M3 - Conference contribution

AN - SCOPUS:85072862482

SN - 9783030299071

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 618

EP - 631

BT - PRICAI 2019

A2 - Nayak, Abhaya C.

A2 - Sharma, Alok

PB - Springer Verlag

ER -