Scheduling Theory

Motivation

Many production and computing systems run jobs on parallel machines that also draw on a shared, limited resource: tools, workers, memory, power. Adding such a resource to a scheduling problem can change its complexity entirely. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan by a resource field $res\lambda\sigma\rho$, and determined the complexity of every problem with unit-time jobs on identical or uniform machines under the makespan criterion. Their Fig. 2 separates the maximal polynomially solvable cases from the minimal NP-hard ones.

This mission formalizes the polynomial side. Two identical machines are easy under arbitrary resources (Theorem 1, due to Garey and Johnson, via maximum matching). Three identical machines with one resource are NP-hard in the strong sense (Theorem 4), and so are two uniform machines with unit resources (Theorem 3). What remains for uniform machines is settled by two algorithms: a sorting-and-shifting procedure for two uniform machines with one resource of arbitrary size (Theorem 5), and a bottleneck transportation problem for any number of uniform machines with one resource and 0–1 requirements (Theorem 6). The hardness results are the subject of the companion missions I and II.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Machine $M_i$ has speed $q_i>0$; every job has unit execution requirement, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) have $q_i=1$; uniform machines ($Q$) have arbitrary speeds. There are $l$ resources $R_h$ with positive integer sizes $s_h$, and job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. The field $res\lambda\sigma\rho$ records restrictions: $\lambda$ bounds the number of resources, $\sigma$ their sizes, $\rho$ the requirements, a dot meaning "part of the input". So $res1{\cdot}{\cdot}$ is one resource with arbitrary size and requirements, and $res1{\cdot}1$ is one resource with requirements in $\{0,1\}$.

A schedule gives every job a machine $\mu(j)$ and a start time $S_j\ge0$; the job is executed during $[S_j,C_j)$ with $C_j=S_j+1/q_{\mu(j)}$. It is feasible if jobs on the same machine do not overlap and, at every time $t$, the jobs executed at $t$ use at most $s_h$ of each resource $R_h$. The makespan is $C_{\max}=\max_j C_j$. No precedence constraints occur in this mission.

Formalization targets

Goal: Theorem 5, correctness of the algorithm

