Operations Research

Motivation

Every manufacturer who makes a part in batches faces the trade-off Ford W. Harris described in 1913: large lots spread the fixed set-up cost of an order over many pieces, but they also tie up money in stock that must be carried. Harris's article "How many parts to make at once" (Factory, The Magazine of Management 10(2), 1913, reprinted in Operations Research 38(6), 1990) resolved the trade-off with a closed formula, the square-root or economic order quantity (EOQ) formula. It is the starting point of deterministic inventory theory and is still taught as the first model of every operations-management course.

Timeline. Harris published the formula in 1913, without proof ("the solution of this problem involves higher mathematics"). The same formula was popularised by R. H. Wilson in 1934 and was for decades attributed to him. D. Erlenkotter traced it back to Harris (Operations Research 38(6), 1990, 937–946), and the article was reprinted in the same issue. Later work built stochastic (Q, r) models on top of it; Zheng (1992) compared the EOQ heuristic with the optimal (Q, r) policy.

Setting

A part is used at a regular rate of $M$ units per month (the movement). Each unit costs $C$ dollars (the unit cost), and each order costs $S$ dollars to set up. Parts are made in lots of $X$ units, the lot size. Under regular movement a lot of $X$ is delivered when the stock reaches nothing and is then used up at rate $M$, so the stock at time $t \ge 0$ (months, from a delivery) is the sawtooth

$$\operatorname{stock}(t) = X\bigl(1 - \{Mt/X\}\bigr),$$

with $\{u\}$ the fractional part. Interest and depreciation on stock are charged at ten per cent a year, a rate the paper fixes.

Harris prices a unit in three parts:

1. the interest charge per piece: the average stock is $X/2$, its value including set-up is $\tfrac12(CX+S)$, ten per cent of this is the annual charge, and dividing by the $12M$ units used a year gives $\frac{1}{240M}(CX+S)$;
2. the set-up cost per piece $S/X$;
3. the unit cost $C$.

The cost per unit is therefore

$$Y(X) = \frac{1}{240M}(CX + S) + \frac{S}{X} + C,$$

and the economic lot size is $X^* = \sqrt{240MS/C}$. In Lean these are stockLevel, interestPerPiece, costPerUnit and econLotSize in the namespace HarrisEOQ.Lot.

Formalization targets

Goal: the square-root formula

For $M, C, S > 0$,

$$X^* > 0, \qquad Y(X^*) \le Y(X) \text{ for all } X > 0, \qquad Y(X) = Y(X^*),\ X > 0 \implies X = X^* .$$

This is Harris's claim that the value of $X$ giving the minimum value to $Y$ "reduces to the square root of (240MS divided by C)": $X^*$ is admissible, attains the minimum, and is the only lot size that does.

Milestones: the derivation of $Y$

1. The long-run average of the sawtooth stock is $X/2$: $\lim_{T\to\infty}\frac1T\int_0^T \operatorname{stock}(t)\,dt = X/2$.
2. The interest charge per piece, built in the paper's steps, equals $\frac{1}{240M}(CX+S)$, and $Y$ is the sum of the three per-piece costs.

These justify the objective $Y$, not its minimization; the paper gives no argument for the minimization.

Companion statements

