# Modeling and Solving Scheduling in Overloaded Situations with Weighted Partial MaxSAT

Authors: Xiaojuan Liao; Hui Zhang; Miyuki Koshimura; Rong Huang; Wenxin Yu; Fagen Li
Journal: Mathematical Problems in Engineering
 (2021)

---

## Abstract

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.


---

## Body

## 1. Introduction

Real-time systems, which are designed to handle tasks with completion due dates, play an important role in a variety of modern applications, such as robotics [1], pacemakers [2], chemical plants [3], telecommunications [4], and multimedia systems [5]. Under ideal circumstances, a real-time system completes all tasks before their due dates expire. However, in reality, the workload may exceed the system’s capacity, leading to missed deadlines [6]. Such a phenomenon is called overload. A classic example is a switch in a communication network which polls its incoming links to forward packets that have arrived since its previous servicing of the link [7]. On each link, different packets may have different processing times, deadlines, and importance values. When packages flood the switch, overload happens. In this situation, designing a suitable scheduling strategy to maximize the total value of forwarded packages is critical to maintain a service’s stability.Generally, scheduling algorithms can be classified as online scheduling and offline scheduling, depending on whether tasks’ information is known a priori. In online scheduling, the scheduler receives tasks that arrive over time and must schedule tasks without any knowledge of the future. On the contrary, offline scheduling algorithms aim at solving the problem optimally, provided that all data are known beforehand1(note that an offline algorithm does not contradict with a real-time system. An offline scheduling algorithm 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 due date). Although online scheduling is more flexible, in many situations, it is necessary to obtain optimal schedules by offline algorithms, especially in time-critical systems or for the evaluation of heuristics [8]. In this paper, we take an interest in designing an offline scheduling method on a single machine to minimize the total weight of tasks that miss their due dates.To date, there has been an immense amount of work devoted to characterizing scheduling problems and analyzing the complexity of problems with specific characteristics. When preemption is prohibited, Michael Moore [9] presented an optimal algorithm in polynomial time to minimize the number of late tasks on a single machine, under the assumption that all tasks are released simultaneously without dependency relations. In the standard three-field notation [10], this problem is 1‖∑Uj. Adding weights on the criteria and setting precedence constraints may complicate the problem. Richard [11] showed that 1‖∑wjUj is binary NP-hard but can be solved by dynamic programming in On∑pj time [12], where n is the number of tasks and pj is the processing time of task τj. Garey and Johnson [13] showed that the problem of unit-time tasks subject to precedence constraints, that is, 1prec,pj=1∑Uj, is NP-hard. Furthermore, Lenstra and Rinnooy Kan [14] proved that, even for chain-like precedence constraints, where each task has at most one immediate predecessor and at most one immediate successor, the problem 1chains,pj=1∑Uj is also NP-hard. Another prevailing common knowledge is that usually preemptive problems are not harder than their nonpreemptive counterparts. For example, the problem with release dates 1rj∑Uj is NP-hard [10], while the preemptive version 1rj,pmtn∑Uj can be solved in On3k2 [15], where k is the number of distinct release dates. Further complexity results for single-machine scheduling problems are listed by [16] and the scheduling problems with the late work criteria are surveyed by [17].Algorithms for solving scheduling are generally classified as online scheduling and offline scheduling, depending on whether the full information about tasks is known a priori or not. Online algorithms aim to return high-quality results within reasonable CPU time [18–21], whereas offline algorithms are devoted to optimally solving scheduling problems, given that all data are known beforehand. For large-scale problems that are computationally intractable, finding optimal solutions requires a significantly long computation time and heuristics are proposed to seek for suboptimal solutions within a short computation time [22–24]. Nevertheless, it is still of great significance to design optimization algorithms as a testbed for suboptimal solutions and reap huge benefit when the scheduled application is executed many times [8]. Previous attempts at finding optimal solutions to single-machine scheduling problems are mainly based on dynamic programming and branch-and-bound algorithms, with promising results. For a comprehensive survey, see the work by [25]. In the last decade, formalizing scheduling problems as a class of generalized problems, such as Mathematical Programming (MP) [26–31], Satisfiability Modulo Theory (SMT) [8, 32–34], Boolean Satisfiability (SAT) [35–37], and Partial Maximum (PM) Satisfiability [38], has received considerable attention. Motivated by the significant progress in solving these generalized problems, the formalized scheduling problem can be efficiently addressed with the corresponding solving algorithms.As a pioneering work in satisfiability formalization, Crawford and Baker [35] first encoded scheduling problems into a SAT problem, paving the way for subsequent work [36] that solved six types of open job-shop scheduling problems. Venugopalan and Oliver [27], Liu et al. [37], and Malik et al. [8] presented optimization frameworks to address task graph scheduling with communication costs based on MIP, SAT, and SMT, respectively. Qi et al. [34] utilized task duplication strategy-based SMT formulation to mitigate the negative impact of the interprocessor communication delay in the task graph scheduling problem. Qamhan et al. [31] presented a new MILP model to schedule a set of tasks on a single-machine subject to nonzero release date, sequence-dependent setup time, and periodic maintenance. The objective of all the above formulations is to minimize the maximum completion time makespan.To achieve the goal of minimizing the number of late jobs, Ourari et al. [26] designed a mathematical integer programming formulation for single-machine scheduling without preemption, and Hung et al. [29] developed a nonstandard MIP formulation to address the arbitrary preemptive version on parallel machines. The restricted preemptive counterpart on a single machine was solved by Cheng et al. [32], which encoded the problem as a set of first-order formulas that are tackled by an SMT solver called Z3. By running the Z3 solver repeatedly to identify the maximum number of on-time tasks, the optimal schedule could be finally determined. The SMT-based scheduling is sufficiently flexible because it handles various task properties and objectives with very few changes in adaption procedure. For example, when tasks have different importance values and the objective turns to minimizing the total weight of late tasks, only the target constraints need to be modified [33]. Later on, Wang et al. [39] enhanced Cheng’s SMT formulation by removing redundant constraints and eliminating successive calls of the Z3 solver. Experiments illustrated that the updated formulation improved the efficiency by more than two orders of magnitude. Recently, Liao et al. [38] encoded the unweighted version of the same scheduling problem into Boolean propositional logic and showed that PM solvers are a competitive alternative to SMT solvers. However, we notice that when encoding scheduling features, PM formulation generates redundant variables and clauses. Such redundancy may create extra calculations and decrease the overall performance. Furthermore, PM formulation presented in [38] is incapable of handling weighted problems where the scheduling goal is to minimize the total weight of late tasks.In this paper, we present a Weighted Partial MaxSAT (WPM) formulation to optimally solve scheduling in overloaded situations, with the aim of minimizing the total weight value of late tasks. The minimization objective is equivalent to maximizing the total weight of the tasks meeting their due dates. Confronted with a weighted scheduling problem, we first identify scheduling features that uniquely characterize the problem, facilitating the WPM formulation in the encoding phase. Then, enlightened by the WPM characteristics that satisfy all hard clauses and maximize the total weight of the satisfied soft clauses, we recast the weighted scheduling problem as a WPM problem. Finally, in the problem-solving phase, we exploit the off-the-shelf WPM solver to satisfy all the scheduling features and maximize the total weight of tasks meeting their due dates, thus deriving the optimal schedule from the output of the WPM solver. Specifically, we make the following contributions:(i)
We extend the PM formulation in [38], which was originally designed for scheduling tasks without weights, to adapt to the weighted cases.(ii)
Having noticed that redundant Boolean variables and clauses exist in the previous formulation [38], we develop a more compact encoding to characterize the scheduling problem. Particularly, to denote a task’s completion time, the number of Boolean variables generated by [38] is proportional to the number of possible preemptions of the task. In contrast, the novel compact encoding generates only one Boolean variable to represent the task’s completion time, no matter how many times the task may be preempted. Theoretical analysis shows the correctness of the compact encoding and experiments demonstrate the substantial advantages over the previous PM encoding [38] and SMT formulation [39], which was enhanced from [33].(iii)
In the WPM encoding, task features are encoded by several separate rules. This means if some of the task features happen to change, only partial rules need to be modified. To demonstrate the flexibility of our formulation, we extend the current WPM encoding to adapt to parallel-machine scheduling with little modification. We believe that the proposed WPM encoding can help users readily and effectively design scheduling for practical systems with low design cost.Confronted with a weighted scheduling problem, we first identify scheduling features that uniquely characterize the problem, facilitating the WPM formulation in the encoding phase. Then, enlightened by the WPM characteristics that satisfy all hard clauses and maximize the total weight of the satisfied soft clauses, we recast the weighted scheduling problem as a WPM problem. In the WPM formulation, tasks’ features are encoded as a set of hard clauses, and the goal of completing tasks before their due dates is transformed into a set of weighted soft clauses. Finally, in the problem-solving phase, we exploit the off-the-shelf WPM solver to satisfy all the scheduling features and maximize the total weight of tasks meeting their due dates, thus deriving the optimal schedule from the output of the WPM solver.To evaluate the performance of the proposed WPM formulation, we compare it with the state-of-the-art SMT formulation [39]. Our evaluation shows that WPM formulation has a dominant advantage over the SMT-based method in finding out the optimal schedule. We also compare WPM with the latest PM formulation [38] on a special case, where all the tasks have equal weights. We reveal redundancies in PM and discuss how they can be avoided in WPM. Experiments show that our WPM encoding is more compact and more time-efficient than PM for solving the same set of problem instances. Furthermore, we show that the presented approach is sufficiently flexible to adapt to parallel-machine scheduling problems with minor changes.The remainder of this paper is organized as follows. The scheduling model is described in Section2, followed by the WPM-based optimization framework in Sections 3. We make theoretical comparisons between WPM and PM formulation [38] in Section 4 and provide experimental results to show the superiority of WPM in Section 5. Section 6 exhibits how to extend the WPM formulation of single-machine scheduling to parallel-machine scheduling. Finally, we conclude this paper in Section 7.


## 2. Scheduling Model