For $Q2\mid res1{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ with $q_1\ge q_2$: put all jobs on $M_1$ in order of nonincreasing $r_{1j}$, then repeatedly move the last job of $M_1$ to the earliest feasible time on $M_2$ after the jobs already there, as long as this strictly reduces $C_{\max}$. For every order with nonincreasing requirements, the resulting schedule $A$ is feasible and

$$C_{\max}(A)\le C_{\max}(\sigma)\quad\text{for every feasible schedule }\sigma.$$

Milestones for the goal

The paper's proof has two steps, both milestones. Call a schedule an (a)–(c) schedule when (a) $M_1$ runs its jobs back to back from time $0$ in nonincreasing $r_{1j}$, (b) $M_2$ runs its jobs in nondecreasing $r_{1k}$, and (c) every requirement on $M_1$ is at least every requirement on $M_2$.

1. The algorithm's schedule is feasible, is an (a)–(c) schedule, and is best among feasible (a)–(c) schedules.
2. Every feasible schedule can be transformed into a feasible (a)–(c) schedule with no larger $C_{\max}$.

Further results

• Theorem 1. For $P2\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$, with $G$ the graph joining two jobs when they can run together and $S$ a maximum matching of $G$, the optimal makespan is $n-|S|$.
• Theorem 6. For $Q\mid res1{\cdot}1,\,p_j=1\mid C_{\max}$ with the $s_1$ fastest machines listed first, the optimal makespan equals the optimal value of a bottleneck transportation problem that assigns jobs to slots (machine, position) with cost $k/q_i$, resource jobs only to the $s_1$ fastest machines.

Significance

Theorems 5 and 6 complete the classification of Fig. 2 for uniform machines: every special case of $Q\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ not covered by the hardness theorems has a polynomial algorithm. Theorem 1 is the classical reduction of two-machine resource scheduling to maximum matching, the model case for later work on scheduling with conflict graphs.

The paper proves these results briefly: "clearly" for the first half of Theorem 5, "obviously" for Theorem 1, and a one-paragraph model for Theorem 6. The exchange argument of Theorem 5 is presented "in an informal way" through five steps that pass through fractional, preempted jobs. A machine-checked proof makes these arguments exact on a model with real start times. No formalization of these results is known, and the platform had no statement about resource-constrained scheduling on uniform machines before this mission.

Difficulty

With $q_1\ne q_2$ the job boundaries on the two machines are misaligned: a job on $M_2$ overlaps parts of several jobs on $M_1$, so the resource check cannot be done slot by slot, and discrete reasoning on integer time grids does not apply. The exchange argument of Theorem 5 must control the resource usage at every real time while jobs are moved between machines and reordered, and it has to end with a nonpreemptive schedule even though the paper's intermediate steps split jobs. For Theorem 1, the hard direction is the lower bound: a feasible schedule with arbitrary real start times must be converted into a matching, which is a statement about how unit jobs on two machines can overlap. For Theorem 6, one must show that restricting resource jobs to the fastest machines and to back-to-back positions loses nothing.

Formalization scope

• Model. Jobs, machines and resources are Fin n, Fin m, Fin l (0-based). Speeds are positive reals, sizes positive naturals, requirements naturals. Start times are nonnegative reals, execution intervals are half-open, and the resource constraint is checked at every real time. $C_{\max}=0$ for $n=0$. The model carries a precedence digraph for consistency with the companion missions; every statement here assumes it has no arcs.
• Implicit hypothesis. Theorems 1 and 5 assume every job fits alone ($r_{hj}\le s_h$), which the paper leaves unstated; without it no feasible schedule exists.
• The algorithm is a Lean definition following the page: the order is an argument (any nonincreasing order), "as early as possible" is the earliest start after $M_2$'s last job at which the resource constraint holds throughout, and the loop stops at the first move that does not strictly reduce $C_{\max}$.
• Optimality is always stated in full: feasibility plus a lower bound against every feasible schedule. No minimum is written as an infimum of a possibly empty set.
• Theorem 6 is stated with 0–1 slot assignments, the interpretation the paper gives to $x_{ijk}$; the page's constraint $\sum_{k=1}^{m}$ is read as $\sum_{k=1}^{n}$.
• Not formalized: the running times $O(ln^2+n^{5/2})$ (Theorem 1), $O(n\log n)$ (Theorem 5, including the phrase "This O(n log n) algorithm") and $O(n^3)$ (Theorem 6), which depend on a machine model the paper does not fix and, for Theorems 1 and 6, on cited matching and transportation algorithms.
• Ruled out: a formalization of the goal that proves optimality only against (a)–(c) schedules, against schedules with integer start times, or for one fixed tie-breaking order proves less than Theorem 5.

Contributions welcome: lemmas about step functions of resource usage on half-open intervals, a left-shifting lemma for unit-time schedules on two machines, and the exchange steps of Theorem 5 as separate lemmas.

Selected references

• J. Błażewicz, J.K. Lenstra, A.H.G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M.R. Garey, D.S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Even, O. Kariv, An O(n^{2.5}) algorithm for maximum matching in general graphs, Proc. 16th IEEE FOCS (1975) 100–112. https://doi.org/10.1109/SFCS.1975.23

Motivation

A jobshop is a factory in which each job visits a sequence of machine groups, the sequence differing from job to job. J. R. Jackson's 1963 paper Jobshop-Like Queueing Systems (Management Science 10(1), 131–142) models such a shop as a network of queues and computes its long-run distribution of queue lengths in closed form. It generalizes his 1957 paper Networks of Waiting Lines (Operations Research 5(4)), which treated Poisson arrivals and multi-server centers, to arrival rates that depend on the total number of customers present and service rates that depend arbitrarily on the local queue length. The resulting product-form equilibrium is the starting point of queueing-network theory, which is used in performance analysis of manufacturing systems, computer systems and communication networks.

Timeline:

• 1957: Jackson, Networks of Waiting Lines, constant external Poisson arrivals and multi-channel exponential servers; product-form equilibrium.
• 1963: Jackson, this paper: state-dependent total arrival rate $\lambda(S(\bar k))$, queue-length-dependent service rates $\mu(n, k)$, routings with self-loops and empty routings; Theorem (4.5).
• 1967: Gordon and Newell, Closed Queuing Systems with Exponential Servers, the closed-network analogue.
• 1979: Kelly, Reversibility and Stochastic Networks, the general theory of migration processes and partial balance.

Setting

There are $N \ge 1$ service centers, Center $1, \dots, N$. A state vector $\bar k = (k_1, \dots, k_N)$ has non-negative integer components, $k_n$ being the number of customers at Center $n$, and $S(\bar k) = k_1 + \dots + k_N$. The system $(N, L, M, R)$ is given by:

1. arrival rates $\lambda(K)$, $K = 0, 1, 2, \dots$: in state $\bar k$ a customer arrives at rate $\lambda(S(\bar k))$;
2. service rates $\mu(n, k)$: a service at Center $n$ completes at rate $\mu(n, k_n)$;
3. routing probabilities $r(m, n)$, $m \in [0, N]$, $n \in [1, N+1]$: an arriving customer's first center is $n$ with probability $r(0, n)$, its routing is empty with probability $r(0, N+1)$; after service at Center $m$ it moves to Center $n$ with probability $r(m, n)$ (possibly $n = m$) or leaves with probability $r(m, N+1)$.

The paper's standing Assumptions (2.1)–(2.4): (2.1) either all $\lambda(K) > 0$, or $\lambda(K) > 0$ exactly for $K \le K_0$; (2.2) $\mu(n, 0) = 0$ and $\mu(n, k) > 0$ for $k \ge 1$; (2.3) each row $\{r(m, n)\}_{n \in [1, N+1]}$ is a probability distribution; (2.4) the traffic equations

$$e(n) = r(0, n) + \sum_{m=1}^N e(m)\, r(m, n), \qquad n \in [1, N], \tag{2.5}$$

have a unique solution, and it is non-negative.

The process is defined by its transition probabilities over a short interval (p. 134), from which the paper derives the balance equations (3.1) for $P(\bar k, t)$. An equilibrium state probability distribution is a probability distribution $p$ on state vectors such that $P(\bar k, t) \equiv p(\bar k)$ solves (3.1). With

$$W(K) = \prod_{i=0}^{K-1}\lambda(i), \quad w(\bar k) = \prod_{n=1}^N\prod_{i=1}^{k_n}\frac{e(n)}{\mu(n, i)}, \quad T(K) = \sum_{S(\bar k) = K} w(\bar k),$$

the constant $\pi$ is $\{\sum_{K \ge 0} W(K) T(K)\}^{-1}$ when the series converges and $0$ otherwise.

Formalization targets

Goal: Theorem (4.5)

If $\pi > 0$, then

$$p(\bar k) = \pi\, w(\bar k)\, W(S(\bar k)) \tag{4.6}$$

is an equilibrium state probability distribution; and if the arrival rates are bounded, it is the only one. The goal fixes no constants; the condition $\pi > 0$ is the paper's.

Milestones

1. The series in (4.4) converges to a positive number or diverges to $+\infty$ (§4, p. 136).
2. If $\pi > 0$, (4.6) is a probability distribution (first claim of the proof sentence, p. 136).
3. (4.6) satisfies equations (3.1) at every state (second claim, p. 136).
4. Under bounded arrival rates, an equilibrium distribution is unique (§4, p. 135).

Companion

Theorem (6.3) in its case $K^* = 0$, $k_n^* = +\infty$: with constant arrival rate $\lambda(K) \equiv \lambda(0)$ and $p_n(0) > 0$ for every $n$, the equilibrium is $p(\bar k) = \prod_n p_n(k_n)$, $p_n$ being the normalized $w_n(k) = \prod_{i=1}^k \lambda(0)e(n)/\mu(n, i)$.

Significance

Theorem (4.5) states that the queue lengths of a whole network have an explicit stationary law, determined by the routing only through the visit ratios $e(n)$, and that conditionally on the total $S(\bar k) = K$ it does not depend on the arrival process. With constant arrival rate it factorizes into independent one-center laws (Theorem (6.3)), each that of a single queue fed at rate $\lambda(0)e(n)$; this is the form in which Jackson networks enter textbooks. State-dependent arrivals cover systems with balking or finite capacity: taking $\lambda(K) = 0$ for $K > K_0$ caps the population.

The result is classical and proved; it has no machine-checked proof on this platform. The platform has Kelly–Yudovina's open migration process (KellyStochasticNetworks.open_migration_equilibrium): constant external arrivals, no self-loops, a full-balance conclusion without uniqueness. It is the companion (6.3) in substance but not the general theorem: arrival rates depending on the total population are not in it. This mission contributes the state-dependent model, a stationary form of Jackson's own equations (3.1), and a uniqueness statement.

Difficulty

The balance equations are an infinite system in $\mathbb{Z}_{\ge 0}^N$. Substituting (4.6) gives terms with shifted states, guarded by non-negativity of components, a double sum over ordered pairs of distinct centers, self-loops appearing only in the outflow factor $1 - r(n, n)$, and centers with $e(n) = 0$, where $w$ vanishes. Checking each state term by term against the traffic equations requires the diagonal of (2.5), excluded in (3.1), to be handled exactly. Summing (4.6) to one requires regrouping a series over $\mathbb{Z}_{\ge 0}^N$ by the finite fibres of $S$.

Uniqueness is the hard part. The paper gives no proof: footnote 5 refers to a limit theorem for Markov processes and to the communication structure of non-transient states. A solution of the algebraic balance equations need not be the stationary law of the process when the process can explode, and the model allows explosion with $\pi > 0$ (e.g. $N = 1$, $\lambda(K) = 4^K$, $\mu(1,k) = 2\cdot 4^{k-1}$). Uniqueness therefore depends on non-explosion as well as on the communication structure of the states, and neither is addressed on the page.

Formalization scope

Centers are Fin N with $N > 0$; states are Fin N → ℕ; rates are real. The routing is one function r : Option (Fin N) → Option (Fin N) → ℝ, where none is the index $0$ in the first argument and $N + 1$ in the second. A structure JobshopSystem N bundles $\lambda, \mu, r, e$ with Assumptions (2.1)–(2.4) as fields; $e$ is a parameter satisfying (2.5), uniqueness and non-negativity, not a formula. Balance sys q k is the stationary equation (3.1) at k for an arbitrary q, and IsEquilibrium sys q is $q \ge 0$, HasSum q 1, and Balance at every state. $\pi$ is defined with an explicit if Summable … then … else 0.

Explicit choices, each stated in the item where it applies:

• Correction of (3.1). The paper prints the arrival outflow as $\lambda(S(\bar k))$:

  $\dfrac{dP(\bar k, t)}{dt} = -[\lambda(S(\bar k)) + \sum_n \mu(n, k_n)(1 - r(n, n))]P(\bar k, t) + \dots$

  Its transition probabilities (p. 134) give $\lambda(S(\bar k))\sum_{n=1}^N r(0, n)$, since an arrival with an empty routing leaves the state unchanged. The two agree only when $r(0, N+1) = 0$, and with the printed coefficient Theorem (4.5) is false ($N = 1$, $r(0,1) = r(0,2) = 1/2$, $r(1,2) = 1$, constant rates, at $\bar k = 0$). The formalization uses the coefficient the transition probabilities give. It does not assume $r(0, N+1) = 0$: the paper allows empty routings.

• Uniqueness under bounded arrival rates. Uniqueness (milestone 4 and the goal's second conjunct) assumes $\exists \Lambda,\ \forall K,\ \lambda(K) \le \Lambda$. The paper asserts uniqueness without proof, citing a limit theorem for regular processes; bounded arrival rates make the process regular and hold for every example in the paper. Existence and the formula carry no added hypothesis.

• Companion (6.3). System $(N, L, M, R)^*$ of §5 is not formalized in the paper and not here; only its case $K^* = 0$, $k_n^* = +\infty$ is stated.

A trivializing formalization is ruled out: Balance and IsEquilibrium are stated for an arbitrary function on states and never mention $w$, $W$ or $\pi$, and equilibrium is neither defined as (4.6) nor as detailed or partial balance.

Useful infrastructure: summation over Fin N → ℕ grouped by total (Finset.Nat.antidiagonalTuple), and a non-explosion and uniqueness theory for countable-state continuous-time chains, which is reusable beyond this mission. Not included: the limit $\lim_{t\to\infty} P(\bar k, t) = p(\bar k)$, which needs a construction of the process; the equivalence of (2.4) with finiteness of routings; Theorem (5.5) and (5.7)–(5.9).

Selected references

• J. R. Jackson, Jobshop-Like Queueing Systems, Management Science 10(1), 131–142, 1963. https://doi.org/10.1287/mnsc.10.1.131
• J. R. Jackson, Networks of Waiting Lines, Operations Research 5(4), 518–521, 1957. https://doi.org/10.1287/opre.5.4.518
• W. J. Gordon and G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2), 254–265, 1967. https://doi.org/10.1287/opre.15.2.254
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/book/whole.pdf
• A. T. Bharucha-Reid, Elements of the Theory of Markov Processes and Their Applications, McGraw-Hill, 1960 (Theorem 2.9, p. 102, cited in footnote 5).

Motivation

Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below $3/2$ unless P = NP; closing the gap between $3/2$ and $2$ has been open since.

The restricted assignment problem is the special case in which every job $j$ has a single size $p_j$ and may only run on a given set $\Gamma(j)$ of machines. The $3/2$ hardness already holds here, and the best known algorithms were still $2$-approximations. Every linear program previously used for the problem has integrality gap $2$, so a better LP lower bound was the natural target.

Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most $33/17 \approx 1.9412$. Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than $2$.

• 1990: Lenstra, Shmoys, Tardos, 2-approximation for unrelated machines, and $3/2$ hardness already for restricted assignment.
• 2006: Bansal and Sviridenko introduce the configuration LP for the max–min variant (the Santa Claus problem).
• 2008: Feige shows the configuration LP has constant integrality gap for restricted Santa Claus, and Asadpour, Feige and Saberi (2008) give a local search proof of a factor-4 gap.
• 2011: Svensson adapts that local search to makespan and proves the gap $33/17$ for restricted assignment (arXiv:1011.1168).

Setting

An instance consists of finite sets $J$ (jobs) and $M$ (machines), sizes $p_j \ge 0$, and for each job a set $\Gamma(j) \subseteq M$. A schedule is a map $\sigma : J \to M$ with $\sigma(j) \in \Gamma(j)$. The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$, and the makespan is the largest load. $\mathrm{OPT}$ is the least makespan of a schedule.

For a target makespan $T$, a configuration for machine $i$ is a set $C \subseteq J$ of jobs that may all run on $i$ ($i \in \Gamma(j)$ for $j \in C$) with $p(C) = \sum_{j \in C} p_j \le T$. Write $\mathcal C(i,T)$ for the set of configurations. The configuration LP asks for $x_{i,C} \ge 0$ with

$$\text{[C-LP]}\qquad \sum_{C \in \mathcal C(i,T)} x_{i,C} \le 1 \quad (i \in M), \qquad \sum_{i \in M}\ \sum_{C \in \mathcal C(i,T),\ C \ni j} x_{i,C} \ge 1 \quad (j \in J).$$

Its dual has variables $y_i, z_j \ge 0$ and constraints $y_i \ge \sum_{j \in C} z_j$ for all $i$ and $C \in \mathcal C(i,T)$. $\mathrm{OPT}_{LP}$ is the least $T$ at which [C-LP] is feasible, and $\mathrm{OPT}_{LP} \le \mathrm{OPT}$.

In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.

Formalization targets

Goal: Theorem 4.1

For every instance with $p \ge 0$ and every $T \ge 0$,

$$\text{[C-LP] feasible at } T \ \Longrightarrow\ \exists\, \sigma : J \to M,\ \ \sigma(j) \in \Gamma(j)\ \forall j,\quad \sum_{j : \sigma(j) = i} p_j \le \tfrac{33}{17}\, T \ \ \forall i .$$

Equivalently $\mathrm{OPT} \le \tfrac{33}{17}\,\mathrm{OPT}_{LP}$. The statement is scale-free and does not define $\mathrm{OPT}_{LP}$.

Milestones

The milestones follow the paper's proof, which normalizes $\mathrm{OPT}_{LP} = 1$ and sets $R = 16/17$:

1. a dual solution with $\sum_i y_i < \sum_j z_j$ makes [C-LP] infeasible;
2. the local search, Algorithm 2 (ExtendSchedule), keeps its partial schedule valid (load at most $1 + R$, at most one big job per machine);
3. when the algorithm has no potential move, an explicit pair $(y^*, z^*)$ is dual feasible (Claim 4.7) and has $\sum y^* < \sum z^*$ (Claim 4.8);
4. hence, if [C-LP] is feasible, a potential move always exists (Lemma 4.6);
5. the algorithm has no infinite run (Lemma 4.9);
6. [C-LP] feasible at $T = 1$ gives a schedule of makespan at most $1 + 16/17$.

Three facts from Section 2 complete the list: normalization by scaling, $\mathrm{OPT}_{LP} \le \mathrm{OPT}$, and monotonicity of feasibility in $T$.

Significance

The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor-$2$ algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within $33/17 + \epsilon$. The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to $11/6$ (Jansen and Rohwedder, 2017) along the same lines.

The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:

• a reusable definition of the configuration LP and its dual certificate;
• a precise, nondeterministic model of a local search whose termination rests on a lexicographic potential;
• a check of a proof that has many cases. The formalization already exposed two edge cases:
  • Claim 4.8 fails when $j_{\mathrm{new}}$ has size $0$ and no admissible machine;
  • the termination proof needs positive job sizes. With a job of size $0$, the algorithm can move it back and forth between two tied machines forever.

The milestones are stated with the corresponding hypotheses.

Difficulty

The obvious approach, rounding a fractional configuration solution, loses a factor $2$. If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.

The milestones along the paper's route are hard for two reasons. First, the dual pair $(y^*, z^*)$ rounds job sizes down by class (big to $11/17$, medium to $9/17$). Proving $\sum y^* < \sum z^*$ requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.

Formalization scope

Jobs and machines are finite types with decidable equality, sizes are real numbers with $p_j \ge 0$, and admissible machines are a Finset per job. Schedules are total maps $J \to M$ with $\sigma(j) \in \Gamma(j)$ stated explicitly. Partial schedules are maps $J \to$ Option M. Constants are exact rationals in $\mathbb R$. Values of moves live in Lex (ℝ × ℝ).

Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.

Three statements would trivialize the goal, and the formalization rules them out:

• a schedule allowed to use machines outside $\Gamma(j)$;
• a target $T < 0$;
• an LP missing either constraint row.

Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.

Useful contributions include:

• the weak-duality certificate;
• the scaling and monotonicity facts;
• the invariants of reachable states (each job lies in at most one blocker, blockers on a machine are never reassigned while present);
• the two claims and the termination argument.

The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.

Selected references

• O. Svensson, Santa Claus Schedules Jobs on Unrelated Machines, arXiv:1011.1168v2, 2011; SIAM J. Comput. 41(5), 2012. https://arxiv.org/abs/1011.1168
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Math. Programming 46, 1990. https://doi.org/10.1007/BF01585745
• N. Bansal, M. Sviridenko, The Santa Claus problem, STOC 2006. https://doi.org/10.1145/1132516.1132522
• A. Asadpour, U. Feige, A. Saberi, Santa Claus meets hypergraph matchings, APPROX 2008; ACM Trans. Algorithms 8(3), 2012. https://doi.org/10.1145/2229163.2229168
• K. Jansen, L. Rohwedder, On the configuration-LP of the restricted assignment problem, SODA 2017. https://arxiv.org/abs/1611.01934

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project so that prescribed time lags between activities are respected and, at every moment, the activities in progress do not require more of any renewable resource (staff, machines, reactors) than is available. When the time lags include maximum time lags (deadlines relative to other activities), even finding a feasible schedule is NP-hard, and the feasible region is in general neither convex nor connected. Branch-and-bound methods for this problem (the problem $PS|temp|C_{\max}$ in the notation of Neumann, Schwindt & Zimmermann) do not search over schedules directly. They search over strict orders of the activities, that is, over sets of precedence constraints "$j$ starts after $i$ has finished".

This mission formalizes the theory behind that search, as developed by Bartusch, Möhring & Radermacher (1988) and presented in §2.3 of Neumann, Schwindt & Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). Its goal, Theorem 2.3.10, says when a strict order resolves every resource conflict.

