Scheduling Theory

Motivation

Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) asks how well a computational task can be carried out when its inputs are held by self-interested agents who may lie about them. Their test case is scheduling on unrelated machines: tasks must be assigned to agents (machines), each agent privately knows how long it needs for each task, and the planner wants to minimize the time at which the last agent finishes. The paper shows that the mechanism MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is truthful and loses a factor of at most $n$ against the optimum, and that no truthful mechanism can do better than a factor $2$. It then conjectures (Conjecture 4.9) that the factor $n$ cannot be improved by any truthful mechanism.

That conjecture became the Nisan–Ronen conjecture, one of the central questions of algorithmic mechanism design. A sequence of papers raised the general lower bound from $2$ to $1 + \sqrt 2$ (Christodoulou, Koutsoupias and Vidali), to $1 + \varphi \approx 2.618$ (Koutsoupias and Vidali) and to larger constants, and Christodoulou, Koutsoupias and Kovács (STOC 2023) finally proved the conjecture for all deterministic truthful mechanisms. In the original paper, Nisan and Ronen confirm the conjecture for two restricted classes of mechanisms, with short direct arguments. This mission concerns the second class, local mechanisms (Theorem 4.12).

Setting

There are $k$ tasks $j \in \{1, \dots, k\}$ and $n$ agents $i \in \{1, \dots, n\}$. A type vector $t$ records, for every agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks of agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j \in X} t^i_j$. The make-span of $x$ is $g(x, t) = \max_i t^i(x^i)$.

A direct mechanism $(x, p)$ asks every agent for its type, computes an allocation $x(t)$ from the declarations, and hands agent $i$ the payment $p^i(t)$. Agent $i$'s utility is $p^i(t) - t^i(x^i(t))$ measured with its true times. The mechanism is truthful if declaring the true type maximizes each agent's utility whatever the other agents declare. The allocation rule is a $c$-approximation if $g(x(t), t) \le c \cdot g(y, t)$ for every type vector $t$ and every allocation $y$.

For a truthful mechanism the payment to agent $i$ depends only on the set it receives and on the declarations $t^{-i}$ of the others (Proposition 4.4). This gives the price offered to agent $i$ for a set $X$ (Definition 12):

$$p^i(X, t^{-i}) = \begin{cases} p^i(t'^i, t^{-i}) & \text{if some } t'^i \text{ gives } x^i(t'^i, t^{-i}) = X, \\ 0 & \text{otherwise.} \end{cases}$$

A mechanism is local (Definition 14) if $p^i(X, t^{-i})$ depends only on the other agents' times $\{t^l_j : l \ne i, j \in X\}$ on the tasks of $X$. MinWork is local: its price for $X$ is $\sum_{j \in X} \min_{l \ne i} t^l_j$.

Formalization targets

Goal: Theorem 4.12

For every $n \ge 1$, every $k \ge n^2$ and every real $c < n$, no truthful local mechanism is a $c$-approximation:

$$\forall (x, p) \text{ truthful and local},\ \forall c < n:\quad \exists\, t,\ y \quad g(x(t), t) > c \cdot g(y, t).$$

The bound holds for every $c < n$, so together with MinWork it shows that $n$ is the exact best ratio for local truthful mechanisms.

Milestones

1. Proposition 4.4 (Independence). Payments depend only on the allocated set and on $t^{-i}$.
2. Proposition 4.5 (Maximization). $x^i(t)$ maximizes $p^i(X, t^{-i}) - t^i(X)$ over the sets $X$ that agent $i$ can obtain.
3. Lemma 4.13. Every type vector has type vectors arbitrarily close to it at which each agent's maximizing set is unique.
4. Claim 4.14, first step. If $x^i(t)$ is the unique maximizer, lowering agent $i$'s times on $x^i(t)$ keeps $x^i(t)$.
5. Ratio step. An allocation that gives one agent $n$ tasks of time about $1$, while every other agent's own tasks are nearly free, has make-span about $n$, while splitting those $n$ tasks gives make-span about $1$.

Significance

The result. Theorem 4.12 settles the Nisan–Ronen conjecture for a natural class of mechanisms. Locality captures the mechanisms in which the price for a bundle of tasks is set only by the competition for those tasks. It includes MinWork and, more generally, every mechanism that prices tasks separately using the other agents' bids on them. The theorem says that for this class the trivial per-task auction is already optimal, so any improvement over the ratio $n$ must use prices that depend on the other agents' times on tasks outside the bundle.

Formalizing it. The statement is not open: it follows from the 2023 proof of the Nisan–Ronen conjecture, and Nisan and Ronen's own argument is much shorter. That argument is a sketch, though. Lemma 4.13 rests on an informal measure-theoretic appeal, and the core claim relies on a maximization property stated over all sets of tasks. A machine-checked proof pins down exactly which properties of truthful mechanisms the short argument needs. None of these results is known to have been formalized. The definitions (type vectors, truthful mechanisms, prices, locality) are shared with the other missions of this series.

Difficulty

An argument that looks at one agent at a time does not go through. Changing one agent's declaration changes the prices offered to every other agent, so an allocation that is stable for one agent can shift for another. The argument needs a type vector at which every agent's choice is strict, and only then can it lower times agent by agent and follow the allocation. Producing such a type vector is Lemma 4.13. The printed argument for it applies a "for almost every type vector" statement to sets defined by the price functions of an arbitrary mechanism, which need not be measurable. A proof must therefore work without any regularity of the mechanism. A second difficulty is Definition 12's convention that a set the agent cannot obtain has price $0$. Locality constrains these zero prices too, and the argument has to account for sets that are obtainable at one type vector and not at a nearby one.

Formalization scope

Agents are Fin n, tasks Fin k. An allocation is a function Fin k → Fin n, a type vector is Fin n → Fin k → ℝ, and a mechanism is a pair of functions alloc (declarations to allocation) and pay (declarations to the payment handed to each agent). Utilities are quasi-linear. All types, declarations and misreports are positive, and every truthfulness, locality and approximation quantifier ranges over positive type vectors. The make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]).

Conventions and explicit thresholds:

• $k \ge n^2$. The theorem is printed without a bound on the number of tasks, and its proof begins "Let $k \ge n^2$". The goal carries $k \ge n^2$ as a hypothesis.
• Truthfulness is assumed. §4.3 assumes throughout that the mechanism is truthful (by the revelation principle this is no loss). The goal quantifies over all truthful local mechanisms.
• Prices use Definition 12 literally, including the value $0$ for sets the agent cannot obtain, and locality is Definition 14 applied to that price function over all sets $X$, not only single tasks. When several declarations give the same set, the price uses one chosen witness; by Proposition 4.4 the choice does not matter for truthful mechanisms.
• Proposition 4.5 is stated over the sets the agent can obtain. As printed, over all subsets, it is false for a truthful mechanism that never leaves an agent idle and pays it negative amounts. Uniqueness of maximizers (Lemma 4.13, Claim 4.14) refers to the same family.
• Lemma 4.13 uses Mathlib's norm on Fin n → Fin k → ℝ, the sup norm. No measurability of the mechanism is assumed.
• Claim 4.14 is printed at $t^i_j = 1$ with $0 < \varepsilon < 1$. The first step is stated at any type vector, with $0 < \varepsilon \le t^i_j$ on the lowered tasks.
• Running time and computability are out of scope.