We adhere to the definition of scheduling problems in previous works [33, 39]. For convenience, the notations used in the model are summarized in Table 1.Table 1
Notations and descriptions in scheduling model.
NotationDescriptionΓFinite set of real-time tasksnNumber of real-time tasks.n=ΓτℓTask inΓ, where ℓ is its indexrℓRelease date ofτℓcℓExecution time ofτℓdℓDue date ofτℓfiℓith fragment of τℓqℓNumber of fragments inτℓciℓExecution time offiℓτk≺τℓτℓ succeeds τkRdpSet of task pairs that have dependency relationsThe problem involvesn tasks Γ=τ1,…,τn to be processed. All the tasks request a uniprocessor for execution when they arrive in the system. Each task τℓ∈Γ is represented by a 4-tuple τℓ=rℓ,cℓ,dℓ,wℓ, where rℓ, cℓ, dℓ, and wℓ are all nonnegative integers 2(assuming all parameters to be integers does not make the problem less general since real numbers can be scaled to integers with a few orders of magnitude) representing the release date, the execution time, the due date, and the weight of τℓ, respectively. Naturally, rℓ+cℓ≤dℓ. Weight wℓ reflects the importance of task τℓ. The larger wℓ is, the more important τℓ is. Given due date dℓ, if task τℓ is completed at or before dℓ, τℓ is on time and weight wℓ is obtained by the system. Otherwise, τℓ is late and worthless to the system.To allow preemption, which indicates that a running task may be interrupted and resumed later, each taskτℓ∈Γ is split into qℓ nonpreemptive subtasks (fragments) and is defined as a chain of indivisible fragments f1ℓ,…,fqℓℓ. Symbol ciℓ stands for the required execution time of fiℓ. Clearly, ∑i=1qℓciℓ=cℓ. For 2≤i≤qℓ, fiℓ can only start to run after fi−1ℓ is completed.In practical systems, tasks usually have dependency relations. For example, if taskτℓ requires the computed result of τk, τℓ cannot start until τk is finished. Such a dependency relation between tasks is written as τk≺τℓ, where τk is the immediate predecessor of τℓ, and τℓ is the immediate successor of τk. Obviously, if τk≺τℓ, the constraint rk+ck≤dℓ−cℓ should be satisfied; otherwise, τℓ can never be completed no matter when its predecessor finishes. The set of task pairs that have dependency relations over Γ is denoted by Rdp=τk,τℓ:τk,τℓ∈Γ,τk≺τℓ.A system is defined as overloaded if no scheduling algorithm can meet the due dates of all the tasks that have been submitted to it. This paper focuses on designing an exact method to tackle overloaded single-machine scheduling problems. The scheduling objective is to maximize the total weight of the on-time tasks. In particular, if all tasks have equal weights, then a schedule that maximizes the total weight will be one that maximizes the number of on-time tasks.


## 3. WPM-Based Optimization Framework

In this section, we provide the WPM formulation for solving the task scheduling problem on a single machine. The overview of the WPM formulation is illustrated in Figure1.Figure 1
Overview of the WPM-based scheduling method.Feature preprocessing identifies the scheduling problem with two types of constraints, that is, constraints on scheduling features and those on objective. Given a set of tasksΓ=τ1,…,τn, scheduling features uniquely characterize the problem over Γ and the objective is to seek for a schedule that completes all tasks on time subject to constraints on the scheduling features. In overloaded situations, making all the tasks complete by their due dates is impossible, and the scheduling problem is then treated as an optimization problem, which aims to maximize the total weight of tasks that are completed by their due dates. After feature preprocessing, WPM encoding can be implemented separately on the scheduling features and objective. Specifically, scheduling features, which are intrinsic and determined when tasks are released, are encoded into a set of hard clauses that should be satisfied without exception. On the other hand, the objective in overloaded situations is encoded as a set of weighted soft clauses that are allowed to be unsatisfied. By conjunction of hard clauses with weighted soft clauses, the problem turns to a WPM problem that can be addressed by any off-the-shelf WPM solver. In the problem-solving phase, a WPM solver tries to satisfy all the hard clauses and maximize the total weight of satisfied soft clauses. The output of the WPM solver includes the assignment of all Boolean variables, from which the optimal schedule can be derived.Section3.1 shows how to identify fragments’ critical time points to characterize the scheduling problem, paving the way for the WPM encoding described in Sections 3.2. Section 3.3 exhibits an example to show how the scheduling problem is addressed with the presented WPM encoding. Details on the problem-solving phase are also exhibited in Section 3.3.


### 3.1. Feature Preprocessing

Given a task setΓ=τ1,…,τn, where each task τℓ∈Γ is characterized by rℓ,cℓ,dℓ,wℓ, ∀τℓ∈Γ, τℓ cannot start before its release date rℓ. Thus, the possible Earliest Start Time (EST) of τℓ, denoted by ESTℓ, is equal to its release date rℓ, and the Earliest Completion Time (ECT) of τℓ, denoted by ECTℓ, is ESTi+ci. ∀τk,τℓ∈Rdp, ESTℓ is jointly restricted by rℓ and ECTk. Specifically, if ECTk≤rℓ, then ESTℓ=rℓ; otherwise, ESTℓ=ECTk, suggesting that τℓ should wait until τk is finished. Typically, let Pℓ be the set of predecessors of τℓ; then ESTℓ=maxrℓ,maxτk∈PℓECTk.AfterESTℓ for each τℓ in Γ has been determined, EST and ECT of each fragment in τℓ can be calculated as follows:(i)
Earliest Start Time (EST) offiℓ is denoted by ESTiℓ, where ESTiℓ=ESTℓ+∑u=1i−1cuℓ. ∀τℓ∈Γ and ∀fiℓ∈τℓ, fiℓ should start at or after ESTiℓ, indicating that fiℓ cannot be started before all its previous fragments are finished. Typically, EST1ℓ=ESTℓ.(ii)
Earliest Completion Time (ECT) offiℓ is denoted by ECTiℓ, where ECTiℓ=ESTℓ+∑u=1icuℓ. No fragment fiℓ can be completed before ECTiℓ. Particularly, ECTiℓ=ESTiℓ+ciℓ.In addition to EST and ECT,∀τℓ∈Γ, each fragment fiℓ∈τℓ is characterized by the two following types of time:(i)
Latest Start Time (LST) offiℓ is denoted by LSTiℓ, where LSTiℓ=dℓ−∑u=iqℓcuℓ. If fiℓ fails to start before LSTiℓ, τℓ cannot end by its due date dℓ, and thus this task becomes worthless to the system.(ii)
Latest Completion Time (LCT) offiℓ is denoted by LCTiℓ, where LCTiℓ=dℓ−∑u=i+1qℓcuℓ. Particularly, LCTiℓ=LSTiℓ+ciℓ.Note that, in the above four critical time points, ECT is unrelated to our WPM encoding. Nevertheless, it is indispensable in the previous work [38], which will be discussed in Section 4..


### 3.2. WPM Formulation

This section introduces how to encode the scheduling problem as a WPM problem. A WPM instance consists of a number of clauses that need to be managed by the WPM solver. To formulate all the necessary constraints that characterize the scheduling model, we introduce the three following Boolean variables:(i)
sai,tℓ, which is true if fiℓ starts at time t or later(ii)
pri,jℓ,k, which is true if fiℓ precedes fjk(iii)
ebℓ, which is true if τℓ ends by its due date dℓBased on the generated Boolean variables, the WPM encoding can be implemented. In what follows, several rules are presented to encode the features of fragments into a set of hard clauses. The main encoding is derived and enhanced from previous work [35, 36, 38]. Logical implication a⟶b is equivalent to ¬a∨b in classical logic.(i)
(C1)∀τℓ∈Γ, the first fragment of τℓ, that is, f1ℓ, starts at or after EST1ℓ:(1)sa1,EST1ℓℓ.(ii)
(C2)∀τℓ∈Γ and ∀fiℓ,fi+1ℓ∈τℓ, fiℓ precedes fi+1ℓ:(2)pri,i+1ℓ,ℓ.(iii)
(C3)∀τk,τℓ∈Γ, ∀fik∈τk, and ∀fjℓ∈τℓ, if k≠l, τk≺τℓ, τℓ≺τk, ESTik<LCTjℓ and ESTjℓ<LCTik, and then fik and fjℓ may require the processor at the same time. In this condition, fik precedes fjℓ or fjℓ precedes fik:(3)pri,jk,ℓ∨prj,iℓ,k.(iv)
(C4)∀τk,τℓ∈Rdp, if τk fails to be completed by its due date, then τℓ cannot even start at LST1ℓ:(4)¬ebk⟶sa1,LST1ℓ+1ℓ.(v)
Furthermore, ifdk>EST1ℓ, the first fragment of τℓ cannot start until the last fragment of τk finishes. That is, if dk>EST1ℓ, then the constraint that fqkk precedes f1ℓ is enforced:(5)prqk,1k,ℓ.(vi)
(C5)∀τℓ∈Γ and ∀fiℓ∈τℓ, if fiℓ starts at or after time t, then it starts at or after time t−1:(6)sai,tℓ⟶sai,t−1ℓ,ESTiℓ+1≤t≤LSTiℓ+1.(vii)
(C6)∀τℓ∈Γ, if τℓ ends before its due date dℓ, then last fragment fqℓℓ must start at or before time LSTqℓℓ. In other words, fqℓℓ cannot start at or after time LSTqℓℓ+1:(7)ebℓ⟶¬saqℓ,LSTqℓℓ+1ℓ.(viii)
(C7)∀τk,τℓ∈Γ, ∀fik∈τk, and ∀fjℓ∈τℓ, if fik starts at or after time t and fjℓ follows fik, then fjℓ cannot start until fik is finished. That is, for each pri,jk,ℓ asserted by (C2)∼(C4), one clause is generated:(8)sai,tk∧pri,jk,ℓ⟶saj,t′ℓ,wheret varies in ESTik,LSTik+1 and(9)t′=LSTjℓ+1,ift+cik>LSTjℓ,ESTjℓ,ift+cik<ESTjℓ,t+cik,Otherwise.This formula reveals the following facts: First, iffik ends after LSTjℓ (i.e., t+cik>LSTjℓ), then fjℓ cannot start at or before LSTjℓ. Second, if fik finishes before ESTjℓ (i.e., t+cik<ESTjℓ), then fjℓ starts at or after ESTjℓ. Otherwise, fjℓ must start at or after time fik finishes, that is, t+cik.Up to this point, we have encoded the scheduling features as Boolean formulas that can be converted to a set of clauses. Since the scheduling features are intrinsic properties inherent in the tasks and their fragments, such clauses are specified as hard, indicating that all of them must absolutely be satisfied. For convenience, we refer to the set of hard clauses introduced in (C1)∼(C7) as C.A task is said to be on time if and only if it is completed before its due date. Thus, the scheduling objective can be directly encoded by the following rule:(O) Maximizing the sum of the weights of on-time tasks:(10)ebℓ,wℓ,1≤ℓ≤n.Equation (10) indicates that if clause ebℓ is satisfied (i.e., evaluating to true), then weight wℓ is gained; otherwise, the gain is zero. To simplify the discussion, we introduce O to denote the set of clauses in equation (10). In an overloaded system, not all tasks can be completed before their due dates. To handle such situations, we declare the clauses in O to be soft, indicating that completing all the tasks by their due dates is a soft constraint. Conjunct with C, the problem is then C,O. This leads to a WPM problem, which tries to find an assignment of variables to satisfy all the hard clauses in C and to maximize the sum of the weights of the satisfied soft clauses in O, that is, to maximize ∑ℓ=1nwℓ⋅ebℓ.