• $X^* = K\sqrt M$ with $K = \sqrt{240S/C}$ (p. 948).
• The fourfold law: $X^*(M') = 2X^*(M) \iff M' = 4M$ (p. 950).
• A lot too small by $d$ costs more than one too large by $d$: $Y(X^*+d) < Y(X^*-d)$ for $0 < d < X^*$ (p. 949, general form of an observation made on an example).
• At the optimum, $S/X^* = CX^*/(240M)$ (p. 948).
• The paper's three worked lot sizes 2,190, 6,850 and 48.5, each to its last printed digit (pp. 948–949).

Significance

The result. The square-root formula gives the cost-minimising batch size in closed form from three observable numbers. Its consequences are the ones Harris draws: lot sizes grow only with the square root of demand (so consumption must quadruple to double a lot), the cost curve is flat near the optimum and asymmetric (erring small is worse than erring large), and at the optimum the set-up cost balances the variable carrying cost. Every later deterministic and stochastic lot-sizing model reduces to this one in its simplest case.

Formalizing it. The result is classical and proved in textbooks, but Harris's paper itself contains no proof. A formalization supplies the missing argument for the paper's exact objective, which differs from the textbook EOQ by charging interest on the set-up cost ($S/2$ in the stock value) and by the fixed ten per cent rate. It also makes the paper's modelling step precise: the claim that the average stock is $X/2$ becomes a statement about a time average of a sawtooth function. To our knowledge none of these statements has a machine-checked proof on the platform; the EOQ items of Zheng (1992) concern a different model, with backorders.

Difficulty

The minimization is elementary calculus; the substance of the mission is fidelity. The objective must be the display as printed, with $\frac{1}{240M}$ meaning $1/(240\cdot M)$, and the claim includes uniqueness, not only that $X^*$ is a minimizer. The average-stock milestone needs a genuine long-run average of a discontinuous periodic function over $[0, T]$ with $T$ not a whole number of cycles, which is where the integration and limit bookkeeping lies.

Formalization scope

All quantities are real numbers; lot sizes are not restricted to integers (the paper's own optimum is 48.5). The hypotheses $M, C, S > 0$ are not written on the page; they are implicit in the meaning of a usage rate, a price and a cost, and are added. Every quantifier over lot sizes is over $X > 0$. Time is measured in months, and the interest rate is fixed at ten per cent, so the constant $240 = 12 \cdot 2 \cdot 10$ appears as printed; the formula is not generalized to an arbitrary rate.

A trivializing formalization is ruled out: $Y$ is defined as the printed display, not rewritten around $X^*$; the average stock is an integral of the stock level, never defined as $X/2$; and the goal does not quantify over all real $X$, where Lean's convention $S/0 = 0$ would make $X = 0$ a spurious minimizer.

The manufacturing interval $T$ and the safe stock minimum play no role in the formula and are not modelled. The examples' cost figures (0.188 cents, $0.00028, and so on) are not formalized. The development needs only Mathlib's real numbers, square roots, fractional parts, interval integrals and limits; contributions of proofs of any item are welcome.

Selected references

• F. W. Harris, How many parts to make at once, Factory, The Magazine of Management 10(2):135–136, 152, 1913; reprinted in Operations Research 38(6):947–950, 1990. https://doi.org/10.1287/opre.38.6.947
• D. Erlenkotter, Ford Whitman Harris and the economic order quantity model, Operations Research 38(6):937–946, 1990. https://doi.org/10.1287/opre.38.6.937
• R. H. Wilson, A scientific routine for stock control, Harvard Business Review 13:116–128, 1934.
• Y.-S. Zheng, On properties of stochastic inventory systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87

Motivation

Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.

This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.

Setting

There are $r$ tasks $T_1,\ldots,T_r$ and $n$ identical processors. Each task $T_j$ has a positive processing time $\mu(T_j)$. A strict precedence order $\prec$ specifies tasks that must be completed first: $T_i\prec T_j$ means $T_j$ cannot start before $T_i$ ends. A priority list $L$ orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.

A schedule gives each task a processor and a start time $S_j\ge0$. Once started, the task occupies that processor continuously on $[S_j,S_j+\mu(T_j))$. Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means $S_i+\mu(T_i)\le S_j$ whenever $T_i\prec T_j$. The finishing time $\omega$ is the largest completion time $S_j+\mu(T_j)$. The paper's list rule starts the first currently ready task in $L$ whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in $L$.

The same task set is run a second time, with processing times $\mu'$, order $\prec'$, list $L'$, processor count $n'$, and finishing time $\omega'$. The data satisfy $\mu'(T_j)\le\mu(T_j)$ for every $j$ and $\prec'\subseteq\prec$. Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.

Formalization targets

General anomaly bound

For $r,n,n'\ge1$, positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:

$$\frac{\omega'}{\omega}\le 1+\frac{n-1}{n'}.$$

The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed $n,n'$. The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.

Significance

The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When $n'=n$, the factor is $2-1/n$; when the first run has one processor, it is $1$. The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.

The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.

Difficulty

Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.

Formalization scope

Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes $r>0$ so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's $\mu:T\to(0,\infty)$ convention.

The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or $\omega$. The covering-chain milestone represents Graham's set $B$ as times before $\omega'$ when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as $n'\omega'-\sum_j\mu'(T_j)$ using display (5). Natural-number subtraction is not used in the constants: $n-1$ and $n'-1$ are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

Motivation

Shop scheduling asks how to sequence jobs that each need processing on several machines. In an open shop, a job's operations may be executed in any order, as in testing stations, repair bays, or classroom and examination timetables, where the order in which a candidate visits the stations is irrelevant. The objective studied here is the makespan $C_{\max}$, the time at which the last operation finishes.

The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) introduced the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it names. For the open shop, its §5.2.1 presents a simplified exposition of the result of Gonzalez and Sahni (J. ACM 23, 1976): with two machines and no preemption, the obvious lower bound on the makespan is always achieved. The same page records that the three-machine case $O3\|C_{\max}$ is binary NP-hard, so two machines is exactly where the problem is easy.

Timeline. Gonzalez and Sahni (1976) gave the linear-time algorithm for $O2\|C_{\max}$, proved NP-hardness for $O3\|C_{\max}$, and gave a polynomial algorithm for the preemptive problem $O|pmtn|C_{\max}$. Graham et al. (1979, §5.2.1) gave the shorter construction formalized here, and observed (§5.2.2) that it implies preemption brings no advantage for $m = 2$. Lenstra (cited as forthcoming in the survey) showed $O2|r_j|C_{\max}$, $O2|tree|C_{\max}$ and $O\|C_{\max}$ unary NP-hard.

Setting

There are $n$ jobs $J_1, \dots, J_n$ and two machines $M_1$, $M_2$. Job $J_j$ has an operation on $M_1$ of length $a_j \ge 0$ and an operation on $M_2$ of length $b_j \ge 0$. There is no preemption, and every job is available at time $0$. A schedule assigns start times $s_1(j)$ and $s_2(j)$ to the two operations of $J_j$, which then occupy $[s_1(j), s_1(j)+a_j)$ on $M_1$ and $[s_2(j), s_2(j)+b_j)$ on $M_2$.

A schedule is feasible if

1. all start times are nonnegative;
2. each machine processes at most one job at a time: the intervals of distinct jobs on the same machine do not overlap;
3. each job is processed on at most one machine at a time: the two intervals of the same job do not overlap, in either order.

Write $T_1 = \sum_j a_j$ and $T_2 = \sum_j b_j$ for the two machine loads. The survey's construction uses the sets

$$A = \{J_j \mid a_j \ge b_j\}, \qquad B = \{J_j \mid a_j < b_j\},$$

two distinct jobs $J_r$, $J_l$ with $a_r \ge \max_{J_j \in A} b_j$ and $b_l \ge \max_{J_j \in B} a_j$, and $A' = A - \{J_r, J_l\}$, $B' = B - \{J_r, J_l\}$.

Formalization targets

Goal: the optimal makespan

$$C^*_{\max} = \max\Big\{T_1,\ T_2,\ \max_j\,(a_j + b_j)\Big\},$$

and the optimum is attained. Formally, for every $T \ge 0$: a feasible schedule completing every operation by $T$ exists if and only if $T_1 \le T$, $T_2 \le T$ and $a_j + b_j \le T$ for all $j$. The goal mentions neither $A$, $B$, $J_r$, $J_l$ nor the case analysis; those are the milestones.

Milestones (in the order of the argument)

1. Two distinct jobs $J_r$, $J_l$ with the required bounds exist when $n \ge 2$.
2. Fig. 5.1: the blocks $B' \cup \{J_l\}$ and $A' \cup \{J_r\}$, with $A'$ and $B'$ in arbitrary order, have feasible staircase schedules without idle time.
3. Fig. 5.2: if $T_1 - a_l \ge T_2 - b_r$, the blocks combine into a feasible schedule of all jobs ending by $T_1 + b_r$.
4. Case (1): if moreover $a_r \le T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, T_2\}$.
5. Case (2): if moreover $a_r > T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, a_r + b_r\}$.
6. The symmetric case $T_1 - a_l < T_2 - b_r$: some feasible schedule has length at most $\max\{T_1, T_2, a_l + b_l\}$.
7. The lower bound: every feasible schedule has $C_{\max} \ge \max\{T_1, T_2, \max_j(a_j + b_j)\}$.