Ruled-out trivializations: locality is not restricted to single tasks; the goal does not assume that maximizers are unique at every type vector (that is Lemma 4.13's conclusion at one point, not a hypothesis); and the bound holds for every $c < n$, not for some.

Needed infrastructure: finite sums over allocation fibres, sup norms on function spaces, and a genericity argument for finitely many affine functions (Lemma 4.13). The model file and the price and locality definitions are reusable in the other missions of the series. Proofs of individual milestones are welcome independently.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (pp. 876–880, basic properties of truthful mechanisms).
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested agents: the designer can pay the agents, and must choose payments so that each agent's own interest leads it to reveal what the algorithm needs. Nisan and Ronen introduced the framework with task scheduling on unrelated machines as the running example (Nisan–Ronen 2001). In the basic model, where payments depend only on what the agents declare, they showed that no truthful mechanism approximates the optimal make-span within a factor below 2, and that the natural mechanism only reaches a factor $n$.

Their Section 5 changes the information available: in a mechanism with verification the payments may also depend on the times in which the tasks were actually performed. With this extra information, an exact optimizer becomes a strongly truthful mechanism (Theorem 5.1, the Compensation-and-Bonus mechanism). Exact scheduling on unrelated machines is NP-hard, so the question is whether an approximation algorithm can take the optimizer's place. Theorem 5.6 of the paper shows that plugging a non-optimal algorithm into Compensation-and-Bonus destroys truthfulness in general. Theorem 5.9, the subject of this mission, shows that for the bounded problem a specific approximation scheme, the rounding algorithm of Horowitz and Sahni (1976), can be combined with a modified payment rule to give a truthful mechanism whose outcome is within a factor $1+\varepsilon$ of optimal.

Setting

There are $n$ agents and $k$ tasks. Agent $i$ needs time $t^i_j$ for task $j$; the vector $t = (t^i_j)$ is the type vector, and agent $i$ alone knows its row $t^i$. In the bounded scheduling problem (Definition 33) there are fixed numbers $0 < a < b$ with $a \le t^i_j \le b$ for all $i, j$, and every declaration lies in the same range. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$.

A strategy of agent $i$ has two parts: a declaration $d^i \in [a,b]^k$, and an execution, which for each decision $x$ of the mechanism specifies the actual time $\tilde t_j \ge t^i_j$ in which agent $i$ performs each task $j \in x^i$. The mechanism chooses $x = x(d)$ from the declarations alone and afterwards observes the actual times $\tilde t$. The objective is the make-span with actual times,

$$g(x,\tilde t) = \max_i \sum_{j \in x^i} \tilde t_j .$$

Agent $i$ receives a payment $p^i$ and has utility $p^i - \sum_{j \in x^i} \tilde t_j$.

The corrected time vector of agent $i$ keeps agent $i$'s actual times on its own tasks and the other agents' declarations elsewhere: $\mathrm{corr}^i(x,d,\tilde t)_j = \tilde t_j$ for $j \in x^i$ and $d^l_j$ for $j \in x^l$, $l \ne i$. For a step $\delta > 0$, $\hat r = \delta\lceil r/\delta\rceil$ rounds $r$ up to a multiple of $\delta$, and $\hat g(x,\tau) = g(x,\hat\tau)$.

The rounding mechanism (Definition 34) allocates with an algorithm that exactly solves the problem with rounded declarations $\hat d$, and pays

$$p^i = \sum_{j\in x^i}\tilde t_j \;-\; \hat g\big(x, \mathrm{corr}^i(x, d, \tilde t)\big).$$

The first term, the compensation, uses exact actual times; the second, the bonus, uses rounded quantities.

A strategy is dominant if it is a best response to every declarations and executions of the others. The mechanism is truthful if every agent has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.9 without running time

For every $\varepsilon > 0$, every $0 < \delta \le \varepsilon a$ and every allocation algorithm solving the rounded problem exactly, the rounding mechanism is truthful, and at every profile of dominant strategies from the class named in the proof (declarations with the true rounded values, executions whose rounded times equal the rounded true times),

$$g\big(x(d),\tilde t\big) \le (1+\varepsilon)\, g(y,t) \quad \text{for every allocation } y .$$

Milestones

1. The solution of the rounded problem is a $(1+\varepsilon)$-approximation: $g(x,\hat t) \le g(y,\hat t)\ \forall y$ implies $g(x,t) \le (1+\varepsilon) g(y,t)\ \forall y$.
2. After rounding, $\hat g$ is the make-span, $\hat g(x,\mathrm{corr}^*(x,d)) = g(x,\hat d)$, and each agent's utility equals its rounded bonus.
3. Every strategy with the true rounded values is dominant.
4. When all agents follow such strategies, the outcome is a $(1+\varepsilon)$-approximation.
5. Truth-telling with minimal execution is dominant; hence the mechanism is truthful.

Significance

The result shows that verification does more than make exact optimization truthful: it lets a polynomial-time approximation scheme be implemented in dominant strategies, provided the bonus is computed on the same rounded instance the algorithm optimizes. This contrasts with Theorem 5.6, where an arbitrary approximation algorithm inside Compensation-and-Bonus is not truthful, and with the factor-2 lower bound of the basic model. The principle it illustrates is that the payments must reward exactly the objective the algorithm optimizes.

The paper gives only a proof sketch. Formalizing it makes the argument's hypotheses explicit: which rounding step suffices, what the allocation algorithm must satisfy, and over which strategy profiles the approximation guarantee holds. No machine-checked version of this theorem or of the Compensation-and-Bonus argument is known to exist.

Difficulty

The sketch reduces the theorem to "arguments similar to those in 5.1", but the rounded setting departs from Theorem 5.1 in two ways. Rounding is many-to-one, so an agent's declaration and execution are pinned down only up to their rounded values, and the algorithm's optimality holds only for the rounded instance. Consequently the claim that the strategies with the true rounded values are the only dominant ones does not survive arbitrary tie-breaking: an agent that is always favoured on ties can overstate its rounded time by one step without ever losing, and two such lies at one profile can push the make-span above the $(1+\varepsilon)$ bound. The approximation guarantee therefore has to be stated for the strategy class the proof identifies, not derived from dominance alone. The remaining steps require exact bookkeeping of rounding across sums and of the corrected time vectors, which a proof sketch leaves implicit.

Formalization scope

• Agents are Fin n with [NeZero n], tasks Fin k; allocations are functions Fin k → Fin n; the make-span is a Finset.sup' over agents. Types and declarations satisfy a ≤ t i j ≤ b with 0 < a < b; actual times are only bounded below by the true times.
• roundUp δ r = δ * ⌈r / δ⌉. The statement holds for every $\delta \in (0,\varepsilon a]$, which covers the intended choice $\delta = \varepsilon a$; the paper leaves $\delta$ as "a function of $a$ and $\varepsilon$".
• The Horowitz–Sahni dynamic program is not formalized. The allocation algorithm is a parameter with the hypothesis that it solves the rounded problem exactly; ties are arbitrary, and the goal holds for every such algorithm. Running time ("polynomial time") is out of scope, and with it the role of the upper bound $b$, which is kept as part of the problem.
• An execution is a function of the decision (Definition 18). Dominance quantifies over all declarations in $[a,b]$ and all executions of the others.
• The payment uses the allocation $x(d)$ in the bonus. Definition 34 prints $x(\hat t)$; since the rounding algorithm rounds the declarations itself, $x(d)$ is the allocation actually computed. The hat on $\mathrm{corr}$ is absorbed by $\hat g$.
• The goal's approximation part is restricted to dominant profiles of the class named in the proof, because the unrestricted form (Definition 3, every dominant profile) is false for some tie-breaking rules; an explicit two-agent, one-task instance is recorded in the goal's Formalization Note.
• A formalization that measures the approximation with declared rather than actual times, lets the allocation read the true types, or states the approximation only at the truthful profile while claiming the general form, does not formalize this theorem.

Useful infrastructure: lemmas on Int.ceil rounding of finite sums and on Finset.sup' monotonicity, and a reusable model of mechanisms with verification. Proofs of the milestones in any order are welcome.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• E. Horowitz, S. Sahni, Exact and Approximate Algorithms for Scheduling Nonidentical Processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951

Motivation

Johnson's 1954 paper in Naval Research Logistics Quarterly is the starting point of machine scheduling theory. Its first section solves the two-machine flow shop: $n$ items must pass through machine 1 and then machine 2, and an explicit ordering rule minimizes the total elapsed time. Its second section treats three machines. There the problem "loses some of the nice structure of the two-stage case" (p. 65), and the general three-machine problem was later shown to be strongly NP-hard (Garey, Johnson and Sethi, 1976). Johnson nevertheless identifies a restricted case, in which the middle machine is dominated by the first (or the last), where the two-machine rule still gives an optimal schedule. That case, and the structural facts behind it, are the content of this mission.

The three-machine results are still the reference point for polynomially solvable flow shops and for lower bounds in branch-and-bound methods for the general problem.

Timeline.

• 1954: Johnson proves the two-machine rule (Theorem 1) and, for three machines, the reduction to a common ordering (Lemma 3), a closed form for the elapsed time, and optimality of the rule on $A_i + B_i$, $B_i + C_i$ when $\min A_i \ge \max B_j$ (Theorem 2), with the mirror case $\min C_i \ge \max B_j$ asserted.
• 1976: Garey, Johnson and Sethi show that minimizing makespan in a three-machine flow shop is strongly NP-hard in general, so some restriction of Theorem 2's kind is unavoidable for an exact ordering rule.

Setting

There are $n$ items and three machines. Item $i$ needs processing time $A_i > 0$ on machine 1, $B_i > 0$ on machine 2 and $C_i > 0$ on machine 3, in that order. Each machine handles at most one item at a time, and processing is not interrupted.

A schedule assigns each item start times $s^1_i, s^2_i, s^3_i$. It is feasible when all start times are at least $0$ on machine 1, the processing intervals of distinct items on the same machine do not overlap, and $s^1_i + A_i \le s^2_i$, $s^2_i + B_i \le s^3_i$. The three machines may process the items in different orders. The total elapsed time (makespan) is $\max_i (s^3_i + C_i)$.

An ordering $\sigma$ lists the items, $\sigma(k)$ being the item in position $k$. Its as-soon-as-possible schedule processes the items in the order $\sigma$ on every machine and starts each item on each machine as early as the rules allow. For an ordering, with positions $1, \dots, n$, Johnson defines

$$K_u = \sum_{i=1}^{u} A_i - \sum_{i=1}^{u-1} B_i, \qquad H_v = \sum_{i=1}^{v} B_i - \sum_{i=1}^{v-1} C_i,$$

the sums running over the items in the first $u$ (resp. $v$) positions.

Johnson's three-stage rule says that item $i$ definitely precedes item $j$ when

$$\min(A_i + B_i,\ C_j + B_j) < \min(A_j + B_j,\ C_i + B_i) \tag{IV}$$

and calls them indifferent under equality. An ordering is consistent with (IV) when no item placed later is definitely preferred to an item placed earlier.

Formalization targets

Goal: Theorem 2 (p. 67)

If every $A_i$ is at least every $B_j$, then an ordering consistent with (IV) exists, and for every such ordering $\sigma$ the as-soon-as-possible schedule of $\sigma$ is feasible and satisfies

$$\operatorname{makespan}(\text{as-soon-as-possible schedule of } \sigma) \le \operatorname{makespan}(s) \quad \text{for every feasible schedule } s .$$

Milestones

1. Lemma 3 (p. 65). Every feasible schedule is matched or beaten by the as-soon-as-possible schedule of some single ordering.
2. Closed form (p. 66). For every ordering, the total idle time of machine 3 is $\sum_i Y_i = \max_{1 \le u \le v \le n}(H_v + K_u)$, so that

$$\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} (K_u + H_v),$$