### 3.3. A Pedagogical Example

Let us consider a simple scheduling problem to describe how WPM formulation works. As shown in Figure2(a), there are a set of real-time tasks Γ=τ1,τ2,τ3, where both τ1 and τ3 rely on the computed result of τ2, represented as τ2≺τ1 and τ2≺τ3; that is, Rdp=τ2,τ1,τ2,τ3. The release dates, the execution times, the due dates, and the weights of these tasks are, respectively, defined as τ1=0,2,3,1, τ2=0,1,1,2, and τ3=0,1,2,3. Suppose that τ1 has two fragments, that is, f11,f21. τ2 and τ3 each have one, denoted by f12 and f13, respectively. The execution time of each fragment is 1.Figure 2
A simple scheduling example. (a) Original problem. (b) Problem after feature preprocessing.
(a)(b)The refined problem exhibition and the critical time points after feature preprocessing are summarized in Figure2(b) and Table 2, respectively. Since ECT has nothing to do with the WPM encoding, we omit this entry in Table 2 for conciseness.Table 2
Critical time points of each fragment in three tasks.
TaskFragmentESTLSTLCTτ1f11112f21223τ2f12001τ3f13112The MaxSAT formulation applied to the scheduling problem is shown in Figure3. Constraint (C1) states that each task starts at or after its EST. Constraints (C2) and (C3) work together to specify the execution sequence of the fragments. (C2) forces all the fragments in a single task to be executed sequentially, and (C3) guarantees no overlap of the execution times of any two fragments in different tasks. In the three tasks, only τ1 has more than one fragment, and hence constraint (C2) only applies to τ1, ensuring that f11 precedes f21. Constraint (C3) applies to pairs of fragments fik and fjℓk≠l satisfying ESTik<LCTjℓ and ESTjℓ<LCTik. If both conditions are met, then fik and fjℓ may simultaneously occupy the processor, and thus we need to decide in what order to execute them. Constraint (C3) tackles this ordering dilemma, which states that either one can precede the other. Consider f11 and f13. As seen in Table 2, EST11<LCT13 and EST13<LCT11; hence, we must explicitly specify that f11 precedes f13 or f13 precedes f11; otherwise, the execution time of these two fragments may overlap. Constraint (C4) applies to a situation where tasks have dependency relations. In the example, τ2 is the predecessor of both τ1 and τ3; thus we should give up processing τ1 and τ3 if τ2 misses its due date. In addition, given d2=EST11 and d2=EST13, there is no need to explicitly specify the execution sequence of the predecessor and successors since τ2 must have finished before τ1 and τ3 start. Constraints (C5)∼(C7) are partially extracted from a collection of coherence conditions [35] on the introduced variables for all the fragments of all the tasks. Finally, constraint (O) gives the problem’s objective, that is, completing the last fragment of each task by its due date.Figure 3
WPM formulation for exemplified problem.All the clauses are conjunct with∧ to form a WPM problem in CNF, where clauses (C1)∼(C7) are declared hard and those in (O) are soft. Then the CNF formula is input to a WPM solver. The solver’s output includes the maximum sum of the weights of the satisfied soft clauses as well as the corresponding assignment of all the Boolean variables.In the exemplified problem, the assigned truth values of all the Boolean variables are listed in Figure4, from which the exact start time of each fragment can be derived. Consider f12. sa1,02=1 and sa1,12=0 indicate that f12 starts at or after time 0, but it does not start at or after time 1. Then we can readily determine that f12 starts at time 0. A similar reference can be made on f13, which starts at time 1. Both τ2 and τ3 can be completed by their due dates. This is ensured by eb2=1 and eb3=1. Now, consider f11. Figure 4 shows that sa1,11=1 and sa1,21=1. Since LST11=1, that sa1,21=1 means that f11 cannot start at or before LST11. Similarly, as indicated by the fact that sa2,31=1, f21 cannot start at or before LST21 either. Thus, we infer that τ1 cannot finish on time. This is confirmed by eb1=0. As a result, the maximized total weight of the completed on-time tasks is 2+3=5, achieved by completing τ2 and τ3 by their due dates.Figure 4
Assignment of all Boolean variables in the exemplified problem.


## 3.1. Feature Preprocessing

Given a task setΓ=τ1,…,τn, where each task τℓ∈Γ is characterized by rℓ,cℓ,dℓ,wℓ, ∀τℓ∈Γ, τℓ cannot start before its release date rℓ. Thus, the possible Earliest Start Time (EST) of τℓ, denoted by ESTℓ, is equal to its release date rℓ, and the Earliest Completion Time (ECT) of τℓ, denoted by ECTℓ, is ESTi+ci. ∀τk,τℓ∈Rdp, ESTℓ is jointly restricted by rℓ and ECTk. Specifically, if ECTk≤rℓ, then ESTℓ=rℓ; otherwise, ESTℓ=ECTk, suggesting that τℓ should wait until τk is finished. Typically, let Pℓ be the set of predecessors of τℓ; then ESTℓ=maxrℓ,maxτk∈PℓECTk.AfterESTℓ for each τℓ in Γ has been determined, EST and ECT of each fragment in τℓ can be calculated as follows:(i)
Earliest Start Time (EST) offiℓ is denoted by ESTiℓ, where ESTiℓ=ESTℓ+∑u=1i−1cuℓ. ∀τℓ∈Γ and ∀fiℓ∈τℓ, fiℓ should start at or after ESTiℓ, indicating that fiℓ cannot be started before all its previous fragments are finished. Typically, EST1ℓ=ESTℓ.(ii)
Earliest Completion Time (ECT) offiℓ is denoted by ECTiℓ, where ECTiℓ=ESTℓ+∑u=1icuℓ. No fragment fiℓ can be completed before ECTiℓ. Particularly, ECTiℓ=ESTiℓ+ciℓ.In addition to EST and ECT,∀τℓ∈Γ, each fragment fiℓ∈τℓ is characterized by the two following types of time:(i)
Latest Start Time (LST) offiℓ is denoted by LSTiℓ, where LSTiℓ=dℓ−∑u=iqℓcuℓ. If fiℓ fails to start before LSTiℓ, τℓ cannot end by its due date dℓ, and thus this task becomes worthless to the system.(ii)
Latest Completion Time (LCT) offiℓ is denoted by LCTiℓ, where LCTiℓ=dℓ−∑u=i+1qℓcuℓ. Particularly, LCTiℓ=LSTiℓ+ciℓ.Note that, in the above four critical time points, ECT is unrelated to our WPM encoding. Nevertheless, it is indispensable in the previous work [38], which will be discussed in Section 4..


## 3.2. WPM Formulation