Significance

The result. The theorem gives a closed form for the optimal makespan of a two-machine open shop, together with a linear-time construction of an optimal schedule. The survey uses it immediately: since the bound is also a lower bound for preemptive schedules, $O2|pmtn|C_{\max}$ is solved by the same schedules, so preemption gives no advantage on two machines (§5.2.2). It is the standard example of a shop problem whose trivial lower bound is tight, and the contrast with the binary NP-hard $O3\|C_{\max}$ marks the complexity boundary for nonpreemptive open shops.

Formalizing it. The result is classical and proved on paper; no machine-checked proof is known to exist on this platform. The mission produces a reusable model of nonpreemptive two-machine open-shop schedules with real processing times, a verified lower bound, and a verified constructive argument. Unlike many existence-of-schedule results, the survey's construction is explicit (orders and start times), so it can be formalized directly rather than through an abstract existence argument.

Difficulty

The lower bound is the easy half. The difficulty is the construction: a schedule must meet the bound simultaneously on both machines and for every job. The natural first idea, running every job on $M_1$ then $M_2$ in some order (a flow-shop schedule), fails: Johnson's rule then gives a makespan that can exceed $\max\{T_1, T_2, \max_j(a_j+b_j)\}$, because the open shop needs some job to visit $M_2$ first. The survey's construction moves exactly one job, $J_r$, to the front of $M_2$, and its correctness depends on the choice of $J_r$ and $J_l$ and on the case split on $T_1 - a_l$ versus $T_2 - b_r$. Figures 5.3 and 5.4 are drawn for $T_1 \ge T_2$; in the other subcases the start times shown in the figures need adjustment, and the formal statements of the cases assert lengths rather than the figures' exact start times.

Formalization scope

All declarations live in the namespace SchedSurvey.O2. Jobs are Fin n, 0-based ($J_j$ is index $j-1$). Processing times and start times are real numbers with $a_j, b_j \ge 0$; the survey's integer data are a special case, and every claim of §5.2.1 holds over the reals. A schedule is a pair of start-time functions s₁ s₂ : Fin n → ℝ. Interval non-overlap is s + p ≤ s' ∨ s' + p' ≤ s, so touching intervals are allowed and a zero-length operation occupies nothing. Feasibility (IsFeasible) contains both disjointness constraints of §2.1, the machine constraint and the job constraint, with the two operations of a job in either order. The job constraint is essential: without it the optimum would be $\max\{T_1, T_2\}$ and the goal false.

"Length at most $L$" is CompletesBy a b S L: every operation ends by $L$. Optimality is stated in threshold form, which avoids taking a supremum or infimum over a possibly empty set and is equivalent to "$C^*_{\max}$ equals the maximum and is attained". A maximum over $A$ or $B$ appears as a bound on every member, which is also correct for empty $A$ or $B$. The orders of $A'$ and $B'$ are duplicate-free lists whose members are exactly those sets; back-to-back start times are given by contigStart.

The milestone on the choice of $J_r$, $J_l$ assumes $n \ge 2$, which the page presupposes; the goal does not, and covers $n \le 1$ as well. The lower bound assumes $T \ge 0$, which matters only for $n = 0$.

A trivializing formalization is ruled out: feasibility includes both disjointness constraints and nonnegative start times, the threshold is quantified over all $T \ge 0$, and no constant is fixed.

Contributions welcome: proofs of the lower bound (a sum of disjoint intervals inside $[0, T]$), of the list-based block lemmas, of the case lemmas, and of the goal from them. The interval and back-to-back-schedule lemmas are reusable for other shop problems.

Selected references

• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
• S.M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110

Motivation

Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first $k$ tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.

The paper also notes two endpoints of this family. With $k=0$, the rule is ordinary list scheduling and has ratio at most $2-1/n$. With $k=n$, the $n$ longest tasks can start one per processor, giving ratio at most $3/2-1/(2n)$. Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of $n$ Graham, pp. 427–428.

Setting

There are $r>0$ independent tasks, indexed by $jin\{0,\ldots,r-1\}$, and $n>0$ identical processors, indexed by $p\in\{0,\ldots,n-1\}$. Task $j$ takes a strictly positive time $\mu_j$. A priority list $L$ contains every task exactly once. Its first $k$ tasks are $k$ of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.

An assignment $\sigma$ records the processor that executes each task. The load $\ell_p(\sigma)$ of processor $p$ is the sum of its assigned task lengths. The finishing time is the largest load, $\omega(k)=\max_p\ell_p(\sigma)$. For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment $\tau$, let $\omega_k(\tau)$ be the largest load contributed by only the first $k$ list tasks. The algorithm requires its own first $k$ assignments to minimize $\omega_k(\tau)$ over all assignments $\tau$; the remaining tasks may occur in any list order.

Write $\omega_0$ for the smallest finishing time achievable for all $r$ tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of $\omega_0$.

Formalization targets

Theorem 3

For $0\le k\le r$, when the first $k$ longest tasks have an optimal prefix schedule, Graham's bound is

$$\frac{\omega(k)}{\omega_0} \le 1+\frac{1-1/n}{1+\lfloor k/n\rfloor}.$$

Here $\lfloor k/n\rfloor$ is the greatest integer at most $k/n$. The theorem also says the bound is best possible when $k$ is divisible by $n$ Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.

Source milestones

The milestones state the finite-volume lower bound on $\omega_0$, the case in which completing all tasks takes no longer than completing the first $k$, and the paper's numbered inequalities (14), (15), and (16). They use $\alpha^*$ for the greatest task length after the first $k$ positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.

Significance

The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is $1+\lfloor k/n\rfloor$, so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of $n$ shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.

The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.

Difficulty

An optimal schedule for the first $k$ long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor $\lfloor k/n\rfloor$. Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.

Formalization scope

Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based $T_j$ and $P_i$. Task lengths are positive real numbers, and both $r$ and $n$ are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition $k\le r$ is explicit because choosing $k$ tasks from $r$ requires it; the paper treats $r>k$ inside the proof and the case $k=r$ is covered by the theorem. There is no precedence relation in this mission.

The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first $k$ positions must contain $k$ longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.

