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

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Maximum satisfiability formulation for optimal scheduling in overloaded real-time systems'. Together they form a unique fingerprint.

Cite this