This section introduces how to encode the scheduling problem as a WPM problem. A WPM instance consists of a number of clauses that need to be managed by the WPM solver. To formulate all the necessary constraints that characterize the scheduling model, we introduce the three following Boolean variables:(i)
sai,tℓ, which is true if fiℓ starts at time t or later(ii)
pri,jℓ,k, which is true if fiℓ precedes fjk(iii)
ebℓ, which is true if τℓ ends by its due date dℓBased on the generated Boolean variables, the WPM encoding can be implemented. In what follows, several rules are presented to encode the features of fragments into a set of hard clauses. The main encoding is derived and enhanced from previous work [35, 36, 38]. Logical implication a⟶b is equivalent to ¬a∨b in classical logic.(i)
(C1)∀τℓ∈Γ, the first fragment of τℓ, that is, f1ℓ, starts at or after EST1ℓ:(1)sa1,EST1ℓℓ.(ii)
(C2)∀τℓ∈Γ and ∀fiℓ,fi+1ℓ∈τℓ, fiℓ precedes fi+1ℓ:(2)pri,i+1ℓ,ℓ.(iii)
(C3)∀τk,τℓ∈Γ, ∀fik∈τk, and ∀fjℓ∈τℓ, if k≠l, τk≺τℓ, τℓ≺τk, ESTik<LCTjℓ and ESTjℓ<LCTik, and then fik and fjℓ may require the processor at the same time. In this condition, fik precedes fjℓ or fjℓ precedes fik:(3)pri,jk,ℓ∨prj,iℓ,k.(iv)
(C4)∀τk,τℓ∈Rdp, if τk fails to be completed by its due date, then τℓ cannot even start at LST1ℓ:(4)¬ebk⟶sa1,LST1ℓ+1ℓ.(v)
Furthermore, ifdk>EST1ℓ, the first fragment of τℓ cannot start until the last fragment of τk finishes. That is, if dk>EST1ℓ, then the constraint that fqkk precedes f1ℓ is enforced:(5)prqk,1k,ℓ.(vi)
(C5)∀τℓ∈Γ and ∀fiℓ∈τℓ, if fiℓ starts at or after time t, then it starts at or after time t−1:(6)sai,tℓ⟶sai,t−1ℓ,ESTiℓ+1≤t≤LSTiℓ+1.(vii)
(C6)∀τℓ∈Γ, if τℓ ends before its due date dℓ, then last fragment fqℓℓ must start at or before time LSTqℓℓ. In other words, fqℓℓ cannot start at or after time LSTqℓℓ+1:(7)ebℓ⟶¬saqℓ,LSTqℓℓ+1ℓ.(viii)
(C7)∀τk,τℓ∈Γ, ∀fik∈τk, and ∀fjℓ∈τℓ, if fik starts at or after time t and fjℓ follows fik, then fjℓ cannot start until fik is finished. That is, for each pri,jk,ℓ asserted by (C2)∼(C4), one clause is generated:(8)sai,tk∧pri,jk,ℓ⟶saj,t′ℓ,wheret varies in ESTik,LSTik+1 and(9)t′=LSTjℓ+1,ift+cik>LSTjℓ,ESTjℓ,ift+cik<ESTjℓ,t+cik,Otherwise.This formula reveals the following facts: First, iffik ends after LSTjℓ (i.e., t+cik>LSTjℓ), then fjℓ cannot start at or before LSTjℓ. Second, if fik finishes before ESTjℓ (i.e., t+cik<ESTjℓ), then fjℓ starts at or after ESTjℓ. Otherwise, fjℓ must start at or after time fik finishes, that is, t+cik.Up to this point, we have encoded the scheduling features as Boolean formulas that can be converted to a set of clauses. Since the scheduling features are intrinsic properties inherent in the tasks and their fragments, such clauses are specified as hard, indicating that all of them must absolutely be satisfied. For convenience, we refer to the set of hard clauses introduced in (C1)∼(C7) as C.A task is said to be on time if and only if it is completed before its due date. Thus, the scheduling objective can be directly encoded by the following rule:(O) Maximizing the sum of the weights of on-time tasks:(10)ebℓ,wℓ,1≤ℓ≤n.Equation (10) indicates that if clause ebℓ is satisfied (i.e., evaluating to true), then weight wℓ is gained; otherwise, the gain is zero. To simplify the discussion, we introduce O to denote the set of clauses in equation (10). In an overloaded system, not all tasks can be completed before their due dates. To handle such situations, we declare the clauses in O to be soft, indicating that completing all the tasks by their due dates is a soft constraint. Conjunct with C, the problem is then C,O. This leads to a WPM problem, which tries to find an assignment of variables to satisfy all the hard clauses in C and to maximize the sum of the weights of the satisfied soft clauses in O, that is, to maximize ∑ℓ=1nwℓ⋅ebℓ.


## 3.3. A Pedagogical Example

Let us consider a simple scheduling problem to describe how WPM formulation works. As shown in Figure2(a), there are a set of real-time tasks Γ=τ1,τ2,τ3, where both τ1 and τ3 rely on the computed result of τ2, represented as τ2≺τ1 and τ2≺τ3; that is, Rdp=τ2,τ1,τ2,τ3. The release dates, the execution times, the due dates, and the weights of these tasks are, respectively, defined as τ1=0,2,3,1, τ2=0,1,1,2, and τ3=0,1,2,3. Suppose that τ1 has two fragments, that is, f11,f21. τ2 and τ3 each have one, denoted by f12 and f13, respectively. The execution time of each fragment is 1.Figure 2
A simple scheduling example. (a) Original problem. (b) Problem after feature preprocessing.
(a)(b)The refined problem exhibition and the critical time points after feature preprocessing are summarized in Figure2(b) and Table 2, respectively. Since ECT has nothing to do with the WPM encoding, we omit this entry in Table 2 for conciseness.Table 2
Critical time points of each fragment in three tasks.
TaskFragmentESTLSTLCTτ1f11112f21223τ2f12001τ3f13112The MaxSAT formulation applied to the scheduling problem is shown in Figure3. Constraint (C1) states that each task starts at or after its EST. Constraints (C2) and (C3) work together to specify the execution sequence of the fragments. (C2) forces all the fragments in a single task to be executed sequentially, and (C3) guarantees no overlap of the execution times of any two fragments in different tasks. In the three tasks, only τ1 has more than one fragment, and hence constraint (C2) only applies to τ1, ensuring that f11 precedes f21. Constraint (C3) applies to pairs of fragments fik and fjℓk≠l satisfying ESTik<LCTjℓ and ESTjℓ<LCTik. If both conditions are met, then fik and fjℓ may simultaneously occupy the processor, and thus we need to decide in what order to execute them. Constraint (C3) tackles this ordering dilemma, which states that either one can precede the other. Consider f11 and f13. As seen in Table 2, EST11<LCT13 and EST13<LCT11; hence, we must explicitly specify that f11 precedes f13 or f13 precedes f11; otherwise, the execution time of these two fragments may overlap. Constraint (C4) applies to a situation where tasks have dependency relations. In the example, τ2 is the predecessor of both τ1 and τ3; thus we should give up processing τ1 and τ3 if τ2 misses its due date. In addition, given d2=EST11 and d2=EST13, there is no need to explicitly specify the execution sequence of the predecessor and successors since τ2 must have finished before τ1 and τ3 start. Constraints (C5)∼(C7) are partially extracted from a collection of coherence conditions [35] on the introduced variables for all the fragments of all the tasks. Finally, constraint (O) gives the problem’s objective, that is, completing the last fragment of each task by its due date.Figure 3
WPM formulation for exemplified problem.All the clauses are conjunct with∧ to form a WPM problem in CNF, where clauses (C1)∼(C7) are declared hard and those in (O) are soft. Then the CNF formula is input to a WPM solver. The solver’s output includes the maximum sum of the weights of the satisfied soft clauses as well as the corresponding assignment of all the Boolean variables.In the exemplified problem, the assigned truth values of all the Boolean variables are listed in Figure4, from which the exact start time of each fragment can be derived. Consider f12. sa1,02=1 and sa1,12=0 indicate that f12 starts at or after time 0, but it does not start at or after time 1. Then we can readily determine that f12 starts at time 0. A similar reference can be made on f13, which starts at time 1. Both τ2 and τ3 can be completed by their due dates. This is ensured by eb2=1 and eb3=1. Now, consider f11. Figure 4 shows that sa1,11=1 and sa1,21=1. Since LST11=1, that sa1,21=1 means that f11 cannot start at or before LST11. Similarly, as indicated by the fact that sa2,31=1, f21 cannot start at or before LST21 either. Thus, we infer that τ1 cannot finish on time. This is confirmed by eb1=0. As a result, the maximized total weight of the completed on-time tasks is 2+3=5, achieved by completing τ2 and τ3 by their due dates.Figure 4
Assignment of all Boolean variables in the exemplified problem.


## 4. Theoretical Discussion

Recall that, in the scheduling model described in Section2, each task τℓ is represented as a 4-tuple τℓ=rℓ,cℓ,dℓ,wℓ. Consider a special case where the weights of all the tasks are equal to a constant w, that is, ∀τℓ∈Γ, wℓ=w. According to Section 3.2, to encode this problem, a set of weighted soft clauses O=ebℓ,w are introduced, where 1≤ℓ≤n. Conjunct with hard clauses C, problem C,O becomes a special WPM problem with equal weights, which tries to find an assignment of variables to satisfy all hard clauses in C and to maximize w⋅∑ℓ=1nebℓ. Obviously, the essence of maximizing w⋅∑ℓ=1nebℓ is equivalent to maximizing ∑ℓ=1nebℓ. This is a PM problem encoded by [38], where each task τℓ is modeled as a 3-tuple τℓ=rℓ,cℓ,dℓ, and the scheduling goal is to maximize the total number of on-time tasks. In this section, we make theoretical comparisons between PM-based [38] and our WPM-based optimization frameworks when all the tasks have equal weights.


### 4.1. Similarities of PM and WPM Formulations

Essentially, the purpose of solving the scheduling problem is to determine the start time of each fragment to construct an optimal scheduling solution. To describe such crucial information,∀τℓ∈Γ and ∀fiℓ∈τℓ, a set of Boolean variables sai,tℓESTiℓ≤t≤LSTiℓ+1 are introduced to indicate whether fiℓ starts at or after time t. As long as the truth values of sa variables are all assigned, we can readily determine the exact start time of each fragment. To be specific, if we find a certain time t′∈ESTiℓ,LSTiℓ such that sai,tℓ=1 for t≤t′ and sai,tℓ=0 for t>t′, then we can determine that the start time of fiℓ is t′. If sai,tℓ is constantly true when t varies in ESTiℓ,LSTiℓ+1, we can conclude that τℓ is late. Note that it is impossible to designate sai,tℓ as true while making sai,t−1ℓ false, since if fiℓ starts at or after time t, fiℓ must start at or after t−1. This constraint is interpreted by rule (C5) in our encoding. In addition, ∀τℓ∈Γ and ∀fiℓ∈τℓ, the start time of fiℓ should be at or after ESTiℓ. Compared with PM, WPM encodes this constraint in a more concise way by (C1). We postpone the discussion later in Section 4.2.Aside from the inherent properties of a fragment’s start time specified in (C1) and (C5), whether a fragment can start at a certain time is constrained by two other factors. The first is the execution order of the fragments, which should be explicitly pointed out in the following two situations: if two fragments belong to the same task, then they should be executed sequentially; if two fragments from different tasks may simultaneously occupy the processor, then either one can precede the other. The execution order of two fragments,fik and fjℓ, is characterized by Boolean variable pri,jk,ℓ, and the constraints specified in the above two cases are interpreted by rules (C2) and (C3), respectively. If the execution order of the two fragments is determined, the relation of their start times should be specified. To be specific, if fik precedes fjℓ, then fjℓ must start after fik finishes. This constraint is guaranteed by rule (C7). Up to this point, all the Boolean variables and clauses introduced by PM and WPM are identical. That is, rules (C2), (C3), (C5), and (C7) are all consistent with those introduced in PM.