All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity $\alpha^*$ is the largest duration outside the prefix when $k<r$, and is defined as zero when none remains; statements using it require $k<r$. Division is by $n>0$ and by $\omega_0>0$. Lean's natural-number quotient represents $\lfloor k/n\rfloor$; real subtraction is used for coefficients such as $n-1$. Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

Why deteriorating jobs need a scheduling rule

On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.

The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.

Jobs, schedules, and cost

There are $N$ jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule $\pi$ is a permutation of the jobs: $\pi(k)$ is the job processed in position $k$. The paper labels positions and jobs from $1$ to $N$; the Lean development labels them from $0$ to $N-1$. The identity schedule $\pi_0$ processes jobs in label order.

For job $i$, $X_i$ is its random initial processing requirement, $\alpha_i$ its deterministic growth rate, and $c_i$ its waiting cost rate. If the job starts at time $t$, its actual processing time is $Y_i(t)=X_i+\alpha_i t$. Deterioration stops once processing starts. Write $S_k(\pi)$ for the time at which the first $k$ scheduled jobs have all finished. The model sets $S_0(\pi)=0$ and

$$S_{k+1}(\pi)=S_k(\pi)+X_{\pi(k+1)}+\alpha_{\pi(k+1)}S_k(\pi)$$

in the paper's one-based position notation. Thus the completion time of the job in position $k$ is $S_k(\pi)$. Its cost is its own rate $c_{\pi(k)}$ times that completion time, giving

$$C(\pi)=\sum_{k=1}^{N}c_{\pi(k)}S_k(\pi).$$

All of these are random quantities until an expectation is taken. Equation (2) of the paper writes $S_k$ as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into $C(\pi_0)$. Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in $C$ from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.

Formalization targets

The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,

$$\frac{E(X_1)}{\alpha_1}<\cdots<\frac{E(X_N)}{\alpha_N}, \qquad \frac{\alpha_1}{c_1(1+\alpha_1)} <\cdots< \frac{\alpha_N}{c_N(1+\alpha_N)},$$

then, for every permutation $\sigma$,

$$E[C(\pi_0)]\le E[C(\sigma)].$$

The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.

The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.

What the result establishes

The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only $E(X_i)/\alpha_i$, enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.

The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.

Where the argument is difficult

Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.

The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.

Formalization scope

Jobs are $\mathrm{Fin}\,N$, and a policy is an equivalence permutation with $\pi(k)$ equal to the job in position $k$. Completion time is defined by the processing rule $Y_i(t)=X_i+\alpha_i t$, not by the closed form (2). At positions beyond the $N$ jobs it stays constant, and theorems about the closed form restrict $k$ to $0\le k\le N$. The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.

The proposition uses a probability space and the Bochner integral of the real-valued cost. Every $X_i$ is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.

The two strict orderings are over the labels of jobs in $\pi_0$, not positions of an arbitrary schedule. The conclusion compares $\pi_0$ with every permutation, not only with schedules obtained by one adjacent swap. The $N=0$ and $N=1$ cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.

Selected references

• Browne, Sid, and Uri Yechiali, Scheduling Deteriorating Jobs on a Single Processor, Operations Research 38(3), 495–498 (1990). DOI: 10.1287/opre.38.3.495.

Motivation

The cutting stock problem asks how to cut standard stock rolls of length $L$ into pieces of demanded lengths $l_1,\dots,l_m$ so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.

Setting

There are $m$ demanded lengths $l_1,\dots,l_m>0$ with linear programming prices $b_1,\dots,b_m\ge0$, and $k$ standard stock lengths $L_1,\dots,L_k$ with costs $c_1,\dots,c_k$. A column for $L_j$ is a vector $(\alpha)_m=(a_1,\dots,a_m)$ of nonnegative integers with $\sum_i l_ia_i\le L_j$. The knapsack problem (1) for $L_j$ is

$$\bar M_j=\max\Big\{\sum_{i=1}^m b_ia_i : a_i\in\mathbb Z_{\ge0},\ \sum_{i=1}^m l_ia_i\le L_j\Big\},$$

and the quantity to compute is $M_j=\max(c_j,\bar M_j)$: a column improves the linear program exactly when $\bar M_j>c_j$.

For a prefix $(\alpha)_s=(a_1,\dots,a_s)$ write $\lambda\cdot(\alpha)_s=\sum_{i\le s}l_ia_i$ and $\beta\cdot(\alpha)_s=\sum_{i\le s}b_ia_i$. Step (1) sorts the data, $b_1/l_1\ge\dots\ge b_m/l_m$ and $L_1>\dots>L_k$, and appends a slack item $a_{m+1}$ with $b_{m+1}=0$, $l_{m+1}=1$. The method then generates vectors in decreasing lexicographic order:

• Steps (2) and (7) fill the coefficients after a prefix greedily, $a_i=[(L-\text{used})/l_i]$, for $L=L_1$ at the start and $L=L_t$ later.
• Step (3) records $\beta\cdot(\alpha)_m$ as the new $M_j$ for each $j\ge t$ with $L_j\ge\lambda\cdot(\alpha)_m$ and $\beta\cdot(\alpha)_m>M_j$.
• Step (4) finds the last nonzero coefficient $a_s$.
• Step (5) lowers $a_s$ by one and looks for the smallest $j$ with $L_j\ge\lambda\cdot(\alpha)_s$ and $(L_j-\lambda\cdot(\alpha)_s)b_{s+1}>(M_j-\beta\cdot(\alpha)_s)l_{s+1}$. This is the bound obtained by relaxing the integrality of $a_{s+1}$.
• Step (6) backs up to the previous nonzero coefficient when no such $j$ exists, and stops when there is none.

In Lean the method is a transition system Step on states (a, s, t, M, phase). Reachable means reachable from the start state of Step (2).

Formalization targets

Goal: the method terminates and computes $M_1$

Under Step (1)'s ordering, with $l_i>0$ and $b_i\ge0$:

$$\text{every run is finite},\quad \text{a non-final state has a successor},\quad M_1^{\text{final}}=\max\big(c_1,\bar M_1\big),$$

and at the end every $M_j$ is $c_j$ or the price of a column for $L_j$, with $c_j\le M_j$. With one stock length ($k=1$) this is the paper's correctness claim in full: the method solves the knapsack problem (1).

Milestones