Setting

A project has activities $V = \{0, 1, \dots, n+1\}$, where $0$ and $n+1$ are fictitious activities marking the project's start and completion and $1, \dots, n$ are the real activities ($n \ge 1$). Activity $i$ has duration $p_i \in \mathbb Z_{\ge 0}$, with $p_0 = p_{n+1} = 0$ and $p_i > 0$ for real activities. Time lags are encoded in the project network $N$: an arc $\langle i, j\rangle \in E$ with integer weight $\delta_{ij}$ imposes $S_j - S_i \ge \delta_{ij}$. The book's standing assumptions give, for every node $i$, a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$.

A schedule is a vector $S \in \mathbb R^{n+2}$ with $S_0 = 0$ and $S_i \ge 0$. It is time-feasible if $S_j - S_i \ge \delta_{ij}$ for all arcs. The set of time-feasible schedules is $\mathcal S_T$.

Each renewable resource $k \in \mathcal R$ has a capacity $R_k$, and activity $i$ uses $r_{ik} \le R_k$ units of it while in progress, with $r_{0k} = r_{n+1,k} = 0$. The active set at time $t$ is $\mathcal A(S,t) = \{ i \mid S_i \le t < S_i + p_i\}$, and $S$ is resource-feasible if $\sum_{i \in \mathcal A(S,t)} r_{ik} \le R_k$ for all $k$ and all $t \ge 0$. The feasible region $\mathcal S$ consists of the schedules that are both time-feasible and resource-feasible.