### 4.2. WPM Improvement

As mentioned in Section4.1, ∀τℓ∈Γ and ∀fiℓ∈τℓ, the start time of fiℓ cannot be earlier than ESTiℓ. PM interprets this constraint by introducing one hard clause sai,ESTiℓℓ for 1≤i≤qℓ; thus, a total of qℓ clauses are generated for τℓ. In comparison, as described by (C1) in Section 3.2, WPM generates only one clause sa1,EST1ℓℓ for each task τℓ∈Γ no matter how many fragments τℓ contains. By combining (C1) with constraints (C2) and (C7), we can easily obtain sai,ESTiℓℓ=1 for 1≤i≤qℓ, which is the same as that declared by PM. Therefore, the updated rule (C1) reduces the number of generated clauses while maintaining the correctness of the encoding.For tasks with dependency relations, their execution sequence may be explicitly or implicitly specified. In particular,∀τk,τℓ∈Rdp, PM indistinguishably generates prqk,1k,ℓ for the dependency relation τk≺τℓ. In fact, if the due date of τk is no later than the EST of τℓ, that is, dk≤EST1ℓ, τℓ naturally starts after τk is completed; thus the constraint that is explicitly imposed on the execution sequence is unnecessary and can be omitted safely. WPM formulation refined the encoding in (C4) by introducing prqk,1k,ℓ to interpret the constraint that τk precedes τℓ only when dk>EST1ℓ; thus, redundant variables and clauses are eliminated.Another factor that affects a fragment’s start time is the completion time of a task. In general, if a task is expected to be completed by a particular time, then each fragment of the task should not start later than its LST. The relation of completion time and LST is encoded by PM and WPM in different ways. In PM, for each fragmentfiℓ1≤ℓ≤n,1≤i≤qℓ, a set of Boolean variables ebi,tℓECTiℓ−1≤t≤LCTiℓ are introduced to indicate whether fiℓ finishes at or before time t. Then a set of hard clauses are generated to restrict the values of the eb variables.(i)
(H1) Iffiℓ ends by t, then it ends by time t+1:(11)ebi,tℓ⟶ebi,t+1ℓ,ECTiℓ−1≤t≤LCTiℓ−1,(ii)
(H2) ifτℓ is completed by its due date, then, ∀fiℓ∈τℓ, fiℓ should finish by LCTiℓ:(12)ebqℓ,dℓℓ⟶ebi,LCTiℓℓ,1≤i≤qℓ−1,(iii)
(H3) iffiℓ starts at or after time t, then it cannot end before time t+ciℓ−1:(13)sai,tℓ⟶¬ebi,t+ciℓ−1ℓ,ESTiℓ≤t≤LSTiℓ+1,In fact, not all the variables and clauses in (H1)∼(H3) are requisite. Given a task, instead of generating variables to characterize each fragment’s completion time, it suffices to create only one variable to declare the task’s due date and introduce one clause to clarify how the task’s due date both restricts and is restricted by its start time. In particular, ∀τℓ∈Γ, WPM introduces Boolean variable ebℓ to describe whether τℓ can finish by its due date. Then a constraint is set to correlate the due date and the start time of τℓ as follows: if τℓ ends by dℓ, then fqℓℓ must start at or before LSTqℓℓ. In other words, if fqℓℓ fails to start at or before LSTqℓℓ, then it cannot end by dℓ. This constraint is encoded by just one clause described in rule (C6), as declared in Section 3.2:(14)ebℓ⟶¬saqℓ,LSTqℓℓ+1ℓ.Theorem 1.
Given taskτℓ∈Γ, if ebqℓ,dℓℓ in PM (resp., ebℓ in WPM) is evaluated as true, then sai,LSTiℓ+1ℓ for 1≤i≤qℓ in both PM and WPM are false.Proof.
In PM, according to (H2),ebqℓ,dℓℓ=1 makes ebi,LCTiℓℓ=1 for 1≤i≤qℓ−1. This indicates that, ∀fiℓ∈τℓ, fiℓ should finish by LCTiℓ. Combined with (H3), it can be inferred that sai,LSTi+1ℓℓ=0 for 1≤i≤qℓ.
In WPM, thatebℓ=1 leads to saqℓ,LSTqℓℓ+1ℓ=0 by (C6). In addition, based on (C2) and (C7), it is clear that saqℓ−1,LSTqℓ−1ℓ+1ℓ⟶saqℓ,LSTqℓℓ+1ℓ holds. Under the condition where saqℓ,LSTqℓℓ+1ℓ=0, it can be immediately inferred that saqℓ−1,LSTqℓ−1ℓ+1ℓ=0. By repeatedly substituting (C2) into (C7), we finally obtain sai,LSTi+1ℓℓ=0 for 1≤i≤qℓ.Theorem 2.
Given taskτℓ∈Γ, if ∃fiℓ∈τℓ that makes sai,LSTiℓ+1ℓ be evaluated as true, then ebqℓ,dℓℓ in PM (resp., ebℓ in WPM) is false.Proof.
In PM, by (H3),sai,LSTiℓ+1ℓ=1 makes ebi,LCTiℓℓ=0. Combined with (H2), it is obvious that ebqℓ,dℓℓ=0.
In WPM, we discuss the two following cases:(1)
If criticalfiℓ, which makes sai,LSTiℓ+1ℓ=1, is the last fragment in τℓ, that is, i=qℓ, it is obvious that ebℓ=0 by (C6).(2)
If1≤i≤qℓ−1, according to (C2) and (C7), we have sai,LSTiℓ+1ℓ⟶sai+1,LSTi+1ℓ+1ℓ. Since sai,LSTiℓ+1ℓ=1, it is clear that sai+1,LSTi+1ℓ+1ℓ=1. The step of substituting (C2) into (C7) can be repeated until i+1=qℓ. Finally, we have saqℓ,LSTqℓℓ+1ℓ=1. Then, by (C6), ebℓ=0 is obtained.
Theorem1 shows that if ebqℓ,dℓℓ=1 in PM (resp., ebℓ=1), both PM and WPM guarantee that sai,LSTi+1ℓℓ=0 for 1≤i≤qℓ. Theorem 2 shows that when there exists a fragment fiℓ∈τℓ that leads to sai,LSTiℓ+1ℓ=1, both PM and WPM come to the same conclusion that τℓ cannot finish by τℓ, pointed out by ebqℓ,dℓℓ=0 and ebℓ=0 in PM and WPM, respectively. Therefore, the eb variables introduced in PM and WPM have the same impact on the sa variables and vice versa. Note that, ∀fqℓℓ∈τℓ, if saqℓ,LSTqℓℓ+1ℓ=0, a WPM solver always prefers ebqℓ,dℓℓ=1 in PM (resp., ebℓ=1 in WPM) to satisfy soft clause ebqℓ,dℓℓ (resp., ebℓ,w). In other words, a WPM solver never prefers ebqℓ,dℓℓ=0 in PM (resp., ebℓ=0 in WPM) as long as all the hard clauses input to the solver are satisfied.Example 1.
This example shows the differences between the PM and WPM formulations when dealing with the completion time. Assume thatτ1=0,2,3,1 is a task in Γ, which contains two fragments f11,f21. Each fragment has execution time 1. Table 3 shows the Boolean variables and the hard clauses introduced by PM and WPM to characterize the fragments’ completion times.
First, we can determine thatECT11=1, LCT11=2, ECT21=2, and LCT21=3. To encode τ1, PM introduces a series of Boolean variables, eb1,01,eb1,11,eb1,21 and eb2,11,eb2,21,eb2,31 for f11 and f21, respectively, representing whether each fragment is completed by time point t, where ECTi1−1≤t≤LCTi1 for 1≤i≤2. The relation of ebi,t1 and ebi,t+11 is specified by rule (H1). To make τ1 finish by its due date, f11 should be completed no later than time 2. This is guaranteed by rule (H2). Finally, the relation between a fragment’s start and completion times is indicated by rule (H3). Therefore, to constrain the completion time of each fragment, six Boolean variables and eleven hard clauses are generated by PM. By contrast, WPM introduces only one variable eb1 to indicate whether τ1 is completed by its due date. Then a hard clause is generated to constrain τ1’s due date and its last fragment’s start time. In this way, both the Boolean variables and clauses generated by the WPM formulation are reduced.
The experimental comparison of these two encodings is demonstrated in Subsection5.3.Table 3
Encodings related toeb variables in PM and WPM formulations.
VariablesPM [38]WPMeb1,01, eb1,11, eb1,21,eb2,11, eb2,21, eb2,31eb1Clauses(H1)¬eb1,01∨eb1,11, ¬eb1,11∨eb1,21, ¬eb2,11∨eb2,21, ¬eb2,21∨eb2,31¬eb1∨¬sa2,31(H2)¬eb2,31∨eb1,21(H3)¬sa1,01∨¬eb1,01, ¬sa1,11∨¬eb1,11, ¬sa1,21∨¬eb1,21¬sa2,11∨¬eb2,11, ¬sa2,21∨¬eb2,21, ¬sa2,31∨¬eb2,31


## 4.1. Similarities of PM and WPM Formulations