1. Steps (2)/(7): the greedy completion is the lexicographically largest extension of a prefix that fits the capacity.
2. Step (4): the lexicographic predecessor of a fitting vector extends $(\alpha^1)_s$.
3. The relaxation bound $\beta\cdot(\alpha')_m\le\beta\cdot(\alpha)_s+b_{s+1}(L-\lambda\cdot(\alpha)_s)/l_{s+1}$ for every fitting extension.
4. After the inequality of Step (5)'s test fails, no vector between $(\alpha)_s$ and the successor of Step (6) improves $M$.
5. The vectors tested in Step (3) strictly decrease lexicographically.
6. The invariant on entry to Step (3).
7. Identical prices: among lengths with equal prices only the shortest is needed (p. 869).

Significance

The goal certifies the pricing oracle of the Gilmore–Gomory column-generation method: the knapsack solver it calls returns the true optimum. The pricing step is exact only if that holds, and so is the conclusion "no improving column exists, the LP is solved". Milestones 1–4 are reusable on their own. They are the textbook ingredients of lexicographic and depth-first branch-and-bound for the integer knapsack: the greedy completion, the density-ordered LP bound, and the pruning rule.

The paper's argument is a short paragraph, "clear from the order in which the $m$-vectors are generated". Writing it out shows that the claim is false for several stock lengths as the steps are printed. With $m=1$, $l_1=b_1=1$, $L=(5,2)$ and $c=(0,0)$, the method tests $(5)$. The test of Step (5) at $(4)$ then fails for $j=2$ only because $4>L_2$, Step (6) stops, and the run ends with $M_2=0$ while the column $(2)$ has price 2. This mission therefore states what the printed algorithm does achieve. The result is the full claim for $k=1$ and for the longest stock length in general. A sorry-free Lean proof of the counterexample run accompanies the mission. No part of the method or its correctness has been formalized before, as far as a search of the platform shows.

Difficulty

The method skips large parts of the lexicographic order in three ways:

• Step (7) jumps to the greedy completion for $L_t$ rather than $L_1$.
• Step (6) jumps past every smaller value of $a_s$ once one test fails.
• Step (3) updates only $j\ge t$.

Each skip has to be justified by a bound that holds for every vector skipped, and the justifications interact. A skipped vector may fit a longer stock length but not $L_t$, and the bound for $L_1$ must cover exactly those vectors. The invariant that survives all three moves is not the naive "every vector above the current one has been examined": the vectors are not examined, only bounded. Termination needs the lexicographic decrease together with finiteness of the fitting vectors, and progress needs the reachability invariants $1\le s\le m$ and $a_s\ne0$ that make Step (5) meaningful.

Formalization scope

• Items are Fin m from 0. The paper's level $s$ is a natural number, and the prefix $(\alpha)_s$ is the coordinates with index < s. Stock lengths are Fin k, and $L_1$ is index 0. The slack item enters only through $b_{s+1}$ and $l_{s+1}$ at $s=m$. The lexicographic order is Mathlib's Pi.Lex, and $[x]$ is Nat.floor.

• $M_j=\max(c_j,\bar M_j)$ is the predicate IsKnapsackMax, never a real supremum, which would be 0 on an empty set. The algorithm's output is never defined as the maximum. The goal includes termination and progress, so its correctness clause is not vacuous. Every invariant is stated for reachable states only.

• The goal adds two disclosed hypotheses:

  • $l_i>0$: demanded lengths.
  • $b_i\ge0$: with a negative price the method is wrong, and the paper applies it to cutting-stock prices, which are nonnegative.

  Step (1) is a hypothesis on the data, not a step.

• The goal also makes these corrections:

  • The claim is narrowed. For every $j$ it states $c_j\le M_j$ and attainment, and the upper bound for $L_1$ only (see Significance).
  • The lexicographic order is repaired. The page's definition misses vectors that differ in their first coefficient.
  • Step (7) reads λ·(α)_m. The page's "satisfies $L_t\ge\lambda\cdot(\alpha)_s$" is read as $\lambda\cdot(\alpha)_m$.
  • Step (4) gets a stopping case. On the zero vector, where the page has no case, the method stops.
  • Milestone 4 is stated for the failed inequality, not for a failed test, because the failed test is what makes the page's successor claim false.

• Not formalized:

  • Step (3′), the variant computing $\max_j(M_j-c_j)$.
  • The record of patterns.
  • The dynamic-programming recursion and the timing estimates.

Contributions welcome: proofs of the milestones, and a corrected multi-length variant of the method with a proof that it computes every $M_j$.

Selected references

• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6) (1963), 863–888. https://doi.org/10.1287/opre.11.6.863
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6) (1961), 849–859. https://doi.org/10.1287/opre.9.6.849
• G. B. Dantzig, Discrete-variable extremum problems, Operations Research 5(2) (1957), 266–288. https://doi.org/10.1287/opre.5.2.266

Why consensus and sharing

Many large optimization problems arising in statistics, machine learning, signal processing and resource allocation have an objective that is a sum of terms, each depending on data held by a different processor, or a coupling term that depends on the sum of the agents' decisions. Chapter 7 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) introduces two templates that turn such problems into distributed algorithms: consensus and sharing. Nearly every distributed application in the rest of the monograph (distributed lasso, distributed logistic regression, splitting across examples and across features in Chapter 8) is an instance of one of the two. Consensus problems in the context of ADMM go back to Bertsekas and Tsitsiklis (Parallel and Distributed Computation, 1989).

The value of the templates lies in a handful of exact algebraic facts about the ADMM subproblems: the global update is an average, the dual variables average to zero, and the sharing update, which looks like a problem in $Nn$ variables, is really a problem in $n$ variables. These facts are what this mission formalizes.

Setting

There are $N\ge1$ agents. Vectors live in $\mathbb R^n$ with the Euclidean inner product, and an overline denotes an average over agents, $\bar v=\frac1N\sum_{i=1}^N v_i$. Each local cost $f_i$ and the shared cost $g$ are functions into $\mathbb R\cup\{+\infty\}$. The penalty parameter is $\rho>0$.

Global variable consensus (§7.1) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)\quad\text{subject to } x_i-z=0,\ i=1,\dots,N,$$

with local variables $x_i\in\mathbb R^n$ and a global variable $z$. ADMM alternates a parallel $x_i$-update, an averaging $z$-update and a dual update of the multipliers $y_i$. With a regularizer $g(z)$ added (7.2), the $z$-update (7.4) becomes a minimization involving $g$.