A strict order $O \subseteq V \times V$ is an asymmetric, transitive relation. Its order polyhedron is

$$\mathcal S_T(O) = \{ S \in \mathcal S_T \mid S_j \ge S_i + p_i \ \text{for all } (i,j) \in O\}.$$

$O$ is time-feasible if $\mathcal S_T(O) \ne \emptyset$, and feasible if moreover $\mathcal S_T(O) \subseteq \mathcal S$. The order network $N(O)$ adds to $N$, for each $(i,j) \in O$, an arc $\langle i,j\rangle$ of weight $p_i$, or raises the weight of an existing arc to $\max(\delta_{ij}, p_i)$. A schedule $S$ induces the strict order $O(S) = \{(i,j) \mid i \ne j,\ S_j \ge S_i + p_i\}$.

A set $F \subseteq V$ is forbidden if $\sum_{i \in F} r_{ik} > R_k$ for some resource $k$. It is a minimal forbidden set if no proper subset of it is forbidden. $\mathcal F$ denotes the set of minimal forbidden sets.

Formalization targets

Goal: Theorem 2.3.10 (Bartusch et al. 1988)

For every time-feasible strict order $O$,

$$O \text{ feasible} \iff \forall F \in \mathcal F\ \exists\, i, j \in F:\ N(O) \text{ has a path from } i \text{ to } j \text{ of length} \ge p_i .$$