Essentially, the purpose of solving the scheduling problem is to determine the start time of each fragment to construct an optimal scheduling solution. To describe such crucial information,∀τℓ∈Γ and ∀fiℓ∈τℓ, a set of Boolean variables sai,tℓESTiℓ≤t≤LSTiℓ+1 are introduced to indicate whether fiℓ starts at or after time t. As long as the truth values of sa variables are all assigned, we can readily determine the exact start time of each fragment. To be specific, if we find a certain time t′∈ESTiℓ,LSTiℓ such that sai,tℓ=1 for t≤t′ and sai,tℓ=0 for t>t′, then we can determine that the start time of fiℓ is t′. If sai,tℓ is constantly true when t varies in ESTiℓ,LSTiℓ+1, we can conclude that τℓ is late. Note that it is impossible to designate sai,tℓ as true while making sai,t−1ℓ false, since if fiℓ starts at or after time t, fiℓ must start at or after t−1. This constraint is interpreted by rule (C5) in our encoding. In addition, ∀τℓ∈Γ and ∀fiℓ∈τℓ, the start time of fiℓ should be at or after ESTiℓ. Compared with PM, WPM encodes this constraint in a more concise way by (C1). We postpone the discussion later in Section 4.2.Aside from the inherent properties of a fragment’s start time specified in (C1) and (C5), whether a fragment can start at a certain time is constrained by two other factors. The first is the execution order of the fragments, which should be explicitly pointed out in the following two situations: if two fragments belong to the same task, then they should be executed sequentially; if two fragments from different tasks may simultaneously occupy the processor, then either one can precede the other. The execution order of two fragments,fik and fjℓ, is characterized by Boolean variable pri,jk,ℓ, and the constraints specified in the above two cases are interpreted by rules (C2) and (C3), respectively. If the execution order of the two fragments is determined, the relation of their start times should be specified. To be specific, if fik precedes fjℓ, then fjℓ must start after fik finishes. This constraint is guaranteed by rule (C7). Up to this point, all the Boolean variables and clauses introduced by PM and WPM are identical. That is, rules (C2), (C3), (C5), and (C7) are all consistent with those introduced in PM.


## 4.2. WPM Improvement

As mentioned in Section4.1, ∀τℓ∈Γ and ∀fiℓ∈τℓ, the start time of fiℓ cannot be earlier than ESTiℓ. PM interprets this constraint by introducing one hard clause sai,ESTiℓℓ for 1≤i≤qℓ; thus, a total of qℓ clauses are generated for τℓ. In comparison, as described by (C1) in Section 3.2, WPM generates only one clause sa1,EST1ℓℓ for each task τℓ∈Γ no matter how many fragments τℓ contains. By combining (C1) with constraints (C2) and (C7), we can easily obtain sai,ESTiℓℓ=1 for 1≤i≤qℓ, which is the same as that declared by PM. Therefore, the updated rule (C1) reduces the number of generated clauses while maintaining the correctness of the encoding.For tasks with dependency relations, their execution sequence may be explicitly or implicitly specified. In particular,∀τk,τℓ∈Rdp, PM indistinguishably generates prqk,1k,ℓ for the dependency relation τk≺τℓ. In fact, if the due date of τk is no later than the EST of τℓ, that is, dk≤EST1ℓ, τℓ naturally starts after τk is completed; thus the constraint that is explicitly imposed on the execution sequence is unnecessary and can be omitted safely. WPM formulation refined the encoding in (C4) by introducing prqk,1k,ℓ to interpret the constraint that τk precedes τℓ only when dk>EST1ℓ; thus, redundant variables and clauses are eliminated.Another factor that affects a fragment’s start time is the completion time of a task. In general, if a task is expected to be completed by a particular time, then each fragment of the task should not start later than its LST. The relation of completion time and LST is encoded by PM and WPM in different ways. In PM, for each fragmentfiℓ1≤ℓ≤n,1≤i≤qℓ, a set of Boolean variables ebi,tℓECTiℓ−1≤t≤LCTiℓ are introduced to indicate whether fiℓ finishes at or before time t. Then a set of hard clauses are generated to restrict the values of the eb variables.(i)
(H1) Iffiℓ ends by t, then it ends by time t+1:(11)ebi,tℓ⟶ebi,t+1ℓ,ECTiℓ−1≤t≤LCTiℓ−1,(ii)
(H2) ifτℓ is completed by its due date, then, ∀fiℓ∈τℓ, fiℓ should finish by LCTiℓ:(12)ebqℓ,dℓℓ⟶ebi,LCTiℓℓ,1≤i≤qℓ−1,(iii)
(H3) iffiℓ starts at or after time t, then it cannot end before time t+ciℓ−1:(13)sai,tℓ⟶¬ebi,t+ciℓ−1ℓ,ESTiℓ≤t≤LSTiℓ+1,In fact, not all the variables and clauses in (H1)∼(H3) are requisite. Given a task, instead of generating variables to characterize each fragment’s completion time, it suffices to create only one variable to declare the task’s due date and introduce one clause to clarify how the task’s due date both restricts and is restricted by its start time. In particular, ∀τℓ∈Γ, WPM introduces Boolean variable ebℓ to describe whether τℓ can finish by its due date. Then a constraint is set to correlate the due date and the start time of τℓ as follows: if τℓ ends by dℓ, then fqℓℓ must start at or before LSTqℓℓ. In other words, if fqℓℓ fails to start at or before LSTqℓℓ, then it cannot end by dℓ. This constraint is encoded by just one clause described in rule (C6), as declared in Section 3.2:(14)ebℓ⟶¬saqℓ,LSTqℓℓ+1ℓ.Theorem 1.
Given taskτℓ∈Γ, if ebqℓ,dℓℓ in PM (resp., ebℓ in WPM) is evaluated as true, then sai,LSTiℓ+1ℓ for 1≤i≤qℓ in both PM and WPM are false.Proof.
In PM, according to (H2),ebqℓ,dℓℓ=1 makes ebi,LCTiℓℓ=1 for 1≤i≤qℓ−1. This indicates that, ∀fiℓ∈τℓ, fiℓ should finish by LCTiℓ. Combined with (H3), it can be inferred that sai,LSTi+1ℓℓ=0 for 1≤i≤qℓ.
In WPM, thatebℓ=1 leads to saqℓ,LSTqℓℓ+1ℓ=0 by (C6). In addition, based on (C2) and (C7), it is clear that saqℓ−1,LSTqℓ−1ℓ+1ℓ⟶saqℓ,LSTqℓℓ+1ℓ holds. Under the condition where saqℓ,LSTqℓℓ+1ℓ=0, it can be immediately inferred that saqℓ−1,LSTqℓ−1ℓ+1ℓ=0. By repeatedly substituting (C2) into (C7), we finally obtain sai,LSTi+1ℓℓ=0 for 1≤i≤qℓ.Theorem 2.
Given taskτℓ∈Γ, if ∃fiℓ∈τℓ that makes sai,LSTiℓ+1ℓ be evaluated as true, then ebqℓ,dℓℓ in PM (resp., ebℓ in WPM) is false.Proof.
In PM, by (H3),sai,LSTiℓ+1ℓ=1 makes ebi,LCTiℓℓ=0. Combined with (H2), it is obvious that ebqℓ,dℓℓ=0.
In WPM, we discuss the two following cases:(1)
If criticalfiℓ, which makes sai,LSTiℓ+1ℓ=1, is the last fragment in τℓ, that is, i=qℓ, it is obvious that ebℓ=0 by (C6).(2)
If1≤i≤qℓ−1, according to (C2) and (C7), we have sai,LSTiℓ+1ℓ⟶sai+1,LSTi+1ℓ+1ℓ. Since sai,LSTiℓ+1ℓ=1, it is clear that sai+1,LSTi+1ℓ+1ℓ=1. The step of substituting (C2) into (C7) can be repeated until i+1=qℓ. Finally, we have saqℓ,LSTqℓℓ+1ℓ=1. Then, by (C6), ebℓ=0 is obtained.
Theorem1 shows that if ebqℓ,dℓℓ=1 in PM (resp., ebℓ=1), both PM and WPM guarantee that sai,LSTi+1ℓℓ=0 for 1≤i≤qℓ. Theorem 2 shows that when there exists a fragment fiℓ∈τℓ that leads to sai,LSTiℓ+1ℓ=1, both PM and WPM come to the same conclusion that τℓ cannot finish by τℓ, pointed out by ebqℓ,dℓℓ=0 and ebℓ=0 in PM and WPM, respectively. Therefore, the eb variables introduced in PM and WPM have the same impact on the sa variables and vice versa. Note that, ∀fqℓℓ∈τℓ, if saqℓ,LSTqℓℓ+1ℓ=0, a WPM solver always prefers ebqℓ,dℓℓ=1 in PM (resp., ebℓ=1 in WPM) to satisfy soft clause ebqℓ,dℓℓ (resp., ebℓ,w). In other words, a WPM solver never prefers ebqℓ,dℓℓ=0 in PM (resp., ebℓ=0 in WPM) as long as all the hard clauses input to the solver are satisfied.Example 1.
This example shows the differences between the PM and WPM formulations when dealing with the completion time. Assume thatτ1=0,2,3,1 is a task in Γ, which contains two fragments f11,f21. Each fragment has execution time 1. Table 3 shows the Boolean variables and the hard clauses introduced by PM and WPM to characterize the fragments’ completion times.
First, we can determine thatECT11=1, LCT11=2, ECT21=2, and LCT21=3. To encode τ1, PM introduces a series of Boolean variables, eb1,01,eb1,11,eb1,21 and eb2,11,eb2,21,eb2,31 for f11 and f21, respectively, representing whether each fragment is completed by time point t, where ECTi1−1≤t≤LCTi1 for 1≤i≤2. The relation of ebi,t1 and ebi,t+11 is specified by rule (H1). To make τ1 finish by its due date, f11 should be completed no later than time 2. This is guaranteed by rule (H2). Finally, the relation between a fragment’s start and completion times is indicated by rule (H3). Therefore, to constrain the completion time of each fragment, six Boolean variables and eleven hard clauses are generated by PM. By contrast, WPM introduces only one variable eb1 to indicate whether τ1 is completed by its due date. Then a hard clause is generated to constrain τ1’s due date and its last fragment’s start time. In this way, both the Boolean variables and clauses generated by the WPM formulation are reduced.
The experimental comparison of these two encodings is demonstrated in Subsection5.3.Table 3
Encodings related toeb variables in PM and WPM formulations.
VariablesPM [38]WPMeb1,01, eb1,11, eb1,21,eb2,11, eb2,21, eb2,31eb1Clauses(H1)¬eb1,01∨eb1,11, ¬eb1,11∨eb1,21, ¬eb2,11∨eb2,21, ¬eb2,21∨eb2,31¬eb1∨¬sa2,31(H2)¬eb2,31∨eb1,21(H3)¬sa1,01∨¬eb1,01, ¬sa1,11∨¬eb1,11, ¬sa1,21∨¬eb1,21¬sa2,11∨¬eb2,11, ¬sa2,21∨¬eb2,21, ¬sa2,31∨¬eb2,31