General form consensus (§7.2) lets local variable $x_i\in\mathbb R^{n_i}$ copy only some entries of $z$: entry $j$ of $x_i$ corresponds to entry $z_{\mathcal G(i,j)}$, and $\tilde z_i\in\mathbb R^{n_i}$ is defined by $(\tilde z_i)_j=z_{\mathcal G(i,j)}$. The number of local entries copying $z_g$ is $k_g$.

Sharing (§7.3) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)+g\Big(\sum_{i=1}^N x_i\Big),\tag{7.11}$$

written for ADMM with copies $z_i$ of the $x_i$ (7.12). In scaled form, with $a_i=u_i^k+x_i^{k+1}$, its $z$-update is

$$(z_1^{k+1},\dots,z_N^{k+1})\in\operatorname*{argmin}_{z_1,\dots,z_N}\ g\Big(\sum_{i=1}^N z_i\Big)+(\rho/2)\sum_{i=1}^N\|z_i-a_i\|_2^2,$$

followed by $u_i^{k+1}=u_i^k+x_i^{k+1}-z_i^{k+1}$.

Formalization targets

Goal: the sharing $z$-update reduction (§7.3, p. 57)

For every $a_1,\dots,a_N$: $(z_1,\dots,z_N)$ solves the $Nn$-variable $z$-update iff $\bar z$ solves

$$\operatorname*{minimize}_{\bar z\in\mathbb R^n}\ g(N\bar z)+(\rho/2)\sum_{i=1}^N\|\bar z-\bar a\|_2^2$$

and

$$z_i=a_i+\bar z-\bar a\quad (7.13);$$

and along every run of sharing ADMM,

$$u_i^{k+1}=\bar u^k+\bar x^{k+1}-\bar z^{k+1}\quad(7.14),$$

so all scaled dual variables agree after one step.

Milestones

• §7.1: the consensus $z$-update is $z^{k+1}=\bar x^{k+1}+(1/\rho)\bar y^k$; then $\bar y^{k+1}=0$, $z^k=\bar x^k$ and the simplified iteration.
• (7.4), §7.1.1: with a regularizer, the $z$-update is averaging followed by a proximal step with weight $N\rho$; the soft-threshold ($g=\lambda\|\cdot\|_1$) and positive-part ($g$ the indicator of $\mathbb R^n_+$) examples.
• §7.2: the general form $z$-update is local averaging, and the dual entries attached to each global index sum to zero after the first iteration.
• (7.13): with $\bar z$ fixed, $z_i=a_i+\bar z-\bar a$ is the unique minimizer.

Significance

The reduction is what makes sharing ADMM scale: the central step needs only the averages $\bar x^{k+1}$, $\bar u^k$ and one $n$-dimensional proximal problem, regardless of the number of agents, and the dual state collapses to a single vector. The same reduction underlies exchange ADMM (§7.3.2) and the splitting-across-features algorithms of §8.3. The consensus facts explain why the fusion center only averages and why the dual variables can be dropped from its update.

All results of the chapter are proved, informally, in the monograph; they are elementary. To our knowledge none has a machine-checked proof. The mission produces checked statements of the update formulas that later chapters of the series and distributed-optimization developments can cite instead of re-deriving.

Difficulty

The statements are exact identities between minimizer sets of nonsmooth problems in which $g$ may be any extended-real-valued function: there is no first-order condition to use, so each step must be argued by comparing objective values, and the iff requires producing, for an arbitrary competitor, a competitor of the reduced problem with no larger value. The index bookkeeping is the other half: averages of sums of sequences indexed by agents and by iterations, the off-by-one in "after the first iteration", and in §7.2 sums over the fibres $\{(i,j):\mathcal G(i,j)=g\}$ of an index map between local vectors of different dimensions.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin n); agents are indexed by Fin N, so the book's $i=1,\dots,N$ is Lean's $i-1$; components are 0-based as well.
• An extended-real-valued function is encoded by its effective domain (a set) and its finite values; every minimization is over the domain. Convexity is not assumed: none of the stated identities needs it, so the statements are slightly more general than the chapter's standing assumption that each $f_i$ is convex.
• Iterates are hypotheses: a run is any sequence satisfying the update rules (argmin properties, not chosen minimizers). The consensus run uses the averaging formula exactly as printed on p. 49; the general form and sharing runs use the argmin form printed on pp. 55–56.
• Explicit hypotheses that the book leaves implicit: $N\ge1$, $\rho>0$, $\lambda>0$ (named lam), $k_g\ge1$ for every global index $g$ in §7.2, and the index ranges $k\ge1$ for $\bar y^{k}=0$ and $k\ge2$ for $z^k=\bar x^k$ (the starting $y^0$ is arbitrary).
• Corrected misprints: p. 52 prints $\bar x^{k+1}-(1/\rho)\bar y^k$ in the soft-threshold and positive-part examples, while the proximal form gives $\bar x^{k+1}+(1/\rho)\bar y^k$; p. 55 prints $\sum_{i=1}^m$ for $\sum_{i=1}^N$; p. 57 writes $u\in\mathbf R^m$ for a vector of $\mathbb R^n$.
• The goal is about minimizers of the $Nn$-variable $z$-subproblem, not the algebraic identity (7.13) alone, and (7.14) is derived for every run rather than built into a single-dual-variable definition; either shortcut would make the goal trivial.
• Not included: the consensus residual norms (p. 51), the duality discussion of §7.3.1 and exchange ADMM (§7.3.2). Contributions formalizing them on top of these definitions are welcome.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 1–122, 2011. https://doi.org/10.1561/2200000016
• D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://web.mit.edu/dimitrib/www/pdc.html

Motivation

In two-stage optimization under uncertainty, a first-stage decision $x$ is taken before the data are known, and a second-stage decision $y$ is taken after a scenario $\omega$ is revealed. The fully adaptive formulation lets $y$ depend on $\omega$ and minimizes the worst-case cost. It is the natural model of recourse, but it optimizes over policies, one decision per scenario, and is computationally hard in general. The static robust formulation fixes one $y$ in advance that must be feasible in every scenario. It is a single deterministic mixed integer program and is the standard tractable surrogate (Ben-Tal, Goryashko, Guslitzer, Nemirovski 2004; Bertsimas & Sim 2004).