Milestones

1. Proposition 2.3.3. A strict order $O$ is time-feasible if and only if $N(O)$ has no cycle of positive length.
2. Bartusch et al.'s criterion (quoted in the proof of Theorem 2.3.10). A schedule $S$ is resource-feasible if and only if every $F \in \mathcal F$ contains distinct $i, j$ with $S_j \ge S_i + p_i$.
3. Proposition 2.3.6. For time-feasible $S$, the strict order $O(S)$ is feasible if and only if $S \in \mathcal S$.
4. Theorem 2.3.7. $\mathcal S = \bigcup_{O \in \mathcal O} \mathcal S_T(O)$, where $\mathcal O$ is the finite set of inclusion-minimal feasible strict orders.
5. Remark 2.3.11. A time-feasible schedule partitions $F$ if and only if every $\mathcal A(S,t) \cap F$, $t \ge 0$, is feasible. A time-feasible order is feasible if and only if it breaks up all (equivalently, all minimal) forbidden sets. A time-feasible schedule is feasible if and only if it partitions all forbidden sets.

Significance

Theorem 2.3.10 turns the feasibility of a strict order, which is a statement about infinitely many schedules and all times $t$, into a finite check: one longest-path computation in $N(O)$ for each minimal forbidden set. Together with Proposition 2.3.3 and the structural Theorem 2.3.7, it shows that $\mathcal S$ is a finite union of polyhedra indexed by feasible strict orders. This justifies the enumeration schemes of Chapter 2 of the book (branching on the pairs that break up a minimal forbidden set) and the notions of active and stable schedules developed in later sections.

All results in this mission are proved in the literature. For the resource-feasibility criterion, the book cites Bartusch et al. (1988) instead of proving it. To our knowledge, none of these results has been machine-checked. A formal development would give a verified foundation for the order-based description of the feasible region, on which later missions of this series (active schedules, delaying modes, stable schedules) build.

Difficulty