the "maximum walk" of p. 68. 3. Special case (p. 67). If $\min A_i \ge \max B_j$ then $\max_{u \le v} K_u = K_v$, so the makespan is $\sum_i C_i + \max_v (H_v + K_v)$. 4. (III) $\Leftrightarrow$ (IV) (p. 67). Interchanging the items in positions $j, j+1$ changes $H$ and $K$ only at $j, j+1$, and the interchange is strictly worse for the diagonal terms exactly when (IV) holds. 5. Lemma 4 (p. 67). Relation (IV) is transitive, except when the middle item is indifferent to both others. 6. Mirror case (p. 68). The conclusion of Theorem 2 also holds when every $C_i$ is at least every $B_j$.

Significance

The result. Theorem 2 gives an $O(n \log n)$ exact method for a class of three-machine flow shops, in a problem that is strongly NP-hard in general. Lemma 3 says that, for three machines, permutation schedules are dominant; Johnson's example on p. 65 shows this fails for four machines. The closed form of milestone 2 expresses the makespan of any ordering as a longest path in a grid, the device behind most later flow-shop lower bounds.

Formalizing it. All results are proved on paper, some tersely: Lemma 3's proof is two lines and cites the wrong lemma, Lemma 4 is proved by reference to Lemma 2, and the mirror case is asserted without proof. A search of Mathlib and of the platform catalog found no machine-checked proof of any of them. The mission produces a checked account of the three-machine flow shop, including the comparison against all feasible schedules rather than only permutation schedules, and pins down the exact form of the hypotheses (see below).

Difficulty

The interchange argument of the two-machine case does not transfer directly. For a general ordering the makespan involves $\max_{u \le v}(H_v + K_u)$, and interchanging adjacent items changes terms that depend on everything placed earlier; the page notes that "the decision is not independent of what precedes the interchanged elements". The hypothesis $\min A \ge \max B$ is what makes $K$ nondecreasing along the ordering, collapsing the double maximum to the diagonal. A second obstacle is that (IV) is not a total preorder: ties break transitivity, so passing from "no adjacent pair can be improved" to "optimal" needs the all-pairs consistency and the tie exception of Lemma 4. Finally, Lemma 3 is a statement about arbitrary start-time schedules, so the reduction to orderings must handle machines whose orders differ.

Formalization scope

Items are Fin n; processing times are real-valued functions A B C : Fin n → ℝ, assumed positive in each theorem that is about schedules (the paper's standing assumption, p. 61). A schedule is three start-time functions; feasibility is spelled out as above with non-overlap written as a disjunction of inequalities. The makespan is the maximum of the machine-3 completion times together with $0$, so the empty instance has makespan $0$. An ordering is an Equiv.Perm (Fin n) with σ k the item in position k; positions are 0-based, so the Lean K u, H v are the paper's $K_{u+1}$, $H_{v+1}$. Statements with maxima over positions assume $n \ge 1$.

Hypotheses made explicit or corrected:

• $\min A_i \ge \max B_i$ is read globally, $B_j \le A_i$ for all $i, j$, as in the section heading. The pointwise reading $B_i \le A_i$ makes Theorem 2 false (an instance with five items is recorded in the Formalization Note of the goal).
• Consistency with (IV) is required for all pairs of positions, not only adjacent ones.
• Lemma 4 carries Lemma 2's exception for an item indifferent to both others; without it the statement is false.
• Lemma 3's proof cites "Lemma 2" where Lemma 1 is meant.
• The interchange equivalence (milestone 4) is stated for arbitrary reals, which is stronger than the page needs.

Optimality in the goal is against every feasible schedule. A formalization that compares only orderings with each other, or that defines the objective as the closed form $\sum C + \max(K_u + H_v)$, would drop Lemma 3's content and is ruled out: the makespan is the latest completion time of a start-time schedule. The existence clause keeps the optimality clause from being vacuous.

A complete development needs finite sums over initial segments of Fin n, Finset.sup', and permutation manipulations (adjacent transpositions, bubble-sort arguments). The feasibility model and the closed form are reusable for other flow-shop results; contributions of general lemmas on adjacent interchanges of permutations are welcome.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117

Motivation

Project scheduling assigns start times to the activities of a project subject to constraints between them. The classical critical path method (CPM) of Kelley and Walker (1959) and the program evaluation and review technique (PERT) allow only minimum time lags: activity $j$ may start no earlier than a given time after activity $i$ starts. Practice also needs maximum time lags: activity $j$ must start no later than a given time after $i$. These express deadlines, release dates, time windows and "no wait" couplings. Once maximum time lags are allowed, the project network has cycles and negative arc weights, and even the existence of a schedule is no longer automatic.

This mission is the first of a series on Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), a standard reference for resource-constrained project scheduling with general temporal constraints. Chapter 1 contains the temporal part of the theory: feasibility, earliest and latest schedules, floats, and the distance order. Every later chapter adds resource constraints on top of this layer.

Timeline. Roy (1964) introduced the Metra Potential Method, which is scheduling on activity-on-node networks with minimum time lags. Neumann (1975, Sect. 6.4) treated time windows through potentials on networks with arbitrary arc weights. Bartusch, Möhring and Radermacher (1988, Annals of Operations Research 16) developed the general theory of scheduling project networks with resource constraints and time windows, including the feasibility criterion stated below. The book collects these results in Chapter 1.

Setting

A project consists of $n\ge 1$ real activities $1,\dots,n$ and two fictitious activities, $0$ (project beginning) and $n+1$ (project completion), so the node set is $V=\{0,1,\dots,n+1\}$. Each activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities.

A minimum time lag $d^{\min}_{ij}$ between two different activities becomes an arc $\langle i,j\rangle$ of weight $\delta_{ij}=d^{\min}_{ij}$. A maximum time lag $d^{\max}_{ij}$ becomes a backward arc $\langle j,i\rangle$ of weight $\delta_{ji}=-d^{\max}_{ij}$. There is at most one arc per ordered pair, keeping the tightest lag. The result is the activity-on-node (AoN) network $N=(V,E,\delta)$, whose integer weights may be positive, negative or zero and which in general contains cycles. The book establishes that for every node $i$ there is a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$ (p. 8, from Definition 1.1.1 and Remarks 1.1.2). This is the standing assumption of the chapter.

A schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ and $S_i\ge 0$. It is time-feasible if it satisfies the temporal constraints

$$S_j-S_i\ \ge\ \delta_{ij}\qquad(\langle i,j\rangle\in E),$$

and $\mathcal S_T$ is the set of time-feasible schedules. A time-feasible schedule minimizing the project duration $S_{n+1}$ is time-optimal.

The length of a path or cycle is the sum of its arc weights. For an integer $L=LS_{n+1}$, which is either a prescribed maximum project duration $\bar d$ or the shortest project duration, the temporal scheduling network $N^+$ adds the backward arc $\langle n+1,0\rangle$ with weight $-L$. The distance $d_{ij}$ is the length of a longest path from $i$ to $j$ in $N^+$, with $d_{ii}=0$. The earliest and latest start times are $ES_i=d_{0i}$ and $LS_i=-d_{i0}$, the earliest completion time is $EC_i=ES_i+p_i$, and the total float is $TF_i=LS_i-ES_i$. The distance order $\prec_D$ is defined for $i\ne j$ by: $i\prec_D j$ if $d_{ij}>0$, or $d_{ij}=0$ and $d_{ji}<0$.

Formalization targets

Goal: Theorem 1.3.3 (p. 10)

$$\mathcal S_T\ne\emptyset\quad\Longleftrightarrow\quad N\ \text{contains no cycle of positive length}.$$

The statement contains no constants. It is the consistency criterion for the temporal constraints and the entry condition for everything else in the book.

Milestones

1. Distances, §1.3, p. 11, Eq. (1.3.3). If $N^+$ has no cycle of positive length, then $d$ satisfies $d_{ij}\ge\delta_{ij}$ on $E^+$ and the triangle inequality $d_{ij}\ge d_{ih}+d_{hj}$, and it is the smallest family that does.
2. Earliest and latest schedules, §1.3, p. 12. Under the same hypothesis and the standing assumption, $ES=(d_{0i})_i$ is time-feasible and lies below every time-feasible schedule. $LS=(-d_{i0})_i$ is time-feasible, satisfies $LS_{n+1}\le L$, and lies above every time-feasible schedule $S$ with $S_{n+1}\le L$.
3. Remark 1.3.2 (p. 10). If $\mathcal S_T\ne\emptyset$, there is an integer-valued time-optimal schedule.
4. Proposition 1.3.8 (p. 15). For a real activity $i$, $[LS_i,EC_i[\ne\emptyset$ if and only if $i$ is critical ($TF_i=0$) or near-critical ($0<TF_i<p_i$). A further item of the mission, not a milestone, states the claim of §1.4, p. 17 (after Definition 1.4.3): if $N^+$ has no cycle of positive length, $\prec_D$ is a strict order on $V$.

Significance

The result itself. Theorem 1.3.3 tells when the temporal constraints of a project can be met at all. Milestones 1 and 2 identify the earliest and latest schedules with longest path lengths, which makes temporal scheduling a pair of longest-path computations (a forward pass from $0$ and a backward pass to $0$). Remark 1.3.2 justifies working in integer time. The distance order and the base time intervals $[LS_i,EC_i[$ are the inputs of the resource-constrained methods in Chapters 2 and 3: priority rules schedule along $\prec_D$, and base time intervals give lower bounds on resource usage.

Formalizing it. These results are classical and proved, but the book does not prove Theorem 1.3.3; it points to Neumann (1975) and Bartusch et al. (1988). To our knowledge they have no machine-checked form in this generality, with arbitrary integer weights, cycles, fictitious start and end nodes, and the backward arc of $N^+$. The CPM results for acyclic event networks with nonnegative durations already on Prove2Me are a special case. The definitions of this mission (project, AoN network, schedule, $N^+$, distances) are intended as the shared substrate for the later missions of the series, which add renewable and cumulative resources.

Difficulty

The necessity direction of the goal is a telescoping sum around a cycle. The sufficiency direction needs a schedule, and the natural candidate $S_i=d_{0i}$ requires three things: longest path lengths must be well defined, they must be finite, and they must satisfy the temporal constraints. With negative weights and cycles, the maximum over walks is unbounded when a positive cycle exists, and a walk-based definition gives nothing. A path-based definition gives a finite maximum but loses the concatenation property, so the triangle inequality becomes a statement about removing nonpositive cycles from walks. $S_0=0$ and $S_i\ge 0$ further depend on the standing assumption: without it, an arc $\langle i,0\rangle$ with positive weight makes $\mathcal S_T$ empty although no cycle is positive. The same combinatorics of walks, paths and cycles is behind milestones 1 and 2 and the distance-order item.

Formalization scope

Nodes are Fin (n + 2): $0$ is the project beginning and Fin.last (n + 1) the project completion. The field one_le_n records $n\ge 1$. Durations are natural numbers with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities. Arc weights are arbitrary integers on a loop-free Finset of ordered pairs, so parallel arcs cannot occur. Start times are real; integrality appears only as Remark 1.3.2.

Walks are functions Fin (m + 1) → Fin (n + 2). A path is an injective walk, and a cycle is a closed walk with at least one arc and distinct nodes apart from the repeated endpoint. Distances are maxima over the finitely many paths, valued in WithBot ℤ with $\bot=-\infty$ for unreachable pairs. No supremum over an unbounded set is taken. $ES_i$ and $LS_i$ convert these to integers with junk value $0$ for $-\infty$, and every milestone that uses them carries the hypotheses under which the distances are finite. The backward arc of $N^+$ has weight $-L$ for an integer parameter $L$. If $N$ already contains an arc $\langle n+1,0\rangle$, the two arcs merge into one carrying the larger weight, as in the book's convention for parallel lags. The standing assumption of p. 8 is a named predicate and a hypothesis of the goal and of milestones 2 and 4.

A trivializing formalization is ruled out: weights are signed integers and cycles are allowed, so the no-positive-cycle condition is not vacuous, and the standing assumption is satisfiable by projects with maximum time lags.

A complete development needs cycle removal from closed walks, the Bellman-type characterization of longest paths without positive cycles, and total unimodularity or a direct integrality argument for Remark 1.3.2. The walk, path and distance layer is reusable for any difference-constraint system. Proofs of milestones and lemmas on walk decomposition 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
• K. Neumann, Operations Research Verfahren, Band III, Hanser, 1975, Sect. 6.4.
• B. Roy, Les problèmes d'ordonnancement: applications et méthodes, Dunod, 1964.
• J. E. Kelley, M. R. Walker, "Critical-path planning and scheduling", Proceedings of the Eastern Joint Computer Conference, 1959, 160–173. https://doi.org/10.1145/1460299.1460318
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993, Sect. 5.4 and 5.6.

Motivation

Resource-constrained project scheduling with general temporal constraints, written $PS|temp|C_{\max}$, asks for start times of the activities of a project that respect minimum and maximum time lags between activities and the capacities of renewable resources (staff, machines, reactors), and that minimize the project duration. Deciding whether a feasible schedule exists at all is already NP-complete (Bartusch, Möhring and Radermacher, 1988), so exact methods are branch-and-bound procedures. The dominant family, going back to De Reyck and Herroelen (1998) and presented in Chapter 2 of Neumann, Schwindt and Zimmermann's monograph, branches on resource conflicts: whenever the currently computed schedule overloads a resource at some time $t$, the set of activities in progress at $t$ is a forbidden set, and the node is split into children, each of which adds precedence constraints that resolve the conflict.

Such a scheme is only correct if the children together retain every feasible schedule. Theorem 2.5.7 of the book is exactly this completeness guarantee, and it is the reason the enumeration can be restricted to the small family of minimal delaying modes instead of arbitrary ways of breaking up a conflict. The same section also contains the preprocessing results (§2.5.2) that exploit two-element forbidden sets before any branching happens. This mission formalizes both.

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, both of duration $0$, and every real activity $i\in\{1,\dots,n\}$ has an integer duration $p_i>0$. The project network $N$ has arc set $E$ and integer arc weights $\delta_{ij}$; the arc $\langle i,j\rangle$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$. A finite set $\mathcal R$ of renewable resources is given; resource $k$ has capacity $R_k\in\mathbb N$ and activity $i$ uses $r_{ik}\in\mathbb Z_{\ge0}$ units of it, with $r_{ik}\le R_k$ and $r_{0k}=r_{n+1,k}=0$.

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge0$. The active set at time $t$ is $\mathcal A(S,t)=\{i\in V\mid S_i\le t<S_i+p_i\}$. The schedule is time-feasible if it satisfies all temporal constraints, resource-feasible if

$$\sum_{i\in\mathcal A(S,t)}r_{ik}\le R_k\qquad(k\in\mathcal R,\ t\ge0),$$

and feasible if it is both; $\mathcal S$ denotes the set of feasible schedules.

A set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$, a feasible set otherwise, and minimal forbidden if no proper subset is forbidden. For a forbidden $F$, a set $B\subseteq F$ is a delaying alternative if $F\setminus B$ is feasible, and a minimal delaying alternative if no proper subset of $B$ is one. A minimal delaying mode for $F$ is a pair $(i,B)$ with $B$ a minimal delaying alternative for $F$ and $i\in F\setminus B$.

For §2.5.2, fix an integer upper bound $UB$ on the project duration. The temporal scheduling network $N^+$ adds to $N$ the arc $\langle n+1,0\rangle$ with weight $\delta_{n+1,0}=-UB$, and $d_{ij}$ is the longest path length from $i$ to $j$ in $N^+$ ($-\infty$ if there is no path, $d_{ii}=0$).

Formalization targets

Goal: Theorem 2.5.7 (p. 49)

For every forbidden set $F$ and every feasible schedule $S\in\mathcal S$ there is a minimal delaying mode $(i,B)$ for $F$ with

$$S_j\ge S_i+p_i\qquad(j\in B).$$

$F$ is arbitrary (not necessarily minimal); $B$ must be a minimal delaying alternative and $i$ must lie outside $B$.

Milestones

1. Eqs. (2.5.2)–(2.5.3), p. 46. $B$ is a minimal delaying alternative for a forbidden $F$ iff $F\setminus B$ is a maximal feasible subset of $F$, iff $B\subseteq F$,

$$\sum_{i\in F\setminus B}r_{ik}\le R_k\ (k\in\mathcal R)\quad\text{and}\quad\forall j\in B\ \exists k:\ \sum_{i\in F\setminus B}r_{ik}+r_{jk}>R_k.$$

2. Bartusch et al.'s criterion (proof of Theorem 2.3.10, p. 35). A schedule is resource-feasible iff every minimal forbidden set $F$ contains distinct $i,j$ with $S_j\ge S_i+p_i$.
3. Lemma 2.5.5, p. 49. A minimal delaying alternative for $F$ is an inclusion-minimal set meeting every minimal forbidden $F'\subseteq F$.
4. Theorem 2.5.11, p. 55. If $\{i,j\}$ is a two-element forbidden set with $d_{ij}<p_i$ and $d_{ij}>-p_j$, then every feasible $S$ with $S_{n+1}\le UB$ satisfies $S_j\ge S_i+p_i$.
5. Eq. (2.5.7), p. 55. If for a two-element forbidden set $\{i,j\}$ neither $d_{ij}>-p_j$ nor $d_{ji}>-p_i$ holds, then for all $h,l\in V$ and every feasible $S$ with $S_{n+1}\le UB$,

$$S_l\ge S_h+\min\bigl(d_{hi}+p_i+d_{jl},\ d_{hj}+p_j+d_{il}\bigr).$$

Significance

The result. Theorem 2.5.7 is the completeness statement of the De Reyck–Herroelen enumeration scheme (Algorithm 2.5.8): if every child of a conflict node imposes the precedence constraints $i\to j$ ($j\in B$) of one minimal delaying mode $(i,B)$, the children's order polyhedra together contain all feasible schedules of the parent. Proposition 2.5.9(a), the correctness of the whole branch-and-bound procedure, rests on it. Because the objective does not enter, the book reuses the theorem for the regular and nonregular objectives of Chapter 3. Theorem 2.5.11 and inequality (2.5.7) are the preprocessing rules that shrink the time-feasible region before enumeration: each adds temporal constraints that every feasible schedule within the bound already satisfies, which raises the lower bound $ES_{n+1}$ and prunes the enumeration.

Formalizing it. All statements are proved in the book (Bartusch et al.'s criterion is quoted from their 1988 paper with the necessity argument sketched). None of them has a machine-checked proof; the Prove2Me catalog contains precedence-only scheduling models (Brucker–Knust) and acyclic event networks (Kelley–Walker) but no model with time windows and forbidden sets. The mission produces a reusable library of forbidden sets, delaying alternatives and longest-path distances in networks with maximum time lags.

Difficulty

The obvious idea — pick any two overlapping activities and delay one — does not give a minimal delaying alternative with a single delaying activity $i$ common to all of $B$. The proof has to pass from the pairwise separations that resource-feasibility guarantees in each minimal forbidden subset to a set $B$ that is simultaneously minimal as a delaying alternative and ordered behind one activity outside $B$. This needs the correspondence between delaying alternatives and hitting sets of the minimal forbidden subsets (Lemma 2.5.5) and the positivity of real durations to keep $i$ outside $B$. For the preprocessing results, the delicate part is relating longest paths in $N^+$, including the backward arc carrying $-UB$, to the start-time differences of every feasible schedule within the bound.

Formalization scope

Activities are Fin (n + 2), with $n+1$ as Fin.last (n + 1). Start times are real; durations, capacities, requirements and time lags are integers (natural numbers where the book says so). The standing assumptions of the book (at least one real activity, zero-duration dummies, positive durations of real activities, no loops, $r_{0k}=r_{n+1,k}=0$, $r_{ik}\le R_k$, and paths in $N$ from $0$ to every node and from every node to $n+1$) are one hypothesis P.StandingAssumptions of every theorem.

Resource constraints are imposed for every $t\ge0$, not only for $0\le t\le\bar d$ as (2.1.4) literally writes. The book's proofs and Remark 2.3.11 use the $t\ge0$ reading; with the literal cut-off, schedules running past $\bar d$ could violate capacities after $\bar d$, and Bartusch et al.'s criterion would fail.

Longest path lengths are maxima over simple paths, with values in WithBot ℝ (⊥ for $-\infty$). If $N^+$ has a cycle of positive length, no schedule satisfies the temporal constraints with $S_{n+1}\le UB$, and the statements using $d_{ij}$ are vacuous, as in the book. The arc $\langle n+1,0\rangle$ of $N^+$ has weight $-UB$, or $\max(\delta_{n+1,0},-UB)$ if $N$ already has such an arc. $UB$ is an integer.

The goal is not trivial: it quantifies over minimal delaying modes only. A variant without the minimality of $B$, or allowing $i\in B$, would be nearly empty (take $B=F\setminus\{i\}$), and the statement here rules both out. Maximality in milestone 1 is taken among subsets of $F$.

Welcome contributions: the hitting-set correspondence between delaying alternatives and minimal forbidden subsets, the telescoping bound $S_j-S_i\ge d_{ij}$ for feasible schedules, and proofs of any milestone. The definitions restate the setup of the series' earlier missions (II: order polyhedra) locally, because those are still drafts.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.5. 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
• B. De Reyck, W. Herroelen, A branch-and-bound procedure for the resource-constrained project scheduling problem with generalized precedence relations, European Journal of Operational Research 111 (1998) 152–174. https://doi.org/10.1016/S0377-2217(97)00305-6

Motivation

In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.

A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem $PSc|temp|C_{\max}$.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ with $n\ge 1$, where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i\ge 0$, with $p_0=p_{n+1}=0$ and $p_i>0$ for the real activities.

For each cumulative resource $k$ in a set $\mathcal R^\gamma$, every activity $i$ has an integer demand $r_{ik}$. If $r_{ik}<0$, activity $i$ withdraws $-r_{ik}$ units of $k$ at its start; if $r_{ik}>0$, it deposits $r_{ik}$ units at its completion; $r_{ik}=0$ means $k$ is not used. The demand $r_{0k}$ of the project beginning is the initial stock. Write $V_k^-=\{i\mid r_{ik}<0\}$ and $V_k^+=\{i\mid r_{ik}>0\}$. Each resource has a safety stock $\underline R_k\in\mathbb Z$ and a storage capacity $\overline R_k\in\mathbb Z$.

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge 0$. The active set and the inventory of $k$ at time $t\ge 0$ are

$$\mathcal A_k(S,t)=\{i\in V_k^-\mid S_i\le t\}\cup\{i\in V_k^+\mid S_i+p_i\le t\},\qquad r_k(S,t)=\sum_{i\in\mathcal A_k(S,t)} r_{ik}.$$

The schedule is inventory-feasible if $\underline R_k\le r_k(S,t)\le\overline R_k$ for all $k$ and all $t\ge 0$.

Two standing assumptions of the section are used throughout: (2.12.1) $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$, so the final inventory is admissible; and Remark 2.12.2, $\underline R_k\le 0\le\overline R_k$.

A nonempty $F\subseteq V$ is a $k$-surplus set if $\sum_{i\in F}r_{ik}>\overline R_k$, and a $k$-shortage set if $\sum_{i\in F}r_{ik}<\underline R_k$. A $k$-surplus set $F$ is minimal if no $k$-surplus set arises from $F$ by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal $k$-shortage sets are defined with the roles of replenishing and depleting activities exchanged. $\mathcal F_k^+$ and $\mathcal F_k^-$ denote the minimal $k$-surplus and $k$-shortage sets.

Formalization targets

Goal: Theorem 2.12.4

A schedule $S$ is inventory-feasible if and only if

$$\forall k,\ \forall F\in\mathcal F_k^+\ \exists j\in F,\ i\notin F:\ r_{jk}>0,\ r_{ik}<0,\ S_j+p_j\ge S_i,$$ $$\forall k,\ \forall F\in\mathcal F_k^-\ \exists j\in F,\ i\notin F:\ r_{jk}<0,\ r_{ik}>0,\ S_j\ge S_i+p_i.$$

Milestones

1. The invariance claim after Remark 2.12.2 (p. 131): adding the same integer $a_k$ to $r_{0k}$, $\underline R_k$ and $\overline R_k$ does not change the set of inventory-feasible schedules.
2. Lemma 2.12.3 (a): for every $k$-surplus set $F$ there is a minimal $k$-surplus set $F'$ with $\emptyset\ne F'\cap V_k^+\subseteq F\cap V_k^+$ and $F'\cap V_k^-\supseteq F\cap V_k^-$.
3. Lemma 2.12.3 (b): the shortage counterpart.
4. Theorem 2.12.4 (a) on its own: the upper constraints $r_k(S,t)\le\overline R_k$ hold for all $t\ge 0$ iff condition (a) holds.
5. Theorem 2.12.4 (b) on its own: the lower constraints hold for all $t\ge 0$ iff condition (b) holds.

Significance

The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation $S_j+p_j\ge S_i$ (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation $S_j\ge S_i+p_i$. Consequences stated in the book: the feasible region of $PSc|temp|C_{\max}$ is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.

The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.

Difficulty

The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family $\mathcal F_k^+$ and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at $t$, so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock $r_{0k}$ is handled by the same active-set rule as any other demand, which matters for the invariance claim.

Formalization scope

• Activities are Fin (n + 2), activity $n+1$ is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.
• The inventory constraints are required for every $t\ge 0$. The book prints (2.12.2) for $0\le t\le\bar d$, but its proof of Theorem 2.12.4 works with an arbitrary $t\ge 0$ (the necessity half uses the last completion time of a replenishing activity, which need not be at most $\bar d$). The two readings coincide for schedules with $S_{n+1}\le\bar d$ whose activities all finish by $S_{n+1}$.
• A schedule satisfies $S_0=0$ and $S_i\ge 0$ and is not required to be time-feasible; time lags play no role in this section's results and are not part of the model.
• (2.12.1) and Remark 2.12.2 are explicit hypotheses (TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.
• A formalization in which $\mathcal F_k^+$ is empty or trivial (for instance, minimality with non-strict inclusions, which no set satisfies) makes condition (a) vacuous; the definitions here follow p. 131 exactly, and a concrete instance with a nonempty $\mathcal F_k^+$ has been checked locally.

Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of $PSc|temp|C_{\max}$ (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.12.1, pp. 128–135. https://doi.org/10.1007/978-3-540-24800-2
• K. Neumann, C. Schwindt, Project scheduling with inventory constraints, Mathematical Methods of Operations Research 56 (2003) 513–533 (cited in the book as 2002). https://doi.org/10.1007/s001860200251

Motivation

The single-machine scheduling problem $1|\mathrm{prec}|\sum w_j C_j$ asks for an order in which to process $n$ jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for general precedence constraints is $2$. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) relate the problem to the dimension theory of partial orders: their Theorem 3.2 states that when the precedence constraints are given together with a realizer of size $k$, the problem has a $(2 - 2/k)$-approximation algorithm. Small realizers of structured precedence orders therefore translate directly into better approximation ratios.

This mission formalizes one such structural result, Lemma 4.1 of the paper: every convex bipartite order has a realizer of size $3$. Convex bipartite orders form a class of precedence constraints that lies strictly between strong bipartite orders and general bipartite orders (Möhring, 1989). Combined with Theorem 3.2, the lemma gives a $4/3$-approximation for $1|\mathrm{prec}|\sum w_j C_j$ on this class. According to the authors, the bound $\dim \le 3$ for convex bipartite orders had not been known before.

Setting

A poset is a set $N$ with a reflexive, antisymmetric, transitive relation $P$. Two elements $x, y$ are incomparable, written $x \parallel y$, when neither $(x,y) \in P$ nor $(y,x) \in P$; the set of incomparable pairs is $\mathrm{inc}(P)$. A linear extension of $P$ is a linear order $L$ on $N$ with $P \subseteq L$. A linear order $L$ reverses the pair $(x,y)$ when $y < x$ in $L$. A realizer of size $t$ is a family $L_1, \dots, L_t$ of linear extensions of $P$ such that every incomparable pair $(x,y)$ is reversed by at least one $L_i$. The dimension $\dim(P)$ is the least $t$ for which a realizer of size $t$ exists.

A convex bipartite order has jobs $N = J^- \cup J^+$ split into minus jobs $J^- = \{j_1, \dots, j_a\}$ and plus jobs $J^+ = \{j_{a+1}, \dots, j_n\}$. Each plus job $j_k$ carries two indices $1 \le l(k) \le r(k) \le a$, and a minus job $j_i$ precedes $j_k$ exactly when $l(k) \le i \le r(k)$. There are no other precedences: the predecessors of each plus job form a nonempty interval of consecutive minus jobs.

For the Appendix construction, the incomparable pairs are sorted into three sets $E_1, E_2, E_3$ according to the kinds of the two jobs, the order of their indices and, for a pair (plus job $j_i$, minus job $j_j$), whether $j_j$ precedes some plus job of larger index than $i$. The sets $\bar E_m = E_m \cup P$ describe what the $m$-th linear order of the realizer must contain.

Formalization targets

Goal: Lemma 4.1

$$\text{For every convex bipartite order } (N, P):\quad \exists\, L_1, L_2, L_3 \text{ linear extensions of } P \text{ with } \forall (x,y) \in \mathrm{inc}(P)\ \exists m:\ y <_{L_m} x .$$

Equivalently, $\dim(P) \le 3$. The goal holds for every numbering of the jobs and every choice of interval ends $l, r$.

Milestones

• Lemma A.1. $E_1, E_2, E_3$ partition $\mathrm{inc}(P)$, and for each $m$, $(x,y) \in E_m$ implies $(y,x) \notin E_m$.
• Lemma A.2. Under the Appendix's numbering of the plus jobs ($i < j$ implies $l(i) \le l(j)$), each $\bar E_m$ is contained in a linear order on $N$.

Significance

The result. Lemma 4.1 places convex bipartite orders among the classes of precedence constraints for which $1|\mathrm{prec}|\sum w_j C_j$ has an approximation ratio strictly below $2$, namely $4/3$ through Theorem 3.2 of the paper. The bound is tight: a bipartite order has dimension $2$ exactly when it is a strong bipartite order (Möhring), so the bound $3$ cannot be lowered for the class of convex bipartite orders. Since $\dim(P) = 3$ also gives $\chi(G_P) = 3$ for the graph of incomparable pairs, a $3$-realizer yields an optimal colouring of that graph.

Formalizing it. The result is proved in the paper, with a short case analysis in the Appendix. No machine-checked proof is known to exist. Mathlib has no dimension theory of posets: realizers, reversals of incomparable pairs and the construction of linear extensions containing a given acyclic relation have to be set up here. The definitions of realizer and linear extension are stated for an arbitrary relation and can be reused for other dimension bounds (interval orders, semiorders, the other missions of this series).

Difficulty

The three relations $\bar E_m$ are not partial orders. $\bar E_2$, for instance, is not transitive: with two minus jobs and one plus job $j_3$ with $l(3) = r(3) = 2$, the pairs $(j_1, j_2) \in E_2$ and $(j_2, j_3) \in P$ are present but $(j_1, j_3)$ lies in $E_1$. The step that requires work is to show that each $\bar E_m$ has no cycle, so that it extends to a linear order. For $\bar E_2$ this depends on the convexity of the predecessor intervals and on the numbering of the plus jobs by their left ends: it is not a consequence of bipartiteness alone. The goal itself carries no numbering assumption, so any proof must also account for renumbering the plus jobs.

Formalization scope

All declarations live in the namespace SingleMachinePrec.ConvexBipartite.

• Relations. A relation on $N$ is a predicate N → N → Prop. Linear orders use Mathlib's unbundled class IsLinearOrder. A linear extension of $P$ is a linear order $L$ with $P \subseteq L$; $L$ reverses $(x,y)$ when $L\,y\,x$ and $y \ne x$. A realizer of size $t$ is a function Fin t → N → N → Prop, so repeated members are allowed, as in the paper's multisets.
• Convex bipartite orders. The jobs are the type Fin a ⊕ Fin b: Sum.inl i is the minus job $j_{i+1}$, Sum.inr k the plus job $j_{a+k+1}$, with indices starting at $0$. The interval ends are maps l r : Fin b → Fin a with l k ≤ r k, and $P$ is equality together with the pairs (minus $i$, plus $k$) with $l(k) \le i \le r(k)$. A file-level instance records that $P$ is a partial order. Any convex bipartite order in the paper's sense is one of these after naming its jobs. The cases $a = 0$ and $b = 0$ are allowed.
• $E_1, E_2, E_3$. Each set is defined as "incomparable and satisfies the paper's case condition". In the plus–minus clauses, "$k > i$" compares plus indices, because $k$ exceeds the index of a plus job.
• Lemma A.2. "$\bar E_m$ is an extension of $P$" is formalized as "there is a linear order containing $\bar E_m$", which is what the paper's proof establishes (absence of cycles) and what its final paragraph uses. Reading it as "$\bar E_m$ is a partial order" would make the lemma false (see Difficulty). The Appendix's numbering assumption is the hypothesis Monotone l of this milestone only.
• Algorithmic wording not formalized. The paper states Lemma 4.1 as "a realizer of size 3 can be computed in polynomial time". What is formalized is the existence of the realizer; the running time is not.

A trivializing formalization would let the members of the realizer be arbitrary relations, which makes reversing every pair free. Here every member must be a linear order containing $P$.

Contributions welcome: proofs of the two milestones and of the goal; a general lemma that a relation whose transitive closure is antisymmetric extends to a linear order on a finite type; and the renumbering argument that removes the numbering assumption.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992.
• R. H. Möhring, Computationally tractable classes of ordered sets, in I. Rival (ed.), Algorithms and Order, NATO ASI Series 255, Kluwer, 1989, pp. 105–193.
• W. T. Trotter, Combinatorics and Partially Ordered Sets: Dimension Theory, Johns Hopkins University Press, 1992.