The question is how much is lost by the surrogate. Bertsimas and Goyal (2010) bound the gap by $2$ against the stochastic problem and by $4$ against the adaptive problem when the uncertainty set is symmetric. Their §5.3 identifies a case with no gap at all: when the uncertainty set is a hypercube (a box), the static robust optimum equals the adaptive optimum, and this holds even when the constraint matrices themselves are uncertain. Box uncertainty is the simplest and most common uncertainty model in practice (interval data on every coefficient), so the result says that for it, adaptivity buys nothing.

This mission formalizes that theorem, Theorem 5.4, together with Theorem 2.4, which shows that under right-hand-side uncertainty the robust problem is a single deterministic problem with the coordinatewise worst right-hand side.

Setting

Fix dimensions $m,n_1,n_2$ and sets $I_1,I_2$ of integer coordinates. The decision domains are

$$D_{I}=\{x\in\mathbb R^n : x\ge0,\ x_i\in\mathbb Z\ \text{for } i\in I\},$$

which is $\mathbb R_+^{n-p}\times\mathbb Z_+^{p}$ up to relabelling coordinates, $p=|I|$.

A scenario set $\Omega$ is given. In scenario $\omega$ the data are a constraint matrix $A(\omega)\in\mathbb R^{m\times n_1}$, a recourse matrix $B(\omega)\in\mathbb R^{m\times n_2}$, a right-hand side $b(\omega)\in\mathbb R^m$ and a second-stage cost $d(\omega)\in\mathbb R^{n_2}_+$. The first-stage cost $c\in\mathbb R^{n_1}_+$ is fixed.

• The adaptive problem $\Pi_{\mathrm{Adapt}}(A,B,b,d)$ (5.6) chooses $x\in D_{I_1}$ and $y(\omega)\in D_{I_2}$ for every $\omega$ with $A(\omega)x+B(\omega)y(\omega)\ge b(\omega)$ for all $\omega$, and has value

$$z_{\mathrm{Adapt}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega).$$

• The robust problem $\Pi_{\mathrm{Rob}}(A,B,b,d)$ (5.7) chooses one $x\in D_{I_1}$, $y\in D_{I_2}$ with $A(\omega)x+B(\omega)y\ge b(\omega)$ for all $\omega$, and has value

$$z_{\mathrm{Rob}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty.$$

The uncertainty set is $\mathcal U=\{(A(\omega),B(\omega),b(\omega),d(\omega)) : \omega\in\Omega\}$, a subset of $\mathbb R^N$ with $N=mn_1+mn_2+m+n_2$. Following Definition 1.1, $\mathcal U$ is a hypercube if $\mathcal U=[l_1,u_1]\times\cdots\times[l_N,u_N]$ for some $l_i\le u_i$.

For Theorem 2.4, $A$, $B$ and $d$ are fixed and only $b(\omega)\in\mathbb R^m_+$ varies; $\Pi_{\mathrm{Rob}}(b)$ (1.2) is the robust problem above, and $\Pi$ is the deterministic problem with right-hand side $b^h_j=\max_\omega b_j(\omega)$.

Formalization targets

Goal: Theorem 5.4 (p. 31)

If $\mathcal U$ is a hypercube, then

$$z_{\mathrm{Rob}}(A,B,b,d)=z_{\mathrm{Adapt}}(A,B,b,d).$$

The integer coordinates $I_1,I_2$ are arbitrary, and nothing is assumed about the signs of $A$, $B$, $b$.

Milestones

1. Theorem 2.4 (p. 17). Under right-hand-side uncertainty, $(x,y)$ is feasible for $\Pi_{\mathrm{Rob}}(b)$ if and only if $Ax+By\ge b^h$; hence $z_{\mathrm{Rob}}(b)=z(\Pi)$.
2. p. 31 display. $z_{\mathrm{Adapt}}(A,B,b,d)\le z_{\mathrm{Rob}}(A,B,b,d)$ for every uncertainty set.
3. Eqs. (5.8)–(5.10). If $\mathcal U$ is a hypercube, some scenario $\bar\omega$ has $A(\bar\omega)$, $B(\bar\omega)$ entrywise minimal and $b(\bar\omega)$, $d(\bar\omega)$ entrywise maximal over $\Omega$.
4. Eqs. (5.11)–(5.13). For such $\bar\omega$, if $(x,y(\cdot))$ is adaptive feasible, then $(x,y(\bar\omega))$ is robust feasible.
5. Eq. (5.14). For such $\bar\omega$, the robust worst-case cost of $(x,y(\bar\omega))$ is at most the adaptive worst-case cost of $(x,y(\cdot))$.

Significance

The result. Theorem 5.4 says that for interval uncertainty on every coefficient, the static robust program, whose size does not grow with the number of scenarios, solves the adaptive problem exactly. Combined with Theorem 2.4 for right-hand-side uncertainty, the adaptive problem collapses to one deterministic mixed integer program with worst-case data. It marks the boundary case of the paper's adaptability-gap bounds: the gap is at most $4$ for symmetric sets, and exactly $1$ for boxes.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean model of two-stage robust and adaptive mixed integer programs with uncertain constraint matrices, with values as extended-real infima, which other formalizations of adjustable robust optimization can build on.

Difficulty

The mathematics is elementary; the care is in the statement. The step that fails for a general uncertainty set is the existence of a single worst scenario $\bar\omega$ that is simultaneously entrywise smallest in $A$, $B$ and entrywise largest in $b$, $d$. For a set that is only contained in a box, the box's worst corner need not be realized. With two scenarios $b=(1,0)$ and $b=(0,1)$, $B=I$, $d=(1,1)$, the adaptive value is $1$ and the robust value is $2$. A formalization therefore has to state the hypercube hypothesis as an equality of sets. A second point is the arithmetic of extended reals: the paper argues from optimal solutions, which need not exist, so the inequalities must be transported through infima over feasible sets that may be empty and through suprema that may be infinite.

Formalization scope

• Decisions are vectors Fin n → ℝ; matrices are Matrix (Fin m) (Fin n) ℝ; constraints use Mathlib's componentwise order and mulVec.
• Mixed-integer domains are "nonnegative, integer on a designated coordinate set $I$", the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$ up to relabelling.
• Optimal values are EReal infima over the feasible set, $+\infty$ when infeasible; worst-case costs are EReal suprema over $\Omega$. No optimal solution is assumed.
• A scenario datum is a structure with the four blocks $(A,B,b,d)$; the box and the hypercube predicate are written entrywise on these blocks, which is Definition 1.1 in $\mathbb R^N$.
• The hypercube hypothesis is IsHypercube (uncertaintySet A B b d), i.e. the realized data are exactly a box. Assuming only that the data lie inside a box would make the statement false (example above); assuming fixed $A$, $B$ would state Corollary 5.1 instead of Theorem 5.4.
• Typos corrected in the Lean: (5.6)–(5.7) print $\mathbb Z^{n_2}_+$ for the second-stage integer block, read as $\mathbb Z^{p_2}_+$; §5.3's opening sentence names $\Pi_{\mathrm{Adapt}}(b,d)$ twice where the first is $\Pi_{\mathrm{Rob}}(b,d)$.
• In Theorem 2.4 the paper's $\max_\omega b_j(\omega)$ is a real supremum under the hypothesis that the right-hand sides are bounded above, and the second stage is continuous ($p_2=0$), as in the problem $\Pi$ on the page.

Contributions welcome: proofs of the milestones and of the goal, and lemmas on monotonicity of mulVec for nonnegative vectors and on EReal infima over feasible sets, which are reusable across the other missions of this series.

Selected references

• D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace).
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task $T_i$ has a length $l_i \ge 0$ and a preferred starting time $a_i \ge 0$, and the discrepancy of a task started at time $s_i$ is $|s_i - a_i|$. The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an $O(N \log N)$ algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy $\max_i |s_i - a_i|$: a linear-time test for a given bound $\gamma$ after an $O(N \log N)$ sort, combined with a search over $\gamma$.