The sufficiency half of the goal is short once the criterion is available: a path of length $\ge p_i$ in $N(O)$ forces $S_j \ge S_i + p_i$ on the whole order polyhedron. The necessity half carries the content. If for some minimal forbidden set $F$ no path in $N(O)$ between elements of $F$ reaches the required length, one must construct a schedule in $\mathcal S_T(O)$ in which all activities of $F$ are simultaneously in progress. This means adding the reverse constraints $S_j - S_i < p_i$ for all $i, j \in F$ to the temporal system without creating a cycle of positive length, while keeping $S_0 = 0$ and $S \ge 0$. The obvious reading "no single arc gives a precedence, so they can overlap" fails because maximum time lags combine into long paths through activities outside $F$. The standing assumption that every node is reachable from $0$ by a path of nonnegative length is needed here: without it the equivalence is false.

Formalization scope

• The activity set is Fin (n + 2): 0 is the project start and Fin.last (n + 1) the project completion. Durations and resource data are natural numbers, arc weights are integers, and start times are real numbers.
• Strict orders are finite sets of pairs, Finset (Fin (n+2) × Fin (n+2)), required to be asymmetric and transitive.
• Resource constraints hold for every $t \ge 0$. The book's (2.1.4) writes $0 \le t \le \bar d$. In Chapter 2 schedules are not bounded by $\bar d$, and the book's proofs and Remark 2.3.11 use all $t \ge 0$. This is a convention of the whole series, not a strengthening.
• A path is a walk (nodes may repeat) and its length is the sum of its arc weights. A cycle of positive length is a closed walk with at least one arc and positive length. For a time-feasible order, $N(O)$ has no cycle of positive length. In that case "some path of length $\ge p_i$" coincides with the book's "longest path length $\ge p_i$", so no supremum over paths appears.
• The standing assumptions of the book form a single predicate Project.StandingAssumptions, which is a hypothesis of every theorem: $n \ge 1$; $p_0 = p_{n+1} = 0$ and $p_i > 0$ otherwise; no loops; $r_{0k} = r_{n+1,k} = 0$ and $r_{ik} \le R_k$; and the two path conditions of p. 8.
• Minimal forbidden sets and inclusion-minimal feasible orders use Mathlib's Minimal, taken among forbidden sets and among feasible strict orders respectively.
• The goal is an equivalence, and both directions are required. Weakening it to sufficiency, or dropping the time-feasibility of $O$ or the minimality of $F$, would change the theorem. Keeping the book's cut-off $t \le \bar d$ would also change it, because a schedule could then have an unresolved conflict after $\bar d$ and still be called feasible.
• Theorem 1.3.3 of Chapter 1 (a time-feasible schedule exists if and only if the network has no cycle of positive length) is needed for Proposition 2.3.3 and is restated here for $N(O)$. Chapter 1's mission is drafted separately.
• Useful infrastructure beyond this mission: longest-path potentials on integer-weighted digraphs without positive cycles (feasibility of difference constraints), and the walk and cycle API on Network. Contributions of this general lemma layer are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745

Motivation

Resource-constrained project scheduling with minimum and maximum time lags is the model behind make-to-order production, process-industry batch planning and large engineering projects. When the objective is the project duration or another regular function (nondecreasing in every start time), an optimum can be found among schedules that cannot be shifted to the left. Many objectives in practice are nonregular: net present value, earliness–tardiness costs, resource levelling and resource investment. For these, delaying an activity can pay, and "shift as far left as possible" no longer identifies a finite set of candidate schedules.

Neumann, Nübel and Schwindt (Math. Methods Oper. Res. 52, 2000) answered this with classes of schedules defined by the absence of pairs of opposite shifts: stable, semistable, pseudostable and quasistable schedules, the mirror image of active, semiactive, pseudoactive and quasiactive schedules. Section 3.2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), shows that these classes are exactly the extreme points of the feasible region and of its natural convex pieces. The classification of objective functions in §3.3, and every enumeration scheme of the later chapter, rests on that correspondence.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$. Activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. The project network $N$ has node set $V$ and arcs $\langle i,j\rangle\in E$ with integer weights $\delta_{ij}$, each encoding a temporal constraint $S_j-S_i\ge\delta_{ij}$. A prescribed deadline $\bar d\in\mathbb N$ is included as the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$. Renewable resources $k$ have capacities $R_k$, and activity $i$ uses $r_{ik}\le R_k$ units while it runs.

A schedule is a vector $S\in\mathbb R^{n+2}$ of start times. The time-feasible region $\mathcal S_T$ collects the schedules with $S_0=0$, $S\ge0$ and $S_j-S_i\ge\delta_{ij}$ on every arc; it is a polyhedron, and a polytope when every activity precedes $n+1$ as in Remarks 1.1.2. A schedule is resource-feasible if at every time $t\ge0$ the running activities $\mathcal A(S,t)=\{i\mid S_i\le t<S_i+p_i\}$ use at most $R_k$ units of every resource. The feasible region is $\mathcal S=\mathcal S_T\cap\mathcal S_R$. It is in general neither convex nor connected.

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$. For a strict order $O$, the order polytope is $\mathcal S_T(O)=\{S\in\mathcal S_T\mid S_j\ge S_i+p_i\ ((i,j)\in O)\}$. The order $O$ is feasible if $\emptyset\ne\mathcal S_T(O)\subseteq\mathcal S$. The schedule polytope of $S$ is $\mathcal S_T(O(S))$.

