The OR Formalization Drive

Motivation

A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.

The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.

Setting

Demand is a random variable with distribution function $F$ and density $f$. The paper assumes $F(0) = 0$, $F$ strictly increasing, and an increasing generalized failure rate (IGFR): $g(x) = x f(x)/(1 - F(x))$ has $g'(x) > 0$. Production costs $c$ per unit, the retail price is $p$, and leftover units are salvaged for $v$, with $v < c < p$. Expected sales with $q$ units available are

$$S(q) = q - \int_0^q F(x)\,dx,$$

and the integrated supply chain's expected profit is $\Pi(q) = (p - v)S(q) - (c - v)q$. It is maximized at $q^o$ with $F(q^o) = (p-c)/(p-v)$; write $\Pi^o = \Pi(q^o)$. The efficiency of a contract is $\Pi(q)/\Pi^o$, where $q$ is the quantity produced.

A contract is a pair of wholesale prices $\{w_1, w_2\}$ with $w_1 \le w_2$. The retailer first prebooks $y \ge 0$ units at $w_1$ each. The supplier, seeing $y$, produces $q \ge y$. During the season the retailer sells the prebook and, once it runs out, places at-once orders at $w_2$ per unit from the supplier's remaining stock, provided $w_2 \le p$. The supplier's and retailer's expected profits are

$$\pi_s(y, q) = (w_1 - v)y + (w_2 - v)(S(q) - S(y)) - (c - v)q,$$ $$\pi_r(y, q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)(S(q) - S(y)),$$

with the at-once terms absent when $w_2 > p$. An outcome of a contract is a pair $(y, q)$ where $q$ maximizes the supplier's profit given $y$, and $y$ maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push ($w_1 < p < w_2$), pull ($w_1 = w_2 \le p$) and advance-purchase discount ($w_1 < w_2 \le p$). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).

Formalization targets

Goal: Theorem 7

For every $w_1$ with $c \le w_1 \le p$, the contract $\{w_1, p\}$ has an outcome and is Pareto; every outcome $(y, q)$ of every Pareto contract satisfies

$$\Pi(q) = \Pi^o;$$

and for every $r \in [0, \Pi^o]$ some contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome with payoffs

$$\bigl(\pi_r, \pi_s\bigr) = \bigl(r,\ \Pi^o - r\bigr).$$

Milestones

1. Eq. (2): $\Pi$ is concave on $[0, \infty)$ and maximized exactly where $F(q^o) = (p-c)/(p-v)$.
2. Eqs. (20)–(21): for $c \le w_2 \le p$, the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - c)/(w_2 - v)$.
3. Eq. (22): for $c \le w_1 \le w_2 \le p$, $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$ is the unique maximizer of $\pi_r(\cdot, q)$.
4. Eq. (3): in push mode the retailer's optimal prebook solves $F(q) = (p - \hat w_1)/(p - v)$.

A further draft theorem states the step of the proof in which the retailer's outcome profit along $\{w_1, p\}$ falls strictly from $\Pi^o$ to $0$ as $w_1$ rises from $c$ to $p$.

Significance

The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces $q^o$; the prebook price then acts as a pure transfer. Every division of $\Pi^o$ is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.

The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.

Difficulty

The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when $w_2 = p$. Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook $y = 0$ always being available and on $w_1 \ge c$. Third, the division claim is surjectivity of the retailer's equilibrium payoff over $w_1 \in [c, p]$, which needs the solution of $F(y_r) = (p - w_1)/(p - v)$ to vary continuously with $w_1$, including at both ends ($y_r = q^o$ at $w_1 = c$, $y_r = 0$ at $w_1 = p$).

Formalization scope

Demand is a probability measure $\mu$ on $\mathbb R$ with $F$ = ProbabilityTheory.cdf μ. The standing assumptions are a structure: $F(0) = 0$, $F$ strictly increasing on $[0, \infty)$, $F' = f$ on $(0, \infty)$, and $g' > 0$ on $(0, \infty)$. Differentiability is required only on $(0, \infty)$, so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over $[0, \infty)$. $q^o$ is a parameter with the hypothesis $F(q^o) = (p-c)/(p-v)$; its existence is part of milestone 1.

Readings of informal words: "includes all" means every contract $\{w_1, p\}$ with $c \le w_1 \le p$ has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the $w_2 = p$ family; "any division is achievable" is surjectivity onto $[0, \Pi^o]$; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is $\max\{y, q_s\}$" is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when $w_2 \le p$ (p. 226, "with push $w_2 > p$, so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires $w_1 \ge c$ (p. 228 sets aside $\hat w_1 < c$ as Pareto inferior); pull includes $w_1 = w_2 = p$ (the paper's remark in the proof) and advance-purchase discounts include $w_2 = p$ (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.

Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of $\{w_1, p\}$ as $(y_r, q^o)$ would turn the goal into algebra, and is ruled out.

Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of $S$, and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere and E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• G. P. Cachon and M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019. https://doi.org/10.1002/9781119584445

Motivation

A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.

In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.

Setting

Demand $D$ for the season has law $\mu$ on $\mathbb R$, distribution function $F$ and density $f$. As in §3 of the paper, $F(0) = 0$, $F$ is strictly increasing on $[0,\infty)$, $F' = f$ on $(0,\infty)$, and the generalized failure rate $g(x) = x f(x)/(1 - F(x))$ is strictly increasing (IGFR). The expected sales from $q$ available units are

$$S(q) = q - \int_0^q F(x)\,dx .$$

The retail price is $p$, the unit production cost $c$, the salvage value $v$, with $v < c < p$.

A contract is a pair of wholesale prices $\{w_1, w_2\}$. Before production the retailer submits a prebook order of $y \ge 0$ units at $w_1$. The supplier then produces $q \ge y$. During the season, after running out of prebooked stock, the retailer places at-once orders at $w_2$, filled from the supplier's remaining stock. Pull is $w_1 = w_2 < p$; an advance-purchase discount is $w_1 < w_2$. In §5.1 the supplier pays an extra shipping and handling cost $\tau > 0$ per at-once unit. The profits are

$$\pi_r(y,q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)\bigl(S(q) - S(y)\bigr),$$ $$\pi_s(y,q) = (w_1 - v)y + (w_2 - \tau - v)\bigl(S(q) - S(y)\bigr) - (c - v)q .$$

A supplier best response to $y$ maximizes $\pi_s(y,\cdot)$ over $q \ge y$. An outcome of $\{w_1, w_2\}$ is a pair $(y, q)$ with $q$ a best response to $y$ and $y \ge 0$ maximizing $\pi_r$ when every alternative prebook is followed by a best response to it.

Formalization targets

Goal: Theorem 8

Fix $w_2 < p$ and $\tau > 0$, and suppose the retailer does not prebook under the pull contract $\{w_2, w_2\}$: $y = 0$ is his unique best reply, followed by the supplier's best response $q_0$. Then there is $w_1$ with

$$c < w_1 < w_2$$

such that $\{w_1, w_2\}$ has an outcome, and every outcome $(y, q)$ of it satisfies

$$\pi_r^{\{w_1,w_2\}}(y,q) > \pi_r^{\{w_2,w_2\}}(0,q_0), \qquad \pi_s^{\{w_1,w_2\}}(y,q) > \pi_s^{\{w_2,w_2\}}(0,q_0).$$

Milestones

1. Eq. (22): for $v < w_1 \le w_2 \le p$ the retailer's profit is concave in $y$ and uniquely maximized at $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$, whatever $q$.
2. Eqs. (20)–(21) with $w_2 - \tau$: the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - \tau - c)/(w_2 - \tau - v)$, independent of $w_1$, and $q_s$ is smaller than without the shipping cost.
3. §5.1: for fixed $w_2$ the retailer is never worse off with $w_1 \le w_2$ than with $w_1 = w_2$.
4. $y_r(w_1) > 0$ for every $w_1 < w_2$.
5. The derivative of $w_1 \mapsto \pi_s(y_r(w_1), q)$, where the density at $y_r(w_1)$ is positive:

$$\frac{d\pi_s(y_r(w_1), q)}{dw_1} = y_r(w_1) - \frac{(w_1 - v) - (w_2 - \tau - v)(1 - F(y_r(w_1)))}{(w_2 - v) f(y_r(w_1))}.$$

6. $y_r(w_1) \to 0$ as $w_1 \to w_2$, and, when $f$ has a positive right limit $f(0)$ at $0$, the derivative in 5 tends to $-\tau/((w_2 - v) f(0)) < 0$.

Significance

Without shipping costs, advance-purchase discounts with $w_2 = p$ coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.

The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at $0$ is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.

Difficulty

The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as $w_1 \to w_2$. That limit involves $f(0)$, which the model does not provide: $F$ is differentiable only on $(0, \infty)$, and for gamma demand with shape above $1$ the density vanishes at $0$, so the paper's limit is $-\infty$. A proof of the goal must therefore not rest on the limit display alone.

The second obstacle is the retailer's global choice. The calculus concerns prebooks $y_r(w_1)$ below the supplier's production $q_s$. Once $w_1 < w_2$, the retailer might instead prefer a prebook at least $q_s$, turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for $w_1$ close to $w_2$ requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at $y_r$.

Formalization scope

Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on $(0,\infty)$ only, so the exponential law is admitted. Quantities range over $[0, \infty)$. Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for $w_2 \le p$, and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue $w_2 - \tau$. The prebook function $y_r$ in milestones 5 and 6 is a function pinned on $(v, w_2)$ by Eq. (22), which determines it uniquely.

Readings of the paper's words:

• "the retailer does not prebook when $w_1 = w_2$" is read as "$y = 0$ is the retailer's unique best reply" (every $y > 0$ gives strictly less); with a tie the conclusion can fail;
• "profit increases for both" is read as a strict increase for both firms, in every outcome of the discounted contract;
• the conclusion $c < w_1$ strengthens "advance-purchase discount" ($w_1 < w_2$);
• "reduces the supplier's optimal production" (milestone 2) is a strict decrease; its formula is stated for $c \le w_2 - \tau$;
• "$f(0)$" in milestone 6 is the right limit of $f$ at $0$, assumed positive there only; the positivity of $f(y_r(w_1))$ in milestone 5 is the hypothesis of the implicit-function step;
• "never worse off" (milestone 3) compares every outcome of $\{w_1, w_2\}$ with every outcome of $\{w_2, w_2\}$.

A version of the goal that assumed $f(0) > 0$, assumed $y_r(w_1) < q_s$, compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with $\ge$, would be weaker than Theorem 8 and is not the target.

A complete development needs the concavity and first-order conditions for $S$, the inverse-function derivative for $F$, and the regime comparison between prebooks below and above $q_s$. The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere, E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971

Motivation

Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written $1|r_j|\sum C_j$), the problem is strongly NP-hard, so research has focused on approximation algorithms whose guarantees are stated against every feasible schedule.

The standard route runs through the preemptive relaxation. When jobs may be interrupted and resumed, the shortest-remaining-processing-time rule (SRPT) produces an optimal schedule, and its value is a lower bound for every nonpreemptive schedule. The question is how to turn that preemptive schedule into a nonpreemptive one without losing too much.

Timeline:

• 1995, Phillips, Stein and Wein (WADS 1995, pp. 86–97): order the jobs by their SRPT completion times and schedule them nonpreemptively in that order. This gives a 2-approximation. Later 2-approximations are by Hoogeveen and Vestjens (IPCO 1996), Stougie (1995), and Goemans (SODA 1997). Hoogeveen and Vestjens also showed that deterministic on-line algorithms cannot beat 2.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1)): order by $\alpha$-points instead of completion times, choose $\alpha$ at random, and take the best $\alpha$ off-line. This gives the $e/(e-1)\approx1.58$ bound for Best-$\alpha$ that is the goal of this mission, and an optimal randomized on-line algorithm.
• 1999, Afrati et al. (FOCS 1999): a polynomial-time approximation scheme for $1|r_j|\sum w_jC_j$. This settled the approximability of the problem, but the resulting algorithms are far from simple.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has a processing time $p_j>0$, a release date $r_j\ge0$, and, where the objective is weighted, a weight $w_j>0$. There is one machine.

A nonpreemptive schedule assigns each job a start time $S_j\ge r_j$ such that the intervals $[S_j,S_j+p_j)$ are pairwise disjoint. Its completion times are $C_j=S_j+p_j$.

A preemptive schedule $P$ specifies, for each time $t$, which job runs at $t$, if any. Job $J_j$ runs only at times $t\ge\max(0,r_j)$, receives exactly $p_j$ units of processing in total, and finishes by some finite time. Its completion time $C^P_j$ is the first time by which all of $J_j$ has been processed. For $\alpha\in(0,1]$, its $\alpha$-point $C^P_j(\alpha)$ is the first time by which $\alpha p_j$ units have been processed.

For a job $J_i$, $T_i$ denotes the idle time of $P$ before $C^P_i$. $x_{ij}$ denotes the fraction of $J_j$ processed before $C^P_i$. The paper writes $S^P_i(\beta)$ for the set of jobs with $x_{ij}=\beta$, and also for their total processing time.

One-machine list scheduling in a given order runs the jobs nonpreemptively in that order. Each job starts at the later of its release date and the completion of the previous job in the list. An $\alpha$-schedule is list scheduling in nondecreasing order of the $\alpha$-points $C^P_j(\alpha)$. $C^\alpha_j$ denotes the completion times of an $\alpha$-schedule.