## 5. Experiments

In this section, we scrutinize the performance comparisons of the presented WPM formulation and two satisfiability-based formulations on a set of randomly generated problems. The experimental design is described in Section5.1, followed by the evaluation of WPM, SMT [39], and PM formulations [38] in Section 5.2 and Section 5.3. All tests were conducted on a 3.4 GHz Intel E3-1230 processor with 8 GB RAM. The selected solver to evaluate WPM and PM is QMaxSAT [40], which is a SAT-based solver using the CNF encodings of cardinality constraints. The solver for SMT is Z3 [41], which is a high-performance theorem prover chosen by the previous SMT formulations [33, 39].


### 5.1. Experimental Design

The procedure for generating test instances is similar to [33, 38, 39], with a variety of parameter values. Tasks’ release times are randomly generated following a discrete uniform distribution with an arriving rate λ, which represents the number of tasks that arrive during 100 time units. Clearly, a larger λ indicates that more tasks arrive in the system during a specific period of time, thus causing heavier overload. For each task τℓ, the execution time cℓ and the number of fragments in τℓ (denoted by qℓ) are also randomly generated according to a discrete uniform distribution. The value of deadline dℓ is calculated by the formula dℓ=rℓ+sfℓ⋅cℓ, where sfℓ is a slack factor that reflects the tightness of the due date. Weight wℓ of task τℓ is randomly chosen from 1 to n in Section 5.2 and is taken as constant 1 in Section 5.3. The number of rule pairs with dependency relations is set 10% to the total number of tasks.We study the factors that may affect the performance of the satisfiability-based formulations. These factors include the number of tasksn, the task density (determined by λ), the execution time cℓ, the number of fragments qℓ, and the slack factor sfℓ. In the rest of this section, we run different types of experiments to test the possible changes on these parameters. Table 4 provides a summary of the experimental design, where DUi,j means the discrete uniform distribution over integer interval i,j. For each individual scenario, 100 problem instances are generated. For each instance and solver, we set a time limit of 300 seconds. If the solver fails to output the optimal result of an instance within the time limit, we terminate the procedure and move to the next problem instance.Table 4
Experimental design.
ScenarionλcℓqℓsfℓS150,100,…,30010DU1,30DU1,3DU1,4S21005,10,…,25DU1,30DU1,3DU1,4S310010DU1,αDU1,3DU1,4α=10,20,…,100S410010DU1,30DU1,βDU1,4β=2,4,…,12S510010DU1,30DU1,3DU1,γγ=1,2,…,7


### 5.2. Comparison on Weighted Case

This subsection evaluates the behavior of WPM and SMT formulations [39] for maximizing the total weight value of on-time tasks. The main metrics for comparison include (1) the proportion of instances solved within the given time limit and (2) the average computation time spent on solved instances. The performances of these two formulations in different types of scenarios are shown in Figure 5. Each data point is the average computation time of the solved problem instances. A number with an arrow in the figures denotes the proportion of instances solved within the time limit and is omitted if the solver addresses all the 100 instances. When the proportion of the solved instances drops to zero, the corresponding curve is omitted.Figure 5
Performance comparison of WPM and SMT for weighted cases in scenarios 1–5. (a) S1: varied number of tasksn; (b) S2: varied task arriving rate λ; (c) S3: varied execution time cℓ; (d) S4: varied number of fragments qℓ; (e) S5: varied slack factor sfℓ.
(a)(b)(c)(d)(e)As shown in Figure5, both formulations perform worse with the increasing values of all parameters. Nevertheless, in all the varied scenarios, WPM substantially outperforms SMT in terms of both the average computation time and the proportion of successfully solved instances.


### 5.3. Comparison on Unweighted Case