A shift moves a schedule $S$ to $S'\neq S$. It is global if both are feasible, local if in addition a continuous path inside $\mathcal S$ joins them, order-preserving if $O(S)\subseteq O(S')$, and order-monotone if $O(S)$ and $O(S')$ are comparable. Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$. A feasible schedule is stable, semistable, pseudostable or quasistable if no pair of opposite global, local, order-monotone or order-preserving shifts, respectively, starts at it. It is antiactive if no global right-shift starts at it.

Formalization targets

Goal: Theorem 3.2.10

For every feasible schedule $S$:

$$\begin{aligned} &\text{(a) } S\text{ antiactive}\iff S\text{ maximal in }\mathcal S, \qquad \text{(b) } S\text{ stable}\iff S\in\operatorname{ext}\mathcal S,\\ &\text{(c) } S\text{ semistable}\iff S\in\operatorname{ext}C_S,\ C_S\text{ the component of }\mathcal S\text{ containing }S,\\ &\text{(d) } S\text{ pseudostable}\iff S\in\operatorname{ext}\mathcal S_T(O)\ \text{for all feasible }O\subseteq O(S),\\ &\text{(e) } S\text{ quasistable}\iff S\in\operatorname{ext}\mathcal S_T(O(S)). \end{aligned}$$

Milestones

• Lemma 3.2.4: opposite order-preserving or order-monotone shifts can be taken uniform (all moved activities move by one common amount).
• Lemma 3.2.8: pseudostable schedules are the local extreme points of $\mathcal S$, the points on no segment that lies entirely in $\mathcal S$.
• Lemma 3.2.9: when $S$ is not pseudostable, a segment through $S$ can be found inside one order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$ feasible.
• Proposition 3.2.13: the quasistable schedules, and every class below them in Fig. 3.2.6, form finite sets.
• Proposition 3.2.16: every vertex of $\mathcal S_T$ is the unique solution of $S_0=0$, $S_j-S_i=\delta_{ij}$ on the arcs of a spanning tree of $N$; for the minimal point, an outtree rooted at $0$.
• Theorem 3.2.18: $S$ is quasistable iff it is the unique solution of such a tree system in the schedule network $N(O(S))$.
• Remark 3.2.7: every activity of a quasistable schedule is tied to another one by a tight duration or time lag, so quasistable schedules are integer-valued.

Significance

The theorem makes four shift-defined classes computable objects: extreme points of explicit polytopes, or of a finite union of them. Together with Proposition 3.2.13, it gives each class of nonregular objective functions in §3.3 a finite candidate set of schedules among which an optimum can be sought (§3.2, p. 207). Theorem 3.2.18 gives the certificate for quasistable schedules: a spanning tree of the schedule network, which the later sections use to enumerate vertices.

The results are proved in the book, except Lemma 3.2.9, whose proof is cited to Neumann, Nübel and Schwindt (2000). As far as a search of the platform shows, none of them has been formalized. A formalization supplies the missing details, among them that connected and path components of $\mathcal S$ coincide and the degenerate vertices behind the tree description. It also produces a reusable library of schedule classes on real-valued start times.

Difficulty

Part (b) is close to the definition, since a pair of opposite global shifts is a segment through $S$ with feasible endpoints. The content is elsewhere. In (c) the definition speaks of continuous trajectories and the right-hand side of connected components, so the proof needs local path-connectedness of a finite union of polytopes. In (d) the feasible region is not convex: an order-monotone shift keeps $S$ and $S'$ in a common order polytope, but $S'$ and $S''$ may lie in different ones. The segment through $S$ has to be moved into a single order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$, and that is Lemma 3.2.9. Proposition 3.2.16 and Theorem 3.2.18 need the passage from $n+2$ linearly independent tight constraints to a spanning tree. They must allow degenerate vertices, where several trees describe the same point, and must represent the nonnegativity constraints $S_i\ge0$ by arcs of the network.

Formalization scope

Activities are Fin (n + 2); start times are real vectors Fin (n + 2) → ℝ with the pointwise order. Durations, capacities and requirements are natural numbers, and time lags integers. The deadline is the arc $\langle n+1,0\rangle$ of weight $-\bar d$, which is always present, as §3.1 prescribes. Resource constraints are imposed for every $t\ge0$, not only for $0\le t\le\bar d$ as (3.1.2) writes; the proofs use the first reading. Extreme points are Mathlib's Set.extremePoints ℝ, maximal points are Maximal for the pointwise order, and components are connectedComponentIn. A local shift carries an explicit continuous map from unitInterval into $\mathcal S$. Strict orders are asymmetric, transitive relations on $V$. A spanning tree is an arc set of size $n+1$ whose underlying simple graph is connected. Its arcs must be arcs of $N$, resp. of $N(O(S))$, with their network weights, so an arbitrary equation system does not count.

The schedule classes are defined through shifts and nothing else. Defining "stable" as "extreme point", or "pseudostable" as "local extreme point", would make the goal and Lemma 3.2.8 tautologies, and such encodings are ruled out. Proposition 3.2.16 carries the book's standing convention (§1.2, p. 8) that every node is reached from $0$ by a walk of nonnegative length. Without it the statement is false.

The definitions duplicate, under this mission's namespace, the model of the book's Chapter 2 missions (order polytopes, shifts, active classes). They are written to be merged with those once published. Contributions on the geometry of finite unions of polytopes, and on spanning-tree bases of difference constraint systems, are reusable beyond this mission.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1–3.2. https://doi.org/10.1007/978-3-540-24800-2
• K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), 441–465. https://doi.org/10.1007/s001860000092
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 199–240. https://doi.org/10.1007/BF02283745

Motivation

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.

Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.

The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$; activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has a duration $p_i\in\mathbb N$, with $p_0=p_{n+1}=0$. The project network $N$ has arc set $E$; an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ on the start times. A schedule is a real vector $S=(S_i)_{i\in V}$ with $S_0=0$ and $S_i\ge0$; it is time-feasible if it meets every temporal constraint.

Cumulative resources $k\in\mathcal R^\gamma$ carry integer demands $r_{ik}$: $r_{ik}<0$ depletes $-r_{ik}$ units at the start $S_i$, $r_{ik}>0$ replenishes $r_{ik}$ units at the completion $S_i+p_i$, and $r_{0k}$ is the initial stock. The inventory at time $t$ is

$$r_k(S,t)=\sum_{i:\ r_{ik}<0,\ S_i\le t} r_{ik}+\sum_{i:\ r_{ik}>0,\ S_i+p_i\le t} r_{ik}.$$