This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).

Setting

Fix a bound $\gamma \ge 0$. A schedule has maximum discrepancy at most $\gamma$ exactly when every task starts no earlier than its release time $r_i = \max\{0, a_i - \gamma\}$ and finishes no later than its deadline $d_i = a_i + l_i + \gamma$ (p. 342). These release times and deadlines are in special form: with $\alpha = 2\gamma$, for every task

$$d_i - r_i = l_i + \alpha \quad\text{or}\quad \big(r_i = 0 \text{ and } d_i < l_i + \alpha\big).$$

From here on the data are arbitrary reals $l_i \ge 0$, $r_i \ge 0$, $d_i$ in special form for some $\alpha \ge 0$.

A schedule is an execution order $\sigma$ ($\sigma(p)$ is the task in position $p$) with starting times $s_i$, such that a task finishes no later than any later-positioned task starts: $s_{\sigma(p)} + l_{\sigma(p)} \le s_{\sigma(q)}$ for $p < q$. It is feasible if $r_i \le s_i$ and $s_i + l_i \le d_i$ for every $i$. Its makespan is $\max_i (s_i + l_i)$, and it is optimum if it is feasible and no feasible schedule has a smaller makespan.

Let $T_N$ be a task of largest deadline. A schedule has the release time property if every task executed after $T_N$ has release time strictly later than the starting time of $T_N$. When the tasks are indexed with $d_1 \le \dots \le d_N$, a schedule is in standard form with split index $j$, $0 \le j \le N-1$, if it begins with an optimum schedule of $T_1, \dots, T_j$, followed by $T_N$ started at the maximum of $r_N$ and the completion time of that first part, followed by $T_{j+1}, \dots, T_{N-1}$ in this order without idle time.

Formalization targets

Goal: Corollary 2 (p. 344)

$$\exists\ \text{a feasible schedule} \;\Longrightarrow\; \exists\ \text{an optimum schedule that is in standard form and has the release time property.}$$

Milestones

1. Theorem 4 (pp. 342–343): if a feasible schedule exists, some optimum schedule has the release time property with respect to any task of largest deadline.
2. The deadline split (proof of Corollary 1, p. 344): in every feasible schedule with the release time property, a task $T_i \neq T_N$ precedes $T_N$ if and only if $d_i \le s_N + \alpha$.
3. Corollary 1 (p. 344): some optimum schedule executes before $T_N$ exactly the tasks of deadline at most $\beta$, for some $\beta \ge 0$.
4. Release before finish (p. 344): every task executed after $T_N$ has $r_i \le s_N + l_N$.
5. Normalization after $T_N$ (p. 344): an optimum schedule with the release time property can be changed, without moving $T_N$ later and without touching the tasks before it, so that there is no idle time from the start of $T_N$ on and the later tasks run in deadline order.

Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with $\alpha = 2\gamma$.

Significance

Corollary 2 reduces the search for an optimum schedule of $T_1, \dots, T_n$ to $n$ candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in $O(N)$ time after an $O(N \log N)$ sort; combined with a search over $\gamma$ it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.

The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.

Difficulty

The obvious argument fails in Theorem 4. Exchanging a straggler (a task after $T_N$ released no later than $T_N$ starts) with $T_N$ shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after $T_N$ starts has $r_i > 0$, hence $d_i - r_i = l_i + \alpha$ exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after $T_N$, then fewest tasks between $T_N$ and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after $T_N$ and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.

Formalization scope

Tasks are indexed by Fin N (0-based: the paper's $T_1, \dots, T_N$ are $0, \dots, N-1$; the paper's $T_N$ in Corollary 2 is the index $N-1$). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.

The standing hypotheses on every structural item are $\alpha \ge 0$, $r_i \ge 0$, $l_i \ge 0$ (from $\gamma \ge 0$, the $\max\{0, \cdot\}$ in $r_i$, and nonnegative lengths); since $s_i \ge r_i$, start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task $T_0$ ($r_0 = d_0 = l_0 = 0$) is not a task; an empty first part completes at time $0$. Corollary 1's "the set of all tasks with deadline $\beta$ or less" is read as excluding $T_N$, the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.

A trivializing formalization is excluded: the standard form pins $T_N$'s start to $\max(r_N, C)$ and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.

Running times ($O(N \log N)$, $O(N)$) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (reference [4] of the paper, cited on p. 342 for the NP-completeness of one-processor scheduling with release times and deadlines). ISBN 0-7167-1045-5