Random-$\alpha$ draws $\alpha$ from a distribution on $(0,1]$ and outputs the $\alpha$-schedule. Best-$\alpha$ outputs the $\alpha$-schedule of smallest total completion time $\min_\alpha\sum_j C^\alpha_j$.

Formalization targets

Goal: Corollary 2.7

Let $P$ be optimal among preemptive schedules for $\sum_j C_j$. Then there is $\alpha\in(0,1]$ such that every $\alpha$-schedule derived from $P$ satisfies

$$\sum_j C^\alpha_j\;\le\;\frac{e}{e-1}\sum_j C_j\qquad\text{for every feasible nonpreemptive schedule } (C_j)_j .$$

Since Best-$\alpha$ returns a schedule no worse than this $\alpha$-schedule, Best-$\alpha$ is an $e/(e-1)$-approximation.

Milestones

1. The calculus behind the constant. For $f(\alpha)=e^\alpha/(e-1)$ and every $\beta\in(0,1]$,

$$\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha=\frac1{e-1}.$$

2. Lemma 2.2: $C^P_i=T_i+\sum_{0<\beta\le1}\beta S^P_i(\beta)$.
3. Lemma 2.3: $C^\alpha_i\le T_i+(1+\alpha)\sum_{\beta\ge\alpha}S^P_i(\beta)+\sum_{\beta<\alpha}\beta S^P_i(\beta)$.
4. Lemma 2.5: if $\alpha$ has density $f$ on $(0,1]$, then $E[C^\alpha_i]\le(1+\delta)C^P_i$ with $\delta=\max_{0<\beta\le1}\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha$.
5. Theorem 2.6, for the weighted objective with $P$ optimal among preemptive schedules: the expected approximation ratio of Random-$\alpha$ is at most $2$ for uniform $\alpha$, at most $1.8$ for $\alpha=1$ w.p. $3/5$ and $\alpha=1/2$ w.p. $2/5$, and at most $e/(e-1)$ for the density $e^\alpha/(e-1)$.

Companion statements, not milestones:

• the upper bound of Theorem 2.1, $\sum_jC^\alpha_j\le(1+1/\alpha)\sum_jC^P_j$;
• the existence of an optimal preemptive schedule.

Significance

The $e/(e-1)$ bound shows that conversion from the preemptive relaxation can beat the factor 2 of the natural ordering. It does so by exploiting that no single instance is bad for many values of $\alpha$ at once. The $\alpha$-point technique was also used with LP relaxations, for example by Goemans (SODA 1997) and by Schulz and Skutella. The randomized version is an optimal randomized on-line algorithm for $1|r_j|\sum C_j$. Lemma 2.3 is a statement about any preemptive schedule, so it applies wherever a good preemptive or fractional schedule is available.

All results of the mission are proved in the paper, except that the proof of Theorem 2.6, part 2 is omitted there. No machine-checked proof of them is known. A complete development would give a verified model of preemptive one-machine schedules, $\alpha$-points and list scheduling, together with the averaging argument over $\alpha$. These are reusable for the later results of the same paper and for the $\alpha$-point literature.

Difficulty

The obvious argument bounds each job's $\alpha$-schedule completion time directly against its preemptive completion time. That argument loses a factor $1+1/\alpha$ (Theorem 2.1), which is at least 2 for every fixed $\alpha$. The improvement needs Lemma 2.3. There the charge to each job depends on how much of it was done by $C^P_i$ relative to $\alpha$, and the idle time $T_i$ is not inflated at all. Proving Lemma 2.3 requires reasoning about a preemptive schedule as a measure on time, and about how moving pieces of jobs changes completion times. A proof that treats the preemptive schedule as a finite list of pieces must first show that nothing is lost by this discretization.

The averaging step needs the expectation over $\alpha$ to be an honest integral. The map $\alpha\mapsto C^\alpha_i$ must be shown integrable, which requires a fixed rule for ties between equal $\alpha$-points.

Formalization scope

• Model. Jobs are Fin n, time is real, $p_j>0$ and $r_j\ge0$. The paper admits $p_j=0$ only in its tightness instances.
  • A preemptive schedule is a function $\sigma:\mathbb R\to$ Option (Fin n) (none = idle). Each job's run set is measurable, lies in $[\max(0,r_j),\infty)$, is bounded above, and has Lebesgue measure $p_j$.
  • Completion times and $\alpha$-points are infima of nonempty sets that are bounded below.
  • $T_i$ is the measure of the idle set in $[0,C^P_i)$.
  • The paper's sums over $\beta$ are sums over jobs, weighted by the fraction $x_{ij}$.
• List scheduling is strict: jobs never overtake the list order, and the machine is free from time $0$.
  • Lemma 2.3, Theorem 2.1, Theorem 2.6.2 and the goal hold for every tie-break among equal $\alpha$-points.
  • The expectations (Lemma 2.5, Theorem 2.6.1 and 2.6.3) use the tie-break by job index. They assert integrability as part of the conclusion.
• Optimality. "Approximation ratio $c$" is stated as an inequality against every feasible nonpreemptive schedule, never against an infimum.
  • The optimality of $P$ among preemptive schedules is the paper's standing assumption for its upper bounds (p. 151). It appears as a hypothesis of Theorem 2.6 and of the goal.
  • The lemmas hold for arbitrary $P$ and do not carry it.
  • An existence statement shows the hypothesis can be met.
• Lemma 2.5's $\delta$ is replaced by any upper bound of the integrals over $\beta\in(0,1]$. This is equivalent, and it avoids assuming that the maximum is attained.
• Not stated:
  • the running time $O(n^2)$ of Best-$\alpha$ and the optimality of SRPT;
  • the tightness parts of Theorem 2.1 and Corollary 2.4, and the lower bounds of Theorem 2.9, which use zero-length jobs;
  • the on-line Theorem 2.8, which needs a model of on-line algorithms.
• Trivializing formalization ruled out. Dropping the optimality of $P$ from the goal would turn it into a statement about arbitrary preemptive schedules, which is Lemma 2.5, not Corollary 2.7. Comparing against $\sum_jC^P_j$ instead of every nonpreemptive schedule would likewise remove the content of the corollary.

Contributions are welcome at every level. The calculus milestone and Lemma 2.2 are good first targets.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• C. Phillips, C. Stein, J. Wein, Scheduling jobs that arrive over time, Proc. 4th Workshop on Algorithms and Data Structures (WADS), 1995, pp. 86–97 (reference [25] of the paper; no link verified).
• J. A. Hoogeveen, A. P. A. Vestjens, Optimal on-line algorithms for single-machine scheduling, Proc. 5th IPCO, 1996, pp. 404–414 (reference [21]; no link verified).
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 1997, pp. 591–598 (reference [12]; no link verified).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th FOCS, 1999 (reference [2]; no link verified).

Motivation