A Partial MaxSAT (PM) formulation for optimal scheduling on a single machine was recently presented [38]. The scheduling objective tackled by PM differs from our WPM formulation in that PM aims to maximize the total number of on-time tasks, while WPM tries to maximize the total weight of the on-time tasks. When all the tasks have equal weights, these two objectives become identical, and thus formulations on these two objectives are directly comparable. In this subsection, we compare the SMT, PM, and WPM formulations on the objective of maximizing the number of on-time tasks.The overall results with variedn, λ, cℓ, qℓ, and sfℓ are shown in Figure 6. MaxSAT encodings (both PM and WPM) solved substantially more instances than SMT within the time limit in all cases. As to the performance comparison between PM and WPM, the completion percentage of WPM is always no less than that of PM no matter how the experimental parameters change. To be specific, with the number of tasks n increasing from 50 to 300, both PM and WPM solved all the instances within the time limit (Figure 6(a)). In comparison, as any of the parameters λ, cℓ, qℓ, and sfℓ increases, WPM formulation gradually surpasses PM with more completed schedules (Figures 6(b)–6(e)).Figure 6
Completion percentage of formulations for unweighted cases in scenarios 1–5. (a) S1: varied number of tasksn; (b) S2: varied task arriving rate λ; (c) S3: varied execution time cℓ; (d) S4: varied number of fragments qℓ; (e) Scenario 5: varied slack factor sfℓ.
(a)(b)(c)(d)(e)To compare the performances of PM and WPM more clearly, we provide more criteria for evaluation. The first criterion is the average runtime of PM and WPM formulations on their respective completed schedules. Note that when PM and WPM solve different numbers of instances within the time limit, the average runtime on solved instances may not clearly reflect the efficiency of these two formulations. For example, whenqℓ∼DU1,12, WPM solved more instances than PM (as shown in Figure 6(d)) and meanwhile consumed longer time on solved instances (as shown in Figure 7(a)). In this case, the average runtime is on longer the proper metric to indicate the performance. On the other hand, we notice that, in all the tested scenarios, the instances that were solved by PM could also be addressed by WPM. Therefore, we provide a secondary criterion on runtime, that is, the average runtime of WPM, in solving the same set of instances as PM solved. Furthermore, since the computation time of MaxSAT-based methods is closely related to the numbers of variables and clauses, we collect such information for reference. The comparison results are illustrated in Figures 8–11 . Criteria for evaluating PM and WPM are summarized as follows:(i)
The average runtime of MaxSAT formulations on their respective completed schedules. The corresponding information of PM and WPM is depicted in Figures8(a), 9(a), 10(a), 7(a), and 11(a) labeled “PM” and “WPM,” respectively.(ii)
The average runtime of WPM in solving the same set of instances as PM solved. The corresponding information is depicted with label “WPM onInstPM.” If the percentages of schedules completed by PM and WPM are the same, then “WPM on InstPM” is omitted (e.g., Figure 7(a)).(iii)
The average number of variables generated by MaxSAT formulations.(iv)
The average number of clauses generated by MaxSAT formulations.Figure 7
Comparison statistics of PM and WPM for unweighted cases in Scenario 4. (a) Average runtime (s) (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 8
Comparison statistics of PM and WPM for unweighted cases in Scenario 1. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 9
Comparison statistics of PM and WPM for unweighted cases in Scenario 2. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 10
Comparison statistics of PM and WPM for unweighted cases in Scenario 3. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 11
Comparison statistics of PM and WPM for unweighted cases in Scenario 5. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Overall, the WPM formulation is more efficient than PM in both runtime criteria. The only exception appears in Figure7(a), where the average runtime of WPM and PM on solved instances when qℓ∼DU1,12 is around 140 and 80 seconds, respectively. Although the average computation time taken by WPM is longer than that by PM, Figure 6(d) shows that WPM managed to solve 14 instances, while PM solved only 8 within the time limit. In this case, we resort to the secondary criterion on runtime. As shown in Figure 7(a), WPM consumed merely 60 seconds to solve all the instances completed by PM. Thus, it is correct to say that WPM can make a considerable improvement to the solving time. In addition, WPM achieved more compact encodings by significantly reducing the number of Boolean variables and slightly decreasing the number of clauses. In general, the computation time increases as the numbers of variables and clauses grow. This in turn explains why WPM achieves higher efficiency in our experiment.


## 5.1. Experimental Design

The procedure for generating test instances is similar to [33, 38, 39], with a variety of parameter values. Tasks’ release times are randomly generated following a discrete uniform distribution with an arriving rate λ, which represents the number of tasks that arrive during 100 time units. Clearly, a larger λ indicates that more tasks arrive in the system during a specific period of time, thus causing heavier overload. For each task τℓ, the execution time cℓ and the number of fragments in τℓ (denoted by qℓ) are also randomly generated according to a discrete uniform distribution. The value of deadline dℓ is calculated by the formula dℓ=rℓ+sfℓ⋅cℓ, where sfℓ is a slack factor that reflects the tightness of the due date. Weight wℓ of task τℓ is randomly chosen from 1 to n in Section 5.2 and is taken as constant 1 in Section 5.3. The number of rule pairs with dependency relations is set 10% to the total number of tasks.We study the factors that may affect the performance of the satisfiability-based formulations. These factors include the number of tasksn, the task density (determined by λ), the execution time cℓ, the number of fragments qℓ, and the slack factor sfℓ. In the rest of this section, we run different types of experiments to test the possible changes on these parameters. Table 4 provides a summary of the experimental design, where DUi,j means the discrete uniform distribution over integer interval i,j. For each individual scenario, 100 problem instances are generated. For each instance and solver, we set a time limit of 300 seconds. If the solver fails to output the optimal result of an instance within the time limit, we terminate the procedure and move to the next problem instance.Table 4
Experimental design.
ScenarionλcℓqℓsfℓS150,100,…,30010DU1,30DU1,3DU1,4S21005,10,…,25DU1,30DU1,3DU1,4S310010DU1,αDU1,3DU1,4α=10,20,…,100S410010DU1,30DU1,βDU1,4β=2,4,…,12S510010DU1,30DU1,3DU1,γγ=1,2,…,7


## 5.2. Comparison on Weighted Case

This subsection evaluates the behavior of WPM and SMT formulations [39] for maximizing the total weight value of on-time tasks. The main metrics for comparison include (1) the proportion of instances solved within the given time limit and (2) the average computation time spent on solved instances. The performances of these two formulations in different types of scenarios are shown in Figure 5. Each data point is the average computation time of the solved problem instances. A number with an arrow in the figures denotes the proportion of instances solved within the time limit and is omitted if the solver addresses all the 100 instances. When the proportion of the solved instances drops to zero, the corresponding curve is omitted.Figure 5
Performance comparison of WPM and SMT for weighted cases in scenarios 1–5. (a) S1: varied number of tasksn; (b) S2: varied task arriving rate λ; (c) S3: varied execution time cℓ; (d) S4: varied number of fragments qℓ; (e) S5: varied slack factor sfℓ.
(a)(b)(c)(d)(e)As shown in Figure5, both formulations perform worse with the increasing values of all parameters. Nevertheless, in all the varied scenarios, WPM substantially outperforms SMT in terms of both the average computation time and the proportion of successfully solved instances.


## 5.3. Comparison on Unweighted Case

A Partial MaxSAT (PM) formulation for optimal scheduling on a single machine was recently presented [38]. The scheduling objective tackled by PM differs from our WPM formulation in that PM aims to maximize the total number of on-time tasks, while WPM tries to maximize the total weight of the on-time tasks. When all the tasks have equal weights, these two objectives become identical, and thus formulations on these two objectives are directly comparable. In this subsection, we compare the SMT, PM, and WPM formulations on the objective of maximizing the number of on-time tasks.The overall results with variedn, λ, cℓ, qℓ, and sfℓ are shown in Figure 6. MaxSAT encodings (both PM and WPM) solved substantially more instances than SMT within the time limit in all cases. As to the performance comparison between PM and WPM, the completion percentage of WPM is always no less than that of PM no matter how the experimental parameters change. To be specific, with the number of tasks n increasing from 50 to 300, both PM and WPM solved all the instances within the time limit (Figure 6(a)). In comparison, as any of the parameters λ, cℓ, qℓ, and sfℓ increases, WPM formulation gradually surpasses PM with more completed schedules (Figures 6(b)–6(e)).Figure 6
Completion percentage of formulations for unweighted cases in scenarios 1–5. (a) S1: varied number of tasksn; (b) S2: varied task arriving rate λ; (c) S3: varied execution time cℓ; (d) S4: varied number of fragments qℓ; (e) Scenario 5: varied slack factor sfℓ.
(a)(b)(c)(d)(e)To compare the performances of PM and WPM more clearly, we provide more criteria for evaluation. The first criterion is the average runtime of PM and WPM formulations on their respective completed schedules. Note that when PM and WPM solve different numbers of instances within the time limit, the average runtime on solved instances may not clearly reflect the efficiency of these two formulations. For example, whenqℓ∼DU1,12, WPM solved more instances than PM (as shown in Figure 6(d)) and meanwhile consumed longer time on solved instances (as shown in Figure 7(a)). In this case, the average runtime is on longer the proper metric to indicate the performance. On the other hand, we notice that, in all the tested scenarios, the instances that were solved by PM could also be addressed by WPM. Therefore, we provide a secondary criterion on runtime, that is, the average runtime of WPM, in solving the same set of instances as PM solved. Furthermore, since the computation time of MaxSAT-based methods is closely related to the numbers of variables and clauses, we collect such information for reference. The comparison results are illustrated in Figures 8–11 . Criteria for evaluating PM and WPM are summarized as follows:(i)
The average runtime of MaxSAT formulations on their respective completed schedules. The corresponding information of PM and WPM is depicted in Figures8(a), 9(a), 10(a), 7(a), and 11(a) labeled “PM” and “WPM,” respectively.(ii)
The average runtime of WPM in solving the same set of instances as PM solved. The corresponding information is depicted with label “WPM onInstPM.” If the percentages of schedules completed by PM and WPM are the same, then “WPM on InstPM” is omitted (e.g., Figure 7(a)).(iii)
The average number of variables generated by MaxSAT formulations.(iv)
The average number of clauses generated by MaxSAT formulations.Figure 7
Comparison statistics of PM and WPM for unweighted cases in Scenario 4. (a) Average runtime (s) (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 8
Comparison statistics of PM and WPM for unweighted cases in Scenario 1. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 9
Comparison statistics of PM and WPM for unweighted cases in Scenario 2. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 10
Comparison statistics of PM and WPM for unweighted cases in Scenario 3. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Figure 11
Comparison statistics of PM and WPM for unweighted cases in Scenario 5. (a) Average runtime (s). (b) Number of variables. (c) Number of clauses.
(a)(b)(c)Overall, the WPM formulation is more efficient than PM in both runtime criteria. The only exception appears in Figure7(a), where the average runtime of WPM and PM on solved instances when qℓ∼DU1,12 is around 140 and 80 seconds, respectively. Although the average computation time taken by WPM is longer than that by PM, Figure 6(d) shows that WPM managed to solve 14 instances, while PM solved only 8 within the time limit. In this case, we resort to the secondary criterion on runtime. As shown in Figure 7(a), WPM consumed merely 60 seconds to solve all the instances completed by PM. Thus, it is correct to say that WPM can make a considerable improvement to the solving time. In addition, WPM achieved more compact encodings by significantly reducing the number of Boolean variables and slightly decreasing the number of clauses. In general, the computation time increases as the numbers of variables and clauses grow. This in turn explains why WPM achieves higher efficiency in our experiment.


## 6. Adaption for Parallel-Machine Scheduling Problem

While the WPM formulation is designed for single-machine scheduling, the encoding can be extended to parallel identical machines with minor changes. This section shows how to apply the WPM formulation to parallel identical machine scheduling problems.The parallel-machine scheduling involves processingn tasks Γ=τ1,…,τn on m identical machines ℳ=M1,M2,…,Mm. Each machine can handle only one task at a time, and each task cannot be processed in parallel. Other settings of the problem are consistent with the single-machine scheduling problem described in Section 2. Given a set of tasks Γ and that of machines ℳ, the optimization problem is not only to find a schedule that gives the start execution time of each fragment fiℓ∈τℓ in Γ but also a mapping for fiℓ to a machine in ℳ.To indicate on which machine a fragment is executed,∀τℓ∈Γ, ∀fiℓ∈τℓ, and ∀Mu∈ℳ, we extend the single-machine scheduling formulation by introducing one more Boolean variable bi,uℓ. bi,uℓ=1 if fiℓ is executed by Mu and bi,uℓ=0 otherwise. Correspondingly, rule (C3) in Section 3.2 is replaced with the two following additional constraints:(i)
(R1)∀τℓ∈Γ and ∀fiℓ∈τℓ, fiℓ is allocated and executed on a single machine:(15)∨u=1,…,mbi,uℓ,1≤ℓ≤n,1≤i≤qℓ.(ii)
(R2)∀τk,τℓ∈Γ, ∀fik∈τk, and ∀fjℓ∈τℓ, if k≠l, τk≺τℓ, τℓ≺τk, ESTik<LCTjℓ and ESTjℓ<LCTik, and then fik and fjℓ may require the processor at the same time. In this condition, fik precedes fjℓ or fjℓ precedes fik:(16)bi,uk∧bi,uℓ⟶pri,jk,ℓ∨prj,iℓ,k.We refer to the set of hard clauses introduced in (R1) and (R2) asℛ and rules in C1∼C7 excluding (C3) as C′. Conjunct with the set of weighted soft clauses O defined in Section 3.2, the problem is C′,ℛ,O, which tries to find an assignment of variables to satisfy all the hard clauses in C′∪ℛ and to maximize the sum of the weights of the satisfied soft clauses in O. Thereby, the parallel identical machine scheduling problem of maximizing the total weight of on-time tasks can be optimally solved with any off-the-shelf weighted Partial MaxSAT solver.


## 7. Conclusions and Perspective

We concentrated on a Weight Partial MaxSAT (WPM) formulation for optimal scheduling in overloaded situations. The aim is to maximize the (weighted) number of on-time tasks. Motivated by the WPM feature that distinguishes between hard clauses and weighted soft clauses, we encoded the properties of tasks as hard clauses and the goal of completing tasks on time as a set of weighted soft clauses. Then an off-the-shelf WPM solver was employed to satisfy all the hard clauses and maximize the total weight of the satisfied soft clauses. From the output of the WPM solver, the optimal schedule can be obtained.The WPM formulation’s performance was compared with that of the recent SMT and Partial MaxSAT (PM) formulations. First, we compared the performance of WPM and SMT, demonstrating that WPM is significantly superior to SMT. Then, we considered a special case where WPM and PM formulations are directly comparable. Results indicate that the WPM formulation achieves more compact encoding and higher efficiency than PM. Finally, we applied the WPM formulation to parallel identical machines with very little modification, highlighting the flexibility and scalability of the encoding.The restricted preemptive scheduling model considered in this paper is built upon earlier works [33, 38, 39], where each task is split into several nonpreemptive fragments, and preemptions can only take place at the fragments’ boundaries. This preemptive model with fixed points is too rigid to apply in many practical systems. Our future work is to design exact methods to adapt to variations of preemptive models. One example is to execute tasks continuously without interruption for at least a certain portion of time [42–44]. Instead of splitting tasks into fragments in advance, this restricted preemptive model only guarantees the minimum “granularity” of preemption without predefined subtasks and thus is more suitable for real-world applications.



---

*Source: 9615463-2021-07-16.xml*