Modeling and Solving Scheduling in Overloaded Situations with Weighted Partial MaxSAT

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

研究成果: ジャーナルへの寄稿学術誌査読

3 被引用数 (Scopus)


In real-time systems, where tasks have timing requirements, once the workload exceeds the system's capacity, missed due dates may cause system overload. In this situation, finding an optimal scheduling that minimizes the cumulative values of late tasks is critical in both theory and practice. Recently, formalizing scheduling problems as a class of generalized problems, such as Satisfiability Modulo Theory (SMT) and Maximum Satisfiability (MaxSAT), has been receiving immense concern. Enlightened by the high efficiency of these satisfiability-based methods, this paper formulates the single-machine scheduling problem of minimizing the total weight of late tasks as a Weighted Partial Maximum (WPM) Satisfiability problem. In the formulation, scheduling features are encoded as rigidly enforced hard clauses and the scheduling objective is treated as a set of weighted soft ones. Then an off-the-shelf WPM solver is exploited to maximize the total weight of the satisfied soft clauses, provided that all the hard clauses are satisfied. Experimental results demonstrate that, compared with the existing satisfiability-based methods, the proposed method significantly improves the efficiency of identifying the optimal schedule. Moreover, we make minor changes to apply the WPM formulation to parallel-machine scheduling, showing that the proposed method is sufficiently flexible and well scalable.

ジャーナルMathematical Problems in Engineering
出版ステータス出版済み - 2021

!!!All Science Journal Classification (ASJC) codes

  • 数学一般
  • 工学一般


「Modeling and Solving Scheduling in Overloaded Situations with Weighted Partial MaxSAT」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。