With safety stock $\underline R_k$ and storage capacity $\overline R_k$ (integers, $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ by (2.12.1)), $S$ is feasible if it is time-feasible and $\underline R_k\le r_k(S,t)\le\overline R_k$ for every $k$ and every $t\ge0$. The decision problem of $PSc|temp|C_{\max}$ asks whether a feasible schedule exists.

For renewable resources $k\in\mathcal R$ with capacities $R_k$ and requirements $r_{ik}\in\mathbb N$, a set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$. A delaying alternative for $F$ is a set $B\subseteq F$ such that $F\setminus B$ is not forbidden; it is minimal if no proper subset of $B$ is one.

In $PS\infty|temp,\bar d|f$ there are no resources, schedules must also satisfy $S_{n+1}\le\bar d$, and the objective here is $f(S)=-\sum_{i\in V}\sum_{j>i}w_{ij}|S_j-S_i|$ with weights $w_{ij}\ge0$.

NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.

Formalization targets

Goal: Theorem 2.12.1

Assuming PARTITION is NP-complete,

$$L=\{\text{codes of instances of }PSc|temp|C_{\max}\text{ with a feasible schedule}\}\ \text{ and }\ L_{\mathrm{acyc}}=L\cap\{N\text{ acyclic}\}$$

are both NP-complete.

Milestones

1. Membership (proof of Theorem 2.12.1): $L\in\mathrm{NP}$ and $L_{\mathrm{acyc}}\in\mathrm{NP}$.
2. Reduction correctness (proof of Theorem 2.12.1): for sizes $s(1),\dots,s(\nu)$ with even sum, the project with $r_0=r_{n+1}=-\sum s(i)/2$, $r_i=s(i)$, $\underline R=\overline R=0$, $d^{\min}_{0,n+1}=1$ has an acyclic network, and it has a feasible schedule iff the sizes split into two parts of equal sum.
3. Polynomial transformation: $\mathrm{PARTITION}\le_p L_{\mathrm{acyc}}$.
4. Proof of Proposition 2.5.4, one resource: for $j^*\in B\subseteq F$, $B$ is a minimal delaying alternative iff $R-\min_{j\in B}r_j<\sum_{i\in F\setminus B}r_i\le R$.
5. Proof of Proposition 2.5.4, with $r_{j^*}=1$: a minimal delaying alternative contains $j^*$ iff some $A\subseteq F\setminus\{j^*\}$ has $\sum_{i\in A}r_i=R$.
6. Proposition 2.5.4: assuming SUBSET SUM is NP-complete, deciding whether some minimal delaying alternative for a forbidden set $F$ contains $j^*\in F$ is NP-complete.
7. Proof of Proposition 3.4.2: a graph has a cut of at least $M$ edges iff the constructed instance has a schedule with $S_i\in\{0,1\}$ and $\sum_{i<j}w_{ij}|S_j-S_i|\ge M$.
8. Proposition 3.4.2: assuming SIMPLE MAX CUT is NP-complete, the decision version of $PS\infty|temp,\bar d|-\sum\sum w_{ij}|S_j-S_i|$ is NP-hard.

The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along $\le_p$ (on the platform as CookPvsNP.npComplete_of_polyReducible).

Significance

The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.

Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.

Difficulty

The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.

First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.

Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.

Formalization scope

The Lean development fixes the following conventions.

• Activities are Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.
• The inventory constraints hold for every $t\ge0$, not only for $0\le t\le\bar d$ as (2.12.2) is printed; the book's proofs use this reading.
• Real activities may have duration $0$ in $PSc|temp|C_{\max}$: the reduction of Theorem 2.12.1 uses only such activities.
• Instances are coded as lists of integers written in binary over the alphabet $\{0,1,-,\#\}$; arc weights are listed for every ordered pair of activities together with an arc indicator. Well-formedness (standing assumptions such as $n\ge1$, $p_0=p_{n+1}=0$, no loops, (2.12.1), $r_{ik}\le R_k$) is part of each language.
• "Acyclic" means the nodes admit a numbering increasing along every arc.
• The NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT (Karp, 1972) enters as a hypothesis of the corresponding theorem; these are not results of the book.
• Proposition 3.4.2 is stated for the decision version of the optimization problem, with natural-number weights and threshold.

A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.

A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of $\le_p$, and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. doi:10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16, 1988.
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. doi:10.1007/978-1-4684-2001-2_9
• S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. claymath.org

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$, needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$. Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$, and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

• 1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
• 1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$-competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
• 1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
• 2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$-competitive deterministic algorithm from an LP relaxation.
• 2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$, integer processing times $p_j \ge 1$ and real weights $w_j > 0$. A schedule assigns each job an integer start time $S_j$. It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$.

Delayed SWPT runs over unit time slots $[t, t+1)$. When the machine is available at time $t$, it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$. Ties go to the smaller $p_j$, then to the smaller index. If $p_j \le t$, it starts $j$ at $t$ and the machine is busy until $t + p_j$. Otherwise the machine stays idle and the rule is applied again at $t+1$. The resulting schedule is written $\pi$, or dswpt I in Lean. In particular no job starts before time $p_j$.

The proof uses three auxiliary problems:

• the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$;
• the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$, where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
• one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$.

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$.

Formalization targets

Goal: Theorem 8

$$\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.$$

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

1. $\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
2. $\pi_E$ is feasible for (E) (§3.2).
3. Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$.
4. Lemma 2. $\pi_E$ is optimal for (E).
5. Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

$$\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}$$

then $C(\pi) \le 2\,C(S)$ for every feasible $S$. 6. Inequality (1) holds for some feasible $\sigma_E$, for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$. The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

• an executable, verified-terminating definition of an online scheduling rule;
• the doubling lemma for release-date problems;
• the optimality criterion behind Lemma 2;
• the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

• Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$.
• Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
• The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$. A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
• Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$, and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

• The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
• The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

• simulation invariants for the algorithm;
• exchange and left-shift arguments for single-machine schedules;
• the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

• E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
• J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
• L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
• H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106