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
N1 - Funding Information:
Supported by National Natural Science Foundation of China (Grant Number 61806171), JSPS KAKENHI (Grant Numbers JP17K00307, JP19H04175), Ministry of Education in China Project of Humanities and Social Sciences (Grant Number 17YJCZH260). We thank Dr. Zhuo Cheng for his constructive advice. c○ Springer Nature Switzerland AG 2019
Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019
Y1 - 2019
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
T2 - 16th Pacific Rim International Conference on Artificial Intelligence, PRICAI 2019
Y2 - 26 August 2019 through 30 August 2019
ER -