Minimizing the average completion time of jobs that arrive over time is a basic objective in machine scheduling. It measures how long a job spends in the system on average. With several identical machines, release dates and no preemption (written $P|r_j|\sum C_j$), the problem is strongly NP-hard already on one machine. Research has therefore looked for approximation algorithms: polynomial-time rules whose total completion time is provably within a constant factor of every feasible schedule.

A common approach solves a relaxation that is easy to optimize and converts its solution into a feasible schedule. Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) use a relaxation that needs neither linear programming nor dynamic programming: pretend that the $m$ machines are one machine that is $m$ times as fast, and allow preemption.

Timeline:

• 1996, Chakrabarti, Phillips, Schulz, Shmoys, Stein and Wein (ICALP 1996, LNCS 1099, pp. 646–657): a $(2.89+\epsilon)$-approximation for $P|r_j|\sum C_j$.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), §3 and §4.5). §3 gives a simple $(3-1/m)$-approximation by list scheduling from the one-machine relaxation. §4.5 combines it with the Delay List conversion to obtain $2\sqrt2\approx2.83$. This mission's goal is the §4.5 result.
• 1999, Afrati, Bampis, Chekuri, Karger, Kenyon, Khanna, Milis, Queyranne, Skutella, Stein and Sviridenko (FOCS 1999, pp. 32–43): polynomial-time approximation schemes for $P|r_j|\sum w_jC_j$. These settle the approximability, but the algorithms are far more involved than the ones formalized here.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$ and $m\ge1$ identical machines. Job $J_j$ has a processing time $p_j>0$ and a release date $r_j\ge0$.

A feasible schedule gives each job a start time $S_j\ge r_j$ and a machine. Job $J_j$ runs without interruption on its machine during $[S_j,S_j+p_j)$, and two jobs on the same machine never overlap. The completion times are $C_j=S_j+p_j$ and the objective is $\sum_j C_j$. $C^*_j$ denotes the completion times of an arbitrary feasible schedule, against which every bound is stated.

The one-machine relaxation $I1$ has the same jobs and a single machine. Job $J_j$ has processing time $p_j/m$ and release date $r_j$ in $I1$, and may be preempted. A preemptive schedule $P1$ of $I1$ gives each job a processing rate $\rho_j(t)\ge0$. The rates sum to at most $1$ at each time, and no job is processed before its release date. Each job receives $p_j/m$ units in total. Its completion time $C^{P1}_j$ is the first time by which all of it has been processed. $P1$ is optimal if $\sum_j C^{P1}_j$ is minimal among all such schedules.

A list is an ordering $\pi$ of the jobs, and the completion order of $P1$ lists the jobs by nondecreasing $C^{P1}_j$. Two ways of turning a list into an $m$-machine schedule are compared.

• Strict-order list scheduling gives the schedule $N$. The jobs start in the order of the list. Each job starts at the earliest time that is no earlier than its release date, no earlier than the previous job's start, and at which some machine is free.
• Delay List with parameter $\beta>0$ gives the schedule $D$. When a machine is idle, Delay List starts the first unscheduled job of the list if it has been released. If that job has not been released, the first released job of the list may jump ahead, but only once at least $\beta p_j$ units of idle time (machine × time) have accumulated that no earlier job has charged. The job then charges exactly that amount. A job started in list order charges all uncharged idle time since its release.

Formalization targets

Goal: Lemma 4.19

With $P1$ optimal, $\pi$ its completion order, $N$ the strict-order list schedule of $\pi$ and $D$ a Delay List schedule of $\pi$ with $\beta_0=\sqrt{3-2\sqrt2}$, every feasible schedule satisfies

$$\min\Bigl(\sum_j C^N_j,\ \sum_j C^D_j\Bigr)\le 2\sqrt2\,\sum_j C^*_j .$$

The printed lemma says $2.83$. Its proof gives $2\sqrt2\approx2.8284$, which is stated here.

Milestones

In the order the proof uses them:

1. (4.2): if $\sum_j p_j>\alpha\sum_j C^*_j$ then $\sum_j r_j\le(1-\alpha)\sum_j C^*_j$.
2. Lemma 3.1: $\sum_j C^{P1}_j\le\sum_j C^*_j$ for $P1$ optimal.
3. (3.3): $\sum_j C^N_j\le 2\sum_j C^{P1}_j+(1-1/m)\sum_j p_j$ for any $P1$.
4. Lemma 3.2: $\sum_j C^N_j\le(3-1/m)\sum_j C^*_j$.
5. Theorem 4.9, specialised to no precedence constraints. With $B_i$ the jobs at or before $J_i$ in the list,

$$C^D_i\le\frac{(1+\beta)p(B_i)}{m}+\Bigl(1+\frac1\beta\Bigr)(r_i+p_i)-\frac{p_i}{\beta}.$$

6. Lemma 4.18: $\sum_j C^D_j\le(2+\beta)\sum_j C^*_j+\frac1\beta\sum_j r_j$.
7. The balanced bound: under (4.2)'s hypothesis, $\sum_j C^D_j\le(2+\beta+(1-\alpha)/\beta)\sum_j C^*_j$.
8. The constants: at $\alpha=2\sqrt2-2$ and $\beta=\sqrt{3-2\sqrt2}$, $2+\alpha=2+\beta+(1-\alpha)/\beta=2\sqrt2$.

Two existence statements accompany them. One says an optimal $P1$ exists. The other says a Delay List schedule exists for every list and every $\beta>0$.

Significance

The result gives a $2\sqrt2$-approximation for $P|r_j|\sum C_j$ that is simple to state and runs in $O(n\log n)$ time. It improves the $2.89+\epsilon$ bound of Chakrabarti et al. Neither of its two algorithms achieves the ratio alone. It comes from an analysis in which each algorithm is good exactly when the other is bad. List scheduling is good when processing times are small relative to the optimum. Delay List is good when release dates are small. The inequality (4.2) connects the two cases.

The component results are reusable beyond this paper. The one-machine relaxation lower bound (Lemma 3.1) and the $(3-1/m)$ bound for list scheduling from it (Lemma 3.2) apply to any conversion from a fast single machine. The per-job bound of Theorem 4.9 is the core of the Delay List technique. Its general form, with precedence constraints, drives the paper's results for precedence-constrained scheduling.

All results are proved in the paper. None of them has a machine-checked proof that this mission knows of. A formalization would check the Delay List charging argument, which the paper states only in discrete time and adapts to continuous time in one sentence. It would also produce reusable Lean definitions of parallel-machine schedules with release dates and of list scheduling.

Difficulty

The arithmetic of the goal is routine once the milestones are in place. The substance lies in two places.

The first is Lemma 3.1 together with the "standard makespan argument" behind (3.2). The one-machine relaxation must be related to the $m$-machine schedule, and to the list schedule, with care about release dates. In particular, in the list schedule every machine is busy between the last release among the first $j$ jobs of the list and the start of the $j$-th job. Proving this needs the strict order.

The second, and harder, is Theorem 4.9. The obvious argument bounds the waiting time of job $J_i$ by the work of the jobs ahead of it, but Delay List lets later jobs jump ahead. The idle time before $J_i$ starts and the work of the jobs that jump ahead of it must both be controlled, and the paper's charging argument for this depends on where charged idle time lies on the time axis and on which jobs charged it. Making that bookkeeping precise for a continuous-time algorithm is the main formalization cost.

Formalization scope

Jobs are Fin n and machines Fin m with $m\ge1$. Times are real, processing times are positive and release dates nonnegative. There are no weights and no precedence constraints. "Optimal" is never an infimum. Every bound is stated against every feasible nonpreemptive schedule, and $P1$'s optimality is the hypothesis that its total completion time is at most that of every preemptive schedule of $I1$.

Committed conventions:

• Preemptive schedules of $I1$ are rate functions, so the machine of $I1$ may be shared. The paper's one-job-at-a-time schedules are a special case.
• Lists are bijections Fin n ≃ Fin n. A list of $P1$ may break ties in completion time in any way, and every such list is covered.
• $N$ is the strict-order variant of list scheduling, which footnote 3 of the paper contrasts with the greedy variant used in §4. It is a recursive definition over list positions.
• Delay List is the continuous-time algorithm, as adopted in the proof of Fact 4.6. It is a predicate on start times, machines, the scheduling order and charge windows. A job scheduled out of order takes its charge from the most recent uncharged idle time; the paper leaves this placement open. Theorem 4.9 and Lemma 4.18 assume $m\ge2$, the setting of §4.1. The goal assumes only $m\ge1$.
• The printed Lemma 4.18 lacks a $\sum_j$ on the $C^*$ term. The summed form of its proof's last display is stated.

The statement cannot be made easy by the hypotheses. Two existence items show that an optimal $P1$ and a Delay List schedule always exist, so no statement is vacuous. The bound is against every feasible schedule, not against the relaxation's value.

Not stated: the $O(n\log n)$ running time, the on-line version of §3's algorithm, and Delay List with precedence constraints (Theorem 4.9 in general, which is the subject of mission III of this series). Contributions welcome: proofs of the milestones, and reusable lemmas on list scheduling with release dates.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• S. Chakrabarti, C. A. Phillips, A. S. Schulz, D. B. Shmoys, C. Stein, J. Wein, Improved scheduling algorithms for minsum criteria, in Proceedings of ICALP 1996, LNCS 1099, Springer, pp. 646–657 (reference [3] of the paper).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, in Proceedings of the 40th IEEE FOCS, 1999, pp. 32–43 (reference [2] of the paper).

Motivation

Minimizing the sum of weighted completion times $\sum_j w_jC_j$ is one of the standard objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. With release dates or precedence constraints the problem is NP-hard already on one machine, and on $m$ identical parallel machines it is harder still, so the literature of the 1990s concentrated on approximation algorithms. Many of these, including LP-based ones, are naturally designed for a single machine, where an order of the jobs determines the schedule.

Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) gave a generic way to move from one machine to many. Their §4 describes an algorithm, Delay List, that takes any one-machine schedule as a priority list and produces an $m$-machine schedule, and proves that a $\rho$-approximate one-machine schedule yields a $\bigl((1+\beta)\rho+1+1/\beta\bigr)$-approximate $m$-machine schedule for every $\beta>0$. The guarantee holds with release dates and arbitrary precedence constraints simultaneously, which at the time gave the best bounds known for several special cases, for example a factor 4 for series-parallel precedence without release dates.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has processing time $p_j>0$, release date $r_j\ge 0$ and weight $w_j>0$. Precedence constraints form a strict partial order $\prec$: $i\prec j$ means that $J_j$ may start only after $J_i$ completes.

A feasible nonpreemptive schedule on $m$ machines assigns each job a start time $S_j$ and a machine; each job runs uninterrupted for $p_j$ time units on its machine, two jobs on one machine do not overlap, $S_j\ge r_j$, and $S_i+p_i\le S_j$ whenever $i\prec j$. The completion time is $C_j=S_j+p_j$ and the value of the schedule is $\sum_j w_jC_j$. A one-machine schedule is the case $m=1$.

The critical-path length $\kappa_j$ (Definition 4.1) is $p_j+r_j$ for a job without predecessors and $p_j+\max\{\max_{i\prec j}\kappa_i,\,r_j\}$ otherwise; it is the earliest time $J_j$ could complete with unlimited machines.

A list is an ordering $\pi$ of the jobs. Delay List with parameter $\beta>0$ processes time continuously. A job is ready once it is released and all its predecessors have completed; $q^m_j$ is the time it becomes ready. The head is the first unscheduled job of the list. Idle machine-time is recorded as charged to jobs. Whenever a machine is idle:

1. if the head is ready, it is started, and charged all uncharged idle time in $(q^m_j,s^m_j)$;
2. otherwise the first ready job $J_k$ of the list is started as soon as at least $\beta p_k$ units of uncharged idle time have accumulated, and is charged $\beta p_k$ of it;
3. otherwise nothing happens.

For a job $J_i$, $B_i$ is the set of jobs up to and including $J_i$ in the list, $A_i$ the set after it, $O_i\subseteq A_i$ the set of jobs of $A_i$ started before $J_i$, and $p(A)=\sum_{k\in A}p_k$. Definition 4.4 builds from the schedule a backward path $P'_i$ ending at $J_i$, whose length is $\kappa'_i$.

Formalization targets

Goal: Theorem 4.13

Let $S^1$ be a feasible one-machine schedule of the instance with $\sum_j w_jC^1_j\le\rho\sum_j w_jC'_j$ for every feasible one-machine schedule $C'$. Let $m\ge 2$ and $\beta>0$. Every Delay List schedule $S^m$ built on the completion order of $S^1$ satisfies, for every feasible $m$-machine schedule $N$,

$$\sum_j w_jC^m_j\le\Bigl((1+\beta)\rho+1+\frac1\beta\Bigr)\sum_j w_jC^N_j .$$

Milestones, in the order the proof uses them

• Fact 4.5: $\kappa'_i\le\kappa_i$.
• Fact 4.6: the idle time charged to $J_i$ is at most $\beta p_i$.
• Lemma 4.7: no uncharged idle time remains in $(q^m_i,s^m_i)$, and that idle time is charged only to jobs in $B_i$.
• Lemma 4.8: the idle time charged to $A_i$ within $(0,s^m_i)$ is at most $m(\kappa'_i-p_i)$, so $p(O_i)\le m(\kappa'_i-p_i)/\beta\le m(\kappa_i-p_i)/\beta$.
• Theorem 4.9: $C^m_i\le(1+\beta)p(B_i)/m+(1+1/\beta)\kappa'_i-p_i/\beta$ for any list obeying precedence.
• Lemma 4.10: $C^m_{\mathrm{OPT}}\ge C^1_{\mathrm{OPT}}/m$.
• Lemma 4.11: $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$.
• Corollary 4.12: $C^m_i\le(1+\beta)C^1_i/m+(1+1/\beta)\kappa_i$ when the list is the completion order of $S^1$.

A further item states that a Delay List schedule exists for every instance and every list, so that the goal does not hold vacuously.

Significance

The result. Theorem 4.13 turns every one-machine approximation algorithm for weighted completion time with release dates and precedence into an $m$-machine algorithm at a bounded loss. With an optimal one-machine schedule and $\beta=1$ the factor is $4$ (Corollary 4.14, for series-parallel orders), and the bounds are job-by-job (Theorem 4.9, Corollary 4.12), which the paper uses in Remark 4.15 to extend the method to other metrics and to one-machine schedules that ignore release dates. The same algorithm is the engine of the paper's $2\sqrt2$-approximation for parallel machines with release dates (§4.5).

Formalizing it. The theorem has been proved since 1997 (SODA) and 2001 (journal). There is no machine-checked version of it or of any of its lemmas, and the platform currently has no model of scheduling with release dates and precedence constraints. A formalization produces a precise specification of Delay List, whose informal description is given in discrete time and repaired in a remark; a checked proof of the charging argument; and reusable lower bounds (Lemmas 4.10 and 4.11) for any later work on parallel-machine scheduling with precedence.

Difficulty

The obvious attempt, list scheduling (start the first available job of the list whenever a machine is free), fails with non-identical processing times: a long job taken out of order can occupy a machine and delay a more valuable job that becomes ready shortly afterwards. Delay List allows out-of-order jobs only against accumulated idle time, and the analysis rests on a charging invariant. Stating it needs care about time (the paper's discrete-time exposition can over-charge by a time unit), about which idle time a charge consumes, and about many jobs being scheduled at one instant. The bound must hold simultaneously for release dates and arbitrary precedence constraints, where idle machines can be forced both by jobs that are not yet released and by chains of predecessors, and it must hold for every tie-breaking choice of the algorithm.

Formalization scope

Jobs are Fin n, machines Fin m, and times are real numbers. Processing times are positive, release dates nonnegative and weights positive, as in §1. Precedence is a strict partial order, the transitive closure of the paper's DAG; $\kappa$, readiness and feasibility are unchanged by taking the closure. The optimum is never a real infimum: "within a factor $\rho$ of an optimal one-machine schedule" and "within a factor $c$ of an optimal $m$-machine schedule" are inequalities against every feasible schedule of the same instance, with the same release dates and precedence constraints.

Delay List is formalized in the continuous-time version described in the proof of Fact 4.6, as a predicate on runs that records start times, machines, the order in which jobs are scheduled at equal times, and charge windows. A case-2 charge takes the most recent uncharged idle time, and idle time is charged by whole time slices. Every guarantee is claimed for every run satisfying the predicate. The ties in Definition 4.4 are broken arbitrarily, so statements involving $\kappa'_i$ hold for every admissible path. Lemma 4.10 uses nonpreemptive one-machine schedules. Lemma 4.11's $C^\infty_{\mathrm{OPT}}$ is modelled by $n$ machines.

It would be trivializing to assume the conclusions of Fact 4.6 or Lemma 4.7 as properties of the run, or to measure $\rho$ against a relaxation without release dates or precedence; both are ruled out. The algorithm's rules are the only hypotheses on the run.

Not stated: the running time of Delay List; the discrete-time algorithm; Corollary 4.14 (it needs a formal class of series-parallel orders and the external one-machine algorithm of Adolphson for them); Remark 4.15 (release-date-free one-machine schedules), whose hypotheses the paper does not pin down; and the extension to delays between jobs. Contributions of general infrastructure, such as idle-time accounting for step functions and lemmas about list schedules under precedence, are welcome and reusable beyond this mission.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM Journal on Computing 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45:1563–1581, 1966. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
• D. Adolphson, Single machine job sequencing with precedence constraints, SIAM Journal on Computing 6(1):40–54, 1977. https://doi.org/10.1137/0206002

Motivation

Minimizing the sum of weighted completion times of jobs on identical parallel machines is one of the basic objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. When the jobs are subject to precedence constraints (a job may start only after certain other jobs have finished), the problem is strongly NP-hard already in very restricted cases, and the question becomes how close to optimal a polynomial-time algorithm can guarantee to be.

Chekuri, Motwani, Natarajan and Stein, Approximation Techniques for Average Completion Time Scheduling (SIAM J. Comput. 31(1), 2001, doi:10.1137/S0097539797327180), develop a general way to turn a good schedule for a single machine into a good schedule for $m$ machines. For arbitrary precedence constraints their conversion (Delay List, §4.1–4.3) loses a factor $(1+\beta)\rho+(1+1/\beta)$ over a $\rho$-approximate one-machine schedule, which is $4$ when the one-machine schedule is optimal. In §4.4 they show that for in-tree precedence without release dates, the plain list-scheduling rule of Graham, fed with an optimal one-machine schedule, already achieves ratio $2$. In-trees are the precedence structures of assembly processes: every job feeds into at most one later job.

Timeline of the relevant results:

• 1966–1969: Graham introduces list scheduling on parallel machines and analyzes it for makespan (Graham 1969).
• 1972: Horn gives a polynomial-time optimal one-machine algorithm for weighted completion time under treelike precedence (Horn 1972).
• 1977: Adolphson gives $O(n\log n)$ one-machine algorithms for tree and series-parallel precedence (Adolphson 1977, the paper's reference [1]).
• 2001: Chekuri, Motwani, Natarajan and Stein prove the ratio-$2$ bound for in-trees on $m$ machines (Theorem 4.17).

Setting

There are $n$ jobs $J_0,\dots,J_{n-1}$ and $m\ge 1$ identical machines. Job $J_j$ has a processing time $p_j>0$ and a weight $w_j>0$; every job is available at time $0$ (there are no release dates).

The precedence constraints form an in-tree (more generally, an in-forest): every job $j$ has at most one immediate successor $\operatorname{succ}(j)$, and following successors never returns to the start. Write $i\prec j$ if $j$ is reached from $i$ by following successors one or more times.

A feasible schedule $S^m$ on $m$ machines gives each job a start time $S_j\ge 0$ and a machine; a job runs without interruption for $p_j$ time units; two jobs on the same machine do not overlap; and $i\prec j$ implies that $j$ starts no earlier than $i$ completes. The completion time is $C^m_j=S_j+p_j$ and the value of the schedule is $\sum_j w_jC^m_j$.

The critical-path length $\kappa_j$ (Definition 4.1 with no release dates) is $\kappa_j=p_j$ if $j$ has no predecessors and $\kappa_j=p_j+\max_{i\prec j}\kappa_i$ otherwise.

A list is an ordering $\pi$ of the jobs that obeys the precedence constraints. It defines the one-machine schedule $S^1$ that runs the jobs in list order without idle time; its completion times are $C^1_j$, the total processing time of the jobs up to and including $j$ in the list. An optimal one-machine schedule is a list minimizing $C^1=\sum_j w_jC^1_j$.

List scheduling (Graham's rule, footnote 3 of the paper) on $m$ machines with list $\pi$: whenever a machine is free, start on it the first job of the list that is ready, i.e. whose predecessors have all completed.

Formalization targets

Goal: Theorem 4.17

Let $\pi$ be an optimal one-machine schedule and $G$ the list schedule on $m$ machines with list $\pi$. Then for every feasible $m$-machine schedule $N$,

$$\sum_j w_jC^G_j\ \le\ 2\sum_j w_jC^N_j .$$

Milestones

Lemma 4.16 (any precedence-respecting list $\pi$, with its idle-free one-machine schedule $S^1$): for every job $i$,

$$C^G_i\ \le\ \kappa_i+\frac{C^1_i}{m}.$$

Lemma 4.10: $C^m_{\mathrm{OPT}}\ge C^1_{\mathrm{OPT}}/m$, i.e. $\sum_j w_jC^1_j/m\le\sum_j w_jC^N_j$ for an optimal list and every feasible $N$.

Lemma 4.11: $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$, i.e. $\sum_i w_i\kappa_i\le\sum_i w_iC^N_i$ for every feasible $N$ on any number of machines, and the value $\sum_i w_i\kappa_i$ is attained by a feasible schedule on $n$ machines.

Significance

The result. Theorem 4.17 gives a simple, fast algorithm with a guaranteed factor $2$ for a strongly NP-hard problem, halving the factor $4$ that the general Delay List conversion gives for the same class. The per-job bound of Lemma 4.16 is stronger than the aggregate statement: every single job completes within its critical-path length plus a $1/m$ share of its one-machine completion time, so the same bound applies to other objectives built from completion times.

Formalizing it. The paper's proof is complete and short, but it argues about events at a time $t$ (jobs that finish exactly at $t$, jobs that become ready at $t$, machines freed at $t$) and runs an induction over jobs ordered by start time with an invariant about idle time. A machine-checked version fixes what "list scheduling" means precisely, pins down the counting argument that uses the in-tree structure, and yields reusable definitions of nonpreemptive parallel-machine schedules, critical paths and list schedules. To the knowledge of this mission, none of these results has a machine-checked proof.

Difficulty

List scheduling may start a job that is late in the list before an earlier one, because the earlier job is not yet ready; so the one-machine order is not preserved and the obvious comparison with $S^1$ fails. Idle machines are the other obstacle: a machine can stay idle while a job waits for its predecessors, and a per-job bound of the form $\kappa_i+C^1_i/m$ holds only if such idle time can be accounted for by $J_i$'s own chain of predecessors. For general precedence constraints, and for out-trees (every job has at most one immediate predecessor), the paper's accounting breaks down, and the paper states the per-job bound only for in-trees; the in-tree structure is essential to the argument. Events with several jobs finishing at the same instant, and ties in start times, have to be handled without loss.

Formalization scope

• Jobs are Fin n, machines Fin m, times real numbers. Processing times and weights are strictly positive. There are no release dates: start times are nonnegative. The paper admits $p_j=0$ only in lower-bound instances elsewhere; the bounds here assume $p_j>0$.
• In-trees are encoded by an immediate-successor map succ : Fin n → Option (Fin n) with no cycles; this covers in-forests, the reading of "in-trees" in Theorem 4.17. The precedence relation is its transitive closure.
• $\kappa$ is defined by well-founded recursion on the precedence order, exactly as Definition 4.1 with $r\equiv 0$.
• One-machine schedules are represented by their precedence-respecting order and are idle-free; with no release dates and positive processing times idle time only delays jobs, so optimality among orders is optimality among one-machine schedules. The optimal one-machine schedule is a hypothesis of the goal; the paper's $O(n\log n)$ algorithm for computing it (reference [1]) is not formalized, and the running-time claim of Theorem 4.17 is not stated. A separate item asserts that an optimal order exists.
• List scheduling is specified by two properties that determine Graham's rule up to machine labels: no machine is idle while a ready job waits, and among jobs ready at a start time the earlier one in the list starts first. A separate item asserts that such a schedule exists for every precedence-respecting list, so the goal is not vacuous.
• Optima are never formed as infima: the approximation ratio is stated against every feasible schedule. A statement of the form "there is an algorithm with ratio 2" would be trivial (an optimal schedule exists) and is ruled out: the goal is about the paper's algorithm.
• The equality $\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$ in Lemma 4.11 is stated as attainment on $n$ machines (as many machines as jobs), which together with the lower bound on every number of machines is the optimum with unboundedly many machines.

Welcome contributions: proofs of the two existence items (Graham's list schedule by event-driven construction; an optimal order over the finite set of linear extensions), of Lemmas 4.10 and 4.11, and of Lemma 4.16. The schedule and list-scheduling definitions are reusable for other parallel-machine results with precedence constraints.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• R. L. Graham, Bounds on multiprocessing timing anomalies, SIAM J. Appl. Math. 17(2):416–429, 1969. https://doi.org/10.1137/0117039
• W. A. Horn, Single-machine job sequencing with treelike precedence ordering and linear delay penalties, SIAM J. Appl. Math. 23(2):189–202, 1972. https://doi.org/10.1137/0123021
• D. L. Adolphson, Single machine job sequencing with precedence constraints, SIAM J. Comput. 6(1):40–54, 1977. https://doi.org/10.1137/0206002

Motivation

Many combinatorial optimization problems ask for the best subset of a finite set subject to combinatorial side conditions. The polyhedral method replaces the finite family of feasible subsets by the convex hull of their incidence vectors and asks for an explicit system of linear inequalities describing that convex hull; once such a system is known, linear programming duality gives min–max theorems and certificates of optimality. The maximum weight stable set problem is the central test case: it is NP-hard in general, so no tractable complete description of its polytope is expected for all graphs, and the question becomes for which graphs a simple description suffices.

V. Chvátal's 1975 paper On certain polytopes associated with graphs answers this question for the two simplest families of valid inequalities, and its Section 3 connects the answer to Berge's perfect graphs. The result is a standard entry point to polyhedral combinatorics and is one of the ingredients behind the later polynomial-time algorithms for stable sets in perfect graphs by Grötschel, Lovász and Schrijver.

Timeline. Berge (1961) introduced perfect graphs and conjectured that a graph is perfect if and only if its complement is. Lovász (Normal hypergraphs and the perfect graph conjecture, Discrete Math. 1972; A characterization of perfect graphs, J. Combin. Theory Ser. B 1972) proved this, together with the characterization of perfection by $\alpha(G_A)\,\omega(G_A)\ge|A|$ and the invariance of perfection under vertex duplication. Fulkerson's theory of antiblocking polyhedra (1971–72) gave a polyhedral route to the same equivalence. Chvátal (received 1972, published 1975) gave the self-contained polyhedral statement formalized here, with a proof based on Lovász's two theorems.

Setting

A graph $G=(V,E)$ is finite, undirected and loopless. A stable set is a set of vertices no two of which are adjacent. A clique is a maximal complete subgraph, and $C(G)$ is the set of vertex sets $W\subseteq V$ of the cliques of $G$.

$S(G)\subseteq\mathbb R^V$ is the set of zero–one vectors $x=(x_u:u\in V)$ such that $\{u:x_u=1\}$ is stable, and the stable set polytope is $P(G)=\operatorname{conv}S(G)$. A finite system of linear inequalities is a defining linear system of $P(G)$ if its solution set is exactly $P(G)$. For $c\in\mathbb R^V$ write $cx=\sum_{u\in V}c_ux_u$.

$G$ is perfect (the paper's $\alpha$-perfect) if for every zero–one vector $c$,

$$\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\ \lambda_W\in\{0,1\},\ \sum_{W\in C(G),\,u\in W}\lambda_W\ge c_u\ (u\in V)\Big\}.$$

For $A\subseteq V$, $G_A$ is the induced subgraph, $\alpha(G_A)$ its stability number and $\omega(G_A)$ its clique number. To duplicate a vertex $u$ is to add a new vertex $u'$ adjacent to all neighbours of $u$ but not to $u$.

In the Lean development these are stableVectors G, stablePolytope G, maximalCliques G, IsPerfect G and duplicate G u in the namespace ChvatalPolytopes.Perfect.

Formalization targets

Goal: Theorem 3.1 (p. 140)

For every graph $G$, the system

$$-x_u\le0\quad(u\in V),\qquad\sum_{u\in W}x_u\le1\quad(W\in C(G))$$

is a defining linear system of $P(G)$ if and only if $G$ is perfect. Both directions are required.

Milestones

1. Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$, $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$, the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.$$

2. Lovász's first theorem (§3, p. 140). Every nonperfect $G$ has $A\subseteq V$ with $\alpha(G_A)\,\omega(G_A)<|A|$.
3. Lovász's second theorem (§3, p. 140). Duplicating a vertex of a perfect graph gives a perfect graph.
4. Condition (iii) (p. 141). $G$ is perfect if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\lambda_W\ge0,\ \sum_{W\ni u}\lambda_W\ge c_u\ (u\in V)\Big\}.$$

Significance

The result. The nonnegativity and clique inequalities are valid for $P(G)$ for every graph. Theorem 3.1 says they are complete exactly for perfect graphs, so on perfect graphs the maximum weight stable set problem is a linear program over an explicitly described polytope, and weighted min–max theorems (stable sets versus clique covers) follow from LP duality. Combined with the perfect graph theorem, it gives a polyhedral characterization of perfect graphs, and it is the model for later results that identify graph classes by the facets of their stable set polytopes (odd-cycle inequalities, $t$-perfection, Section 7 of the same paper).

Formalizing it. The result is classical and proved. No machine-checked version of it is known, and Mathlib has neither perfect graphs nor stable set polytopes. The mission produces a formal statement of the polyhedral characterization with the paper's own notion of perfection, a formal version of the convex-hull/LP min–max principle (Proposition 2.1), which is reusable for any 0–1 polytope, and formal statements of the two theorems of Lovász that the proof relies on.

Difficulty

Proposition 2.1 reduces Theorem 3.1 to the equivalence of perfection with a fractional min–max for all integer weights. The obvious approach to that equivalence fails in both directions. From perfection one only gets the min–max for zero–one weights and zero–one multipliers; general integer weights do not reduce to zero–one weights by linearity, because the minimum over clique covers is not additive in $c$. Conversely, a fractional clique cover of value $\alpha$ does not directly produce an integral one. The paper crosses this gap with two theorems of Lovász: a numerical certificate of nonperfection, and the invariance of perfection under vertex duplication. Both are substantial graph-theoretic results in their own right, and neither follows from the definitions by routine manipulation.

Proposition 2.1 itself needs separation of a point from a polytope by an integral objective and LP strong duality with the nonnegativity rows handled separately.

Formalization scope

Vertices form a finite type V with decidable equality; a graph is a SimpleGraph V. $S(G)$ is a set of functions V → ℝ, and $P(G)$ is Mathlib's convexHull ℝ of it. $C(G)$ is the finset of finsets that are maximal among cliques (Maximal), as on the page; with $V=\emptyset$ the only maximal clique is $\emptyset$. "Defining linear system" is an equality of sets. Every "max = min" is written out in full: there is a value $m$ that is the maximum over $S$ (attained and an upper bound), some feasible multiplier vector attains $m$, and every feasible multiplier vector has objective at least $m$. Clique multipliers are functions Finset V → ℝ read only on $C(G)$.

Explicit conventions and added hypotheses:

• In Proposition 2.1 the index set $J$ is a finite type, coefficients are real, the nonnegativity rows are kept as a separate conjunct $x\ge0$, and $S$ is assumed nonempty (the paper's $\max$ over $S$ needs it).
• $\alpha$ and $\omega$ are Mathlib's indepNum and cliqueNum (natural numbers) of G.induce A.
• The duplicated graph lives on Option V, with none the new vertex.

Perfection is the paper's zero–one min–max, not "the clique system defines $P(G)$" (which would make the goal a tautology) and not Berge's $\chi(G_A)=\omega(G_A)$ (a different definition, equivalent only through the perfect graph theorem). $P(G)$ is the convex hull of $S(G)$, never the solution set of an inequality system.

Needed infrastructure, all reusable: integral separation from a rational polytope and LP strong duality in the form $\max\{cx:Ax\le b,x\ge0\}=\min\{\lambda b:\lambda A\ge c,\lambda\ge0\}$; basic facts about stable sets and maximal cliques of induced subgraphs and of duplicated graphs; invariance of IsPerfect under graph isomorphism and under taking induced subgraphs. Proofs of the Lovász milestones, which have independent value for a Mathlib theory of perfect graphs, are welcome.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
• L. Lovász, A characterization of perfect graphs, J. Combin. Theory Ser. B 13 (1972) 95–98. https://doi.org/10.1016/0095-8956(72)90045-7
• D. R. Fulkerson, Anti-blocking polyhedra, J. Combin. Theory Ser. B 12 (1972) 50–71. https://doi.org/10.1016/0095-8956(72)90032-9
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4