All missions

Motivation

The assignment problem asks how to assign $n$ men to $n$ jobs, one man per job, so that the total cost (or, equivalently, the total rating) is optimal. It is the simplest combinatorial optimization problem with a nontrivial polynomial-time algorithm, and it appears as a subroutine across operations research: in transportation and network-flow methods, in tracking and data association, in scheduling, and as the relaxation behind branch-and-bound methods for the travelling salesman problem.

The algorithm studied here is the one now usually called the Hungarian method or Kuhn–Munkres algorithm.

• 1931: Kőnig and Egerváry prove the theorem on lines and independent zeros of a matrix that the method rests on.
• 1955: H. W. Kuhn gives the Hungarian method, with finiteness argued for integer matrices through a decreasing integer sum (Kuhn 1955). M. Flood restates it as Steps A–D.
• 1957: J. Munkres gives a fully specified version, in which Step B of Flood's outline (find a minimal set of lines containing all zeros and a maximal set of independent zeros) is carried out by an explicit marking procedure with starred and primed zeros. He proves it correct, shows that the integrality assumption is unnecessary, and bounds the work by a polynomial in $n$ (Munkres 1957).

The mission formalizes Munkres' correctness proof for §1 of that paper.

Setting

Let $A=(x_{ij})$ be a real $n\times n$ matrix, $x_{ij}$ being the cost of assigning man $i$ (row $i$) to job $j$ (column $j$). A set of entries is independent if no two of them lie in the same line (row or column). An assignment is a permutation $\sigma$, with $\sigma(r)$ the man doing job $r$. Its cost is $\sum_r x_{\sigma(r)\,r}$, and $\sigma$ is an optimal assignment if this cost is at most that of every permutation $\tau$. Choosing $n$ independent entries of minimum sum is the same as choosing an optimal assignment.

The algorithm. A state of the algorithm holds the current matrix, a set of starred zeros $0^*$, a set of primed zeros $0'$, a set of covered rows and a set of covered columns. An entry is non-covered, once-covered or twice-covered according as it lies in zero, one or two covered lines.

• Preliminaries. Subtract from each row its smallest element, then from each column its smallest entry. Consider the zeros in turn and star each one that has no starred zero in its row or column. Cover the columns containing a $0^*$.
• Step 1. Prime a non-covered zero. If its row contains no $0^*$, go to Step 2. Otherwise cover its row and uncover the column of that $0^*$. When no non-covered zero remains, go to Step 3.
• Step 2. Build the alternating sequence $Z_0,Z_1,\dots,Z_{2k}$. It starts at the $0'$ just found. Each $Z_{2i+1}$ is the $0^*$ in the column of $Z_{2i}$, each $Z_{2i+2}$ is the $0'$ in the row of $Z_{2i+1}$, and the sequence stops at a $0'$ with no $0^*$ in its column. Unstar its starred zeros and star its primed zeros. Erase all primes, uncover all rows and cover the columns containing a $0^*$. Stop if all columns are covered; otherwise return to Step 1.
• Step 3. Let $h$ be the smallest non-covered element. Add $h$ to each covered row, subtract $h$ from each uncovered column, and return to Step 1 with all marks kept.

The quantity $n_k$, the maximal number of independent zeros of the matrix $A_k$, measures progress.

Formalization targets

Goal: correctness of the algorithm

For every real $n\times n$ matrix $A$:

$$\exists\,\text{start};\quad \text{every run is finite};\quad \text{no reachable non-final state is stuck};\quad \text{at a final state } \{0^*\}=\{(\sigma(r),r)\}\ \text{with}\ \sum_r x_{\sigma(r)r}=\min_\tau \sum_r x_{\tau(r)r}.$$

The four clauses are needed together: optimality at final states alone holds for an algorithm that never stops.

Milestones

1. Remark (2): subtracting row constants $u_i$ and column constants $v_j$ does not change the optimal assignments.
2. The zeros starred in the Preliminaries are independent.
3. At Step 2 the sequence $Z_0,\dots,Z_{2k}$ exists, is unique and has distinct elements.
4. Step 2 leaves an independent set of starred zeros, larger by one.
5. Lines containing all the zeros number at least the maximal number of independent zeros.
6. At Step 3 the starred zeros are a maximal independent set and the covered lines a minimal cover.
7. At Step 3, $h>0$; the transformation subtracts $h$ from non-covered entries, adds $h$ to twice-covered ones, keeps every $0^*$ and $0'$ a zero, and $n_{k+1}\ge n_k$.
8. If $n_{k+1}=n_k$, Step 2 does not occur before the next Step 3, which begins with more covered rows.
9. While $n_k$ is constant, Step 3 is applied at most $n$ times.
10. Every row and column of the matrix always contains a zero.
11. Step 3 decreases the sum of the entries by $n(n-n_k)h$.

Significance

Correctness of the Hungarian method is the basis of a standard algorithm for the assignment problem and, through it, of methods for transportation problems, minimum-cost bipartite matching and weighted bipartite matching. Its $O(n^3)$ refinements remain in practical use. The invariants of the proof are the primal–dual structure of the problem: the row and column constants subtracted along the way form a dual solution, and the starred zeros at the end are a primal solution satisfying complementary slackness.

The result has been proved since 1957 and is in every textbook on combinatorial optimization. A machine-checked version of Munkres' specific procedure, as a transition system with all its free choices, with finiteness for real (not only integer) matrices, is not available on this platform; Mathlib has no assignment algorithm. The mission produces a verified specification of the algorithm, reusable invariants about covers and independent zeros, and a termination argument that does not rely on integrality.

Difficulty

Optimality at termination is short once the invariants are known. The work lies in two places.

First, the invariants hold only along runs. "Each $0^*$ is covered by precisely one line", "no column contains more than one $0^*$" and "no row contains more than one $0'$" fail for arbitrary marked matrices, so they must be carried as an inductive invariant through every move, including the Step 3 transformation, which keeps the primes.

Second, termination. The obvious measure, the sum of the entries, decreases by $n(n-n_k)h$ at each Step 3, but for real entries $h$ can be arbitrarily small, so the decreasing sum gives no bound on the number of steps. The page replaces this argument by the stronger result of p. 35 (milestone 8), which holds for real entries. Turning it into a proof that every run of the nondeterministic move relation is finite, including the moves inside Step 1 and Step 2, is the core of the formalization.

Formalization scope

• Matrices and positions. Entries are arbitrary reals, as on p. 35. Positions are Fin n × Fin n (row, column).
• Output orientation. The output permutation follows the published definition HeldWolfeCrowder_Assignment_Setting: σ r is the row assigned to column r, the starred positions are $(\sigma(r),r)$, and optimality is IsOptimalAssignment A σ with respect to the original input matrix.
• Nondeterminism. The algorithm is an inductive move relation Step. The order in which the Preliminaries consider the zeros, and the non-covered zero primed in Step 1, are free choices. Every claim holds for every run.
• Relational steps. Step 2's sequence and Step 3's $h$ are described relationally. Their existence, and $h>0$, are theorems, not built into the moves.
• Reachable states. Invariants are stated for states reachable from a start state, never for arbitrary states.
• Finiteness. Finiteness of every run is accessibility (Acc) of each start state for the reversed move relation.
• Termination test after the Preliminaries. "If all columns are covered, stop" is also applied when leaving the Preliminaries. The page goes to Step 1 unconditionally there. If the Preliminaries already star $n$ zeros, Step 3 would then have no non-covered element.
• Independent zeros. The maximal number of independent zeros is a finite maximum of cardinalities, so it has no junk value.
• Edge case $n=0$. No positivity of $n$ is assumed. For $n=0$ the start state is final.
• Ruled out. A goal stating only optimality at final states, or invariants stated for arbitrary states, would be a trivializing formalization; the goal states termination of every run and absence of stuck states as well.

Not formalized: the operation count $(11n^3+12n^2+31n)/6$ of pp. 35–36, whose cost model is informal; the argument that returning to the standard input after Step 3 is unnecessary (pp. 34–35); König's theorem (Remark (1), cited); and §2 on the transportation problem, which is stated without proof.

Welcome contributions: proofs of the milestones, a general library of lines and independent zeros in matrices (reusable for König–Egerváry), and an executable refinement of the move relation.

Selected references

• J. Munkres, Algorithms for the assignment and transportation problems, J. Soc. Indust. Appl. Math. 5 (1957), 32–38. https://doi.org/10.1137/0105003
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. https://doi.org/10.1002/nav.3800020109
• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223 (source of the published assignment-cost definitions reused here)

Motivation

A firm that sells a product line of different qualities cannot see how much each customer values quality. It can only post a price for every quality and let customers choose. Mussa and Rosen's 1978 paper solves the monopolist's problem in this setting and compares the result with the competitive outcome. Their model is, together with Mirrlees' optimal income tax and Maskin and Riley's later treatment of nonlinear pricing, one of the founding examples of screening: the seller designs a menu so that customers sort themselves. The model's main qualitative prediction, that a monopolist degrades the quality sold to every customer except the one who values quality most, is the origin of the phrase "no distortion at the top". Textbooks on contract theory and mechanism design still teach it in this form.

Timeline. Mussa and Rosen (1978) give the first-order analysis, including "bunching" of customers at a common quality when marginal revenue is not monotone. Maskin and Riley (1984) treat the same problem for nonlinear quantity pricing. Myerson (1981) introduced the "ironing" procedure for non-monotone virtual valuations in auction design, which later became the standard way of describing the bunching conditions of this paper.

Setting

Consumer types are numbers $\theta\in[\underline\theta,\bar\theta]$ with $0\le\underline\theta<\bar\theta$, distributed with a density $f$ that is positive and differentiable on the whole interval; $F(\theta)=\int_{\underline\theta}^{\theta}f(s)\,ds$. A consumer of type $\theta$ buys at most one unit, and from quality $q$ at price $p$ gets utility $\theta q-p$. Producing one unit of quality $q\ge0$ costs $C(q)$, where $C(0)=0$, $C$ is twice differentiable, and $C'(q)>0$, $C''(q)>0$ for $q\ge0$.

Under competition, price equals unit cost and type $\theta$ buys the quality $J(\theta)$ with $C'(J(\theta))=\theta$, or nothing when $\theta\le C'(0)$.

The monopolist chooses an assignment $q(\theta)$, the quality bought by type $\theta$. It must be nondecreasing, nonnegative and piecewise differentiable on $[\underline\theta,\bar\theta]$; such assignments are called admissible. Incentive compatibility and participation fix the consumer surplus at $z(\theta)=\int_{\underline\theta}^{\theta}q(s)\,ds$, so the monopolist maximizes

$$\Pi(q)=\int_{\underline\theta}^{\bar\theta}\bigl[\theta\,q(\theta)-z(\theta)-C(q(\theta))\bigr]f(\theta)\,d\theta .$$

An assignment is optimal if it is admissible and maximizes $\Pi$ among admissible assignments. The marginal revenue of quality sold to type $\theta$ is

$$MR(\theta)=\theta-\frac{1-F(\theta)}{f(\theta)} .$$

The paper's analysis runs through the marginal profit of a uniform quality increase for all types $\theta\ge t$,

$$\mu(t)=\int_t^{\bar\theta}\Bigl[\theta-\int_t^\theta ds-C'(q(\theta))\Bigr]f(\theta)\,d\theta .$$

Formalization targets

Goal: quality distortion below the top

For every optimal assignment $q$:

$$C'(q(\theta))<\theta\quad\text{for }\underline\theta\le\theta<\bar\theta,\ \theta>C'(0);\qquad q(\theta)=0\quad\text{for }\underline\theta\le\theta<\bar\theta,\ \theta\le C'(0);$$

and, if $C'(0)<\bar\theta$, the limit $L=\lim_{\theta\uparrow\bar\theta}q(\theta)$ exists and satisfies $C'(L)=\bar\theta$ (if $\bar\theta\le C'(0)$, then $q(\theta)\to0$). In words: $q^m(\theta)<J(\theta)$ for every type below the top that buys under competition, types that do not buy under competition do not buy from the monopolist, and $q^m(\bar\theta)=J(\bar\theta)$.

Milestones

The paper's own chain of claims, in order: $MR(\theta)<\theta$ except at $\bar\theta$ (p. 308); the first-order condition (9), $\Lambda(h;q)\le0$ for every admissible deformation; the identity (10) = (12), $\mu(t)=\int_t^{\bar\theta}[MR-C'(q)]f$; condition (13), $\mu\le0$; condition (15), $\mu=0$ where $\dot q>0$; $\mu=0$ at a jump; the absence of jumps; (17), $C'(q)=MR$ where $\dot q>0$; the bunching conditions (18)–(19); and the absence of a bunch at the top. Companion items state the two-type case of footnote 4, the uniform–quadratic example of §5, and the loss of consumer surplus (§6, "Second").

Significance

The result. The goal says how the monopolist differs from competition: it lowers every quality except the top one, and it never serves a type that competition leaves out. The distortion comes from the gap $\theta-MR(\theta)=(1-F(\theta))/f(\theta)>0$, which closes only at $\bar\theta$. The same comparison underlies results on second-degree price discrimination, regulation of product lines, and versioning of information goods. The bunching conditions (18)–(19) are an early statement of what is now called ironing.

Formalizing it. The result has been proved since 1978 in the economic literature, under the paper's smoothness assumptions and by a variational argument. As far as is known, it has not been machine-checked: no formal library contains the monopoly quality problem, its first-order conditions or the bunching conditions. The mission produces a checked version with the hypotheses made explicit, including the conventions at the endpoints that the paper leaves implicit. The uniform–quadratic example gives a concrete optimum that certifies the hypotheses are satisfiable.

Difficulty

The obvious argument sets $C'(q(\theta))=MR(\theta)$ pointwise and compares with $C'(J(\theta))=\theta$. This fails when $MR$ is not increasing: the pointwise solution is then decreasing somewhere and not admissible. The optimal assignment is constant on some intervals, and on such a bunch $C'(q)\ne MR$ pointwise. The comparison with $J$ there needs the boundary conditions (18)–(19) and the fact that no bunch reaches $\bar\theta$. All of these come from one-sided deformations that respect monotonicity, so the first-order conditions are inequalities and need a separate argument for equality. The paper also asserts without a separate step that optimal assignments have no jumps, and later steps use continuity.

Formalization scope

Types and assignments are real functions on $\mathbb R$; only their values on $[\underline\theta,\bar\theta]$ matter. The type distribution and $MR$ are the published MechanismDesign.Screening.TypeDistribution and virtualValuation. The standing assumptions are hypotheses of every main statement: $f$ is differentiable on $[\underline\theta,\bar\theta]$ (positivity and total mass 1 are part of the distribution), $C(0)=0$, $C$ and $C'$ are differentiable on $\mathbb R$, and $C'>0$, $C''>0$ on $[0,\infty)$. $C(0)=0$ is an added normalization: quality 0 means not buying. "Piecewise differentiable" means differentiable on $(\underline\theta,\bar\theta)$ outside a finite set. The competitive assignment $J=C'^{-1}$ is never formed; every comparison with $J$ is written through $C'$. Admissible deformations $h$ in (9) are required to keep $q+h\ge0$.

The value $q(\bar\theta)$ does not affect $\Pi$, so a statement about $q(\bar\theta)$ itself would be false; the top-type claim is stated as a left limit. Optimality ranges over admissible assignments only. Any reading under which no optimal assignment exists makes the goal vacuous; the §5 companion rules this out, since its optimal assignment has a kink and uses the same notion of optimality.

Needed infrastructure: interval integrals of monotone functions, first variations under monotonicity constraints, and fundamental-theorem-of-calculus arguments for $F$. The incentive-compatibility reduction (monotonicity and the envelope formula) is not posed here, because it is posed on the platform in Börgers' screening chapter. Related platform item: Börgers' Proposition 2.6 (MechanismDesign.Screening.nonlinear_pricing_optimal) treats a linear-cost, concave-valuation model under regularity, which is a different statement. Contributions to any milestone, and reusable lemmas about monotone deformations, are welcome.

Selected references

• M. Mussa and S. Rosen, Monopoly and product quality, Journal of Economic Theory 18 (1978), 301–317. https://doi.org/10.1016/0022-0531(78)90085-6
• E. Maskin and J. Riley, Monopoly with incomplete information, RAND Journal of Economics 15 (1984), 171–196. https://doi.org/10.2307/2555674
• R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6 (1981), 58–73. https://doi.org/10.1287/moor.6.1.58
• J. A. Mirrlees, An exploration in the theory of optimum income taxation, Review of Economic Studies 38 (1971), 175–208. https://doi.org/10.2307/2296779
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 2. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

Motivation

Semiconductor burn-in ovens can process several jobs at once. A group placed in one oven must remain together until the longest job has finished, so increasing batch size saves oven starts but can delay short jobs. When several ovens are available, a scheduler also has to decide which oven receives each batch. Lee, Uzsoy, and Martin-Vega studied this setting and gave guarantees for a simple rule that first groups an arbitrary job list into batches and then sends those batches to the next available oven (Lee, Uzsoy & Martin-Vega 1992, §§2 and 5). Their bounds give a way to assess this easily specified rule against the best possible schedule, even when finding that schedule is difficult.

The paper treats both makespan, the time when all jobs have finished, and maximum lateness, the largest difference between a job's completion time and its due date. These objectives respond differently to batching. The makespan ignores which particular job finishes late; maximum lateness depends on each job's due date. Proposition 4 relates the lateness guarantee to the makespan guarantee of Proposition 1, making the two results a natural formalization unit (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).

Setting

There are $n>0$ jobs, indexed by $j$, with processing times $p_j>0$ and due dates $d_j\ge0$. All jobs are available at time zero. There are $m>0$ identical batch machines, each able to process at most $B>0$ jobs at once. A batch cannot be interrupted or enlarged after it begins, and its processing time is the largest $p_j$ among its members. A schedule partitions the jobs into nonempty batches, chooses a machine for each batch, and orders the batches on each machine. Batches assigned to a machine run one after another from time zero. Every job in a batch finishes when that batch finishes (Lee, Uzsoy & Martin-Vega 1992, p. 766).

For a set of jobs $J$, write $C_{\max}^*(J)$ for the least makespan over all valid batchings and machine assignments. Write $L^*(J)$ for the least possible value of $\max_{j\in J}(C_j-d_j)$, where $C_j$ is job $j$'s completion time. For the full job set, abbreviate these by $C_{\max}^*$ and $L^*$. The maximum due date over all jobs is $d_{\max}=\max_jd_j$.

Batch list scheduling (BLS) begins with any ordering of the jobs. It divides successive entries into full batches of $B$ jobs, apart from a possibly smaller final batch. It then assigns each next batch to a machine that becomes available first. Denote the resulting makespan by $C_{\max}^{\mathrm{BLS}}$ and its maximum lateness by $L$. The guarantee applies to every initial list; it does not require an earliest-due-date or longest-processing-time order (Lee, Uzsoy & Martin-Vega 1992, p. 771, Algorithm BLS).

Formalization targets

Makespan guarantee

Proposition 1 asserts, for every BLS list,

$$C_{\max}^{\mathrm{BLS}}\le\left(B+1-\frac1m\right)C_{\max}^*.$$

The milestone list includes the paper's processing-volume lower bound, $\sum_jp_j/(mB)\le C_{\max}^*$, and Proposition 1 itself. The latter is stated for arbitrary job subsets as well as the full instance, because the paper applies it to a prefix sub-instance in the proof of Proposition 4 (Lee, Uzsoy & Martin-Vega 1992, p. 772).

Relative maximum-lateness guarantee

The mission's goal is the printed ratio of Proposition 4:

$$\frac{L-L^*}{L^*+d_{\max}} \le B-\frac1m+\frac{d_{\max}}{L^*+d_{\max}}.$$

The denominator is positive under the stated conditions, even if the optimal maximum lateness is negative. The remaining milestones record the paper's lower bound $L^*(J)\ge C_{\max}^*(J)-d_{\max}$ for a nonempty sub-instance and its reduction from the full instance to the BLS prefix containing a maximum-lateness job (Lee, Uzsoy & Martin-Vega 1992, p. 773).

Significance

The makespan result controls the cost of using an arbitrary initial list and simple next-available-machine assignments instead of optimizing both the batching and machine allocation. At $B=1$, its factor becomes $2-1/m$, the ordinary list-scheduling factor noted by the authors. Proposition 4 gives a corresponding bound for maximum lateness, normalized in a way that remains meaningful when $L^*<0$ (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).

These are proved results in the 1992 paper. The formalization work is to give their batch model, sub-instance optima, and the printed inequalities machine-checked statements and eventually proofs. The imported library already has definitions of least-loaded list scheduling and optimal assignment makespan for ordinary items on identical machines. This mission adds the batch layer, its lateness objective, and the comparison between the batch algorithm and unrestricted batch schedules. The Lean declarations here compile as open theorem targets; this proposal does not claim completed machine-checked proofs.

Difficulty

The processing time of a batch is a maximum, while its contribution to the volume of jobs is a sum. Treating each batch as an ordinary job gives a list-scheduling instance, but it does not by itself compare that instance's optimum with the optimum over all ways to form batches. That gap is central to the makespan bound. The lateness goal has a second obstacle: the job that determines the BLS maximum lateness may sit in a batch that is not the last to finish, and due dates prevent a direct substitution of a makespan bound for a lateness bound. Moreover, $L^*$ may be negative, so dividing by it would not give a valid relative error. The stated normalization and its positivity require explicit attention (Lee, Uzsoy & Martin-Vega 1992, proof of Proposition 4).

Formalization scope

Jobs are Fin n and machines are Fin m; the paper's first job is Lean index zero. Processing times and due dates are real numbers. The paper's integer-data convention is sufficient for these inequalities but is not needed for their statements. Processing times are positive, all jobs are available at time zero, and the lateness goal requires nonnegative due dates. This last condition makes explicit what the paper's final inequality uses: allowing negative due dates makes Proposition 4 false. The full job set is nonempty. Prefix jobs are the first batches of the given arbitrary list, and the optimal values for a prefix range over every valid batching and assignment of those jobs.

The BLS implementation chunks the list into full batches and a final remainder. A batch is sent to a least-loaded machine, which is the first machine to become free when no idle time is inserted. The published list-scheduling definitions of NumStochOpt.ListScheduling supply this rule and the ordinary assignment optimum. They select the lowest machine index on a tie; identical-machine labels do not affect the resulting completion times. Machine schedules are represented by an ordered batch list and an assignment, with each machine processing its own batches back to back. No bound is obtained by defining the optimum over BLS-shaped consecutive batches, and no theorem fixes a favorable job list.

The mission covers correctness inequalities, not the paper's running-time claims or its later BLPT rule. Useful contributions include proofs of the four milestones, finite-schedule facts showing the optima are attained, and reusable links between batch completion times and least-loaded list scheduling. The parallel batch model can also support other objectives and scheduling rules.

Selected references

• C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. DOI: 10.1287/opre.40.4.764.

Motivation

Burn-in is the final testing stage of semiconductor manufacturing: finished integrated circuits are loaded on boards and held in an oven at high temperature for a prescribed minimum time, so that weak devices fail before shipment. An oven holds many boards at once, a load cannot be interrupted, and a board may stay in the oven longer than its specified time but never shorter. Because burn-in times are long compared to the other test operations, the ovens are frequently the bottleneck of the test facility, and the order in which lots enter them determines whether customer due dates are met.

Lee, Uzsoy and Martin-Vega (Operations Research 40(4), 1992) modelled an oven as a batch processing machine and gave polynomial algorithms for several due-date objectives. This mission covers the first of them: one machine, jobs with release times and a common processing time, and the question whether every job can be completed by its due date. Ikura and Gimple (Operations Research Letters 5(2), 1986) had already given an $O(n^2)$ algorithm for this feasibility question when release times and due dates are agreeable; the paper replaces it by a simpler dynamic program, DP1, and uses DP1 with a bisection search to minimize the maximum tardiness.

Setting

There are $n$ jobs, indexed $1, \dots, n$. Job $i$ has a release time $r_i$ (it cannot be processed earlier), a due date $d_i$, and the common processing time $p$; all data are natural numbers. One machine processes up to $B \ge 1$ jobs simultaneously.

A batch schedule of a set $J$ of jobs is a sequence of batches $P_1, \dots, P_m$: nonempty, pairwise disjoint sets of at most $B$ jobs whose union is $J$, processed in this order. A batch cannot be interrupted, and no job joins it once it has started. It starts as soon as the previous batch is finished and all its jobs are released, and it takes time $p$:

$$C(P_k) = \max\{r(P_k),\, C(P_{k-1})\} + p,\qquad r(P) = \max\{r_i : i \in P\},\qquad C(P_0) = 0 .$$

Job $i$ completes at $C_i = C(P_k)$ for the batch $P_k \ni i$; the makespan is $C_{\max} = C(P_m)$. A schedule is feasible (has $T_{\max} = 0$) if $C_i \le d_i$ for every job, and its maximum tardiness is $T_{\max} = \max_i \max\{0, C_i - d_i\}$.

Release times and due dates are agreeable if $r_i < r_j$ implies $d_i \le d_j$. A schedule is in batch-EDD order if no job of an earlier batch has a larger due date than a job of a later batch.

Algorithm DP1. With the jobs indexed in nondecreasing order of due dates, let $f(0) = 0$ and, for $j \ge 1$,

$$f(j) = \min_{\max\{1,\,j-B+1\} \le i \le j} f_i(j),\qquad f_i(j) = \begin{cases} \max\{f(i-1), r_j\} + p & \text{if } \max\{f(i-1), r_j\} + p \le d_i,\\ \infty & \text{otherwise.}\end{cases}$$

Formalization targets

Goal: correctness of DP1

For an index order nondecreasing in both $d$ and $r$, and every $0 \le j \le n$,

$$f(j) = \min\{\, C_{\max}(S) : S \text{ a feasible batch schedule of jobs } 1,\dots,j \,\},\qquad \min\emptyset = \infty .$$

The minimum ranges over all batch schedules of the prefix: every batching and every batch order. The case $j = n$ is the paper's statement that DP1 "will find a feasible schedule with minimum makespan if a feasible schedule exists" (p. 768).

Milestones

1. Lemma 1 (p. 767): if a feasible schedule exists, a feasible schedule in batch-EDD order exists.
2. Justification of DP1 (p. 768): every feasible schedule of jobs $1, \dots, j$ can be replaced by a feasible schedule whose batches are blocks of at most $B$ consecutively indexed jobs, in increasing index order, with no larger makespan, so the problem "becomes a consecutive partition problem".
3. Lemma 2 (p. 769): under $r_j + p \le d_j$ for all $j$, some schedule has $T_{\max} \le (n-1)p$.

Significance

DP1 decides feasibility of $1/r_i, p_i = p, B/T_{\max}$ and, when the instance is feasible, returns the minimum makespan of an on-time schedule. Applied to due dates augmented by a trial value $T$, it decides whether $T_{\max} \le T$ is achievable, which together with the bound of Lemma 2 gives the paper's polynomial procedure for minimizing $T_{\max}$. The consecutive-partition structure behind it recurs in the paper's later dynamic programs (DP2 for agreeable processing times and due dates, DP3 for the number of tardy jobs), and in much of the later literature on batch scheduling with release dates.

The results are proved in the paper; none of them has a machine-checked proof. The mission formalizes the known proofs. Its formal statements also make explicit two assumptions that the printed text leaves loose: the tie-break of the index order, without which DP1 returns a wrong value, and the hypothesis $r_j + p \le d_j$ of Lemma 2, without which the lemma is false.

Difficulty

The obvious argument for the goal is "by Lemma 1 the batches are consecutive, and DP1 enumerates consecutive partitions". Lemma 1 orders the batches by due dates, but it does not make the batches intervals of the index order: jobs with equal due dates may still be split across batches in an order that is not the index order, and when equal due dates are indexed against the release order DP1's value $\max\{f(i-1), r_j\} + p$ underestimates the start of the batch $\{i, \dots, j\}$. The step from batch-EDD order to consecutive batches, and the fact that the exchange never increases the makespan, are the content of the justification milestone. The goal also asserts two directions at once: that the DP value is attained by some feasible schedule, and that no feasible schedule, consecutive or not, finishes earlier.

Formalization scope

Jobs are Fin n, 0-based (the paper's job $i$ is i - 1); a prefix "jobs $1, \dots, j$" is a prefix length $j \le n$. Data are natural numbers, as the paper assumes ("all data to be integers", p. 769). A batch schedule is a List (Finset (Fin n)); schedules are semi-active, starting every batch as early as possible, which loses nothing for the regular objectives here. DP1 is a def written as printed, with values in ℕ∞ and $\infty = \top$; the minimum in the goal is an infimum in ℕ∞ over all valid feasible schedules, so its value on an infeasible prefix is $\top$.

Explicit readings of loose phrases:

• "Jobs are indexed in increasing order of due dates" (p. 767): the index order is nondecreasing in both $d$ and $r$. Such an order exists for agreeable data (sort by $(d, r)$), and it implies agreeability. With ties in $d$ ordered against $r$ the goal is false: $B = 2$, $p = 1$, $d = (2, 2)$, $r = (1, 0)$ gives $f(2) = 1$, while every schedule finishes at time $2$.
• "Agreeable" is printed as "$r_i \le r_j$ implies $d_i \le d_j$"; the strict form $r_i < r_j \Rightarrow d_i \le d_j$ is used, a weaker hypothesis.
• "A solution with $T_{\max} = 0$" is a batch schedule in which every job is on time.
• "$(n - 1)p$ is an upper bound on the value of $T_{\max}$" (Lemma 2) is read as a bound on the optimal $T_{\max}$, with the hypothesis $r_j + p \le d_j$ that its proof invokes ("by assumption $r_j + p < d_j$"), in the weak form.
• "If $f(j) \le d_j$, then it is possible to schedule jobs $1, \dots, j$ so that none are tardy" is not formalized separately; it is subsumed by the goal.

Not formalized: the $O(nB)$ running time of DP1, Algorithm 1 (bisection over $T_{\max}$) and Corollary 1, whose content is a running time. A formalization that restricts the minimum in the goal to consecutive or batch-EDD schedules would assume the milestones and is excluded; so is a DP value defined as the optimum itself.

The development needs list-based schedule recursions and ℕ∞ arithmetic only; the exchange lemmas for batch schedules (moving a job between batches without delaying later batches) are reusable for the paper's other dynamic programs. Proofs of any milestone, and of auxiliary lemmas on finish, jobCompletion and permutations of batch lists, are welcome.

Selected references

• C.-Y. Lee, R. Uzsoy, L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. https://doi.org/10.1287/opre.40.4.764
• Y. Ikura, M. Gimple, Scheduling Algorithms for a Single Batch Processing Machine, Operations Research Letters 5(2), 61–65, 1986. https://doi.org/10.1016/0167-6377(86)90092-7

Burn-in ovens as batch processing machines

In semiconductor manufacturing, finished chips go through burn-in: they are loaded on boards and held in an oven at high temperature to expose early failures. An oven holds a bounded number of boards, a load cannot be interrupted once started, and a chip may stay in the oven longer than its specified burn-in time but not shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model the oven as a batch processing machine and give polynomial algorithms for several due-date objectives. The model has since become a standard one in scheduling theory; the survey of Potts and Kovalyov (2000) traces the batching literature that grew from it.

This mission formalizes the part of the paper's §3 on minimizing maximum tardiness when all jobs are available at time $0$ and processing times and due dates are agreeable. That is the problem the paper writes $1/B/T_{\max}$. The paper's own route is a feasibility test by dynamic programming, Algorithm DP2, which a bisection over due-date shifts turns into a $T_{\max}$ minimizer.

The batch machine

There are $n$ jobs $1,\dots,n$. Job $i$ has a processing time $p_i$ and a due date $d_i$, both natural numbers. The machine has capacity $B\ge 1$. A batch is a nonempty set of at most $B$ jobs processed together. It occupies the machine for the processing time of its longest job,

$$t(P)=\max_{i\in P}p_i .$$

A batch schedule of a job set $J$ is a sequence $S=(P_1,\dots,P_m)$ of pairwise disjoint batches covering $J$, processed in this order and back to back from time $0$. Batch $P_k$ and all of its jobs complete at $C(P_k)=t(P_1)+\dots+t(P_k)$. The makespan is $C_{\max}(S)=C(P_m)$, and the maximum tardiness is

$$T_{\max}(S)=\max_k\max_{i\in P_k}\max\{0,\,C(P_k)-d_i\}.$$

A schedule is feasible when $T_{\max}(S)=0$, that is, when every job meets its due date.

A sequence is in batch-EDD order (Definition 1) if no job in an earlier batch has a strictly later due date than a job in a later batch. Processing times and due dates are agreeable if $p_i<p_j$ implies $d_i\le d_j$. A schedule is consecutive when every batch is a block $\{i,i+1,\dots,k\}$ of indices and the blocks appear in increasing order.

Algorithm DP2 computes values $f(0),\dots,f(n)\in\mathbb N\cup\{\infty\}$:

$$f(0)=0,\qquad f(j)=\min_{\max\{1,\,j-B+1\}\le i\le j} f_i(j),\qquad f_i(j)=\begin{cases}f(i-1)+p_j,& f(i-1)+p_j\le d_i,\\ \infty,&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: correctness of DP2

Index the jobs so that $d_1\le\dots\le d_n$ and $p_1\le\dots\le p_n$. Then for every $0\le j\le n$,

$$f(j)=\min\{\,C_{\max}(S) : S \text{ a batch schedule of jobs } 1,\dots,j,\ T_{\max}(S)=0\,\},$$

with $\min\emptyset=\infty$. The minimum ranges over all schedules: any batching, any order. This is the paper's reading of $f(j)$ as "the minimum completion time of jobs $1,\dots,j$ if they can be scheduled feasibly, and infinity otherwise".

Milestones

1. Lemma 3. With agreeable processing times and due dates, if a feasible schedule exists, then a feasible schedule in batch-EDD order exists.
2. Consecutive partition (justification of DP2). Under the index order above, if jobs $1,\dots,j$ can be scheduled feasibly, then some feasible schedule of minimum makespan is consecutive.
3. FBEDD. With equal processing times and due dates in index order, the Full-Batch EDD schedule $\{1,\dots,B\},\{B+1,\dots,2B\},\dots$ has $T_{\max}$ no larger than that of any batch schedule.

Significance

DP2 is the paper's feasibility test for $1/B/T_{\max}$ with agreeable data. With a bisection over the common shift of the due dates, it yields a polynomial algorithm for minimizing $T_{\max}$. A correct statement of what DP2 computes is therefore the core of that result. The same consecutive-partition structure underlies the paper's DP1 (release times, equal processing times) and DP3 (number of tardy jobs), which are separate missions of this series.

No machine-checked proof of any of these statements is known. The dynamic program's correctness is argued in the paper only by reference ("the justification of this algorithm is similar to that of algorithm DP1"), and the index order it needs is left implicit. A formal proof pins down exactly which ordering of the jobs makes the recursion correct.

Difficulty

The recursion charges $p_j$ for the last batch $\{i,\dots,j\}$ and checks only $d_i$. Both shortcuts rely on the jobs being sorted by due date and by processing time at the same time. Lemma 3's exchange argument sorts a feasible schedule by due date, but it does not by itself produce consecutive blocks of a fixed index order. With ties in due dates the indexing also has to be compatible with processing times. Without that, the recursion is wrong: for $B=2$, $p=(3,1)$, $d=(5,5)$ it gives $f(2)=1$, while every schedule takes at least $3$. The goal compares the DP with the optimum over all schedules, so the exchange arguments have to bridge arbitrary batchings and the consecutive ones the recursion enumerates. That bridge is the main step left to prove.

Formalization scope

• Jobs are Fin n (job $i$ of the paper is index $i-1$); jobs $1,\dots,j$ are jobsUpTo n j. Data are natural numbers; the paper assumes integral data (p. 769).
• A schedule is a List (Finset (Fin n)); validity requires nonempty batches of size at most $B$ inside the job set, pairwise disjoint, covering the set. Batches start as early as possible. Batch time is the maximum processing time in the batch.
• $\infty$ is ⊤ : ℕ∞, and the goal's minimum is the infimum in ℕ∞, which is ⊤ exactly when no feasible schedule exists. DP2 is defined by the printed recursion, not as an optimum.
• Explicit readings of loose phrases:
  • "jobs are indexed in increasing order of due dates" (p. 767) becomes Monotone d ∧ Monotone p for DP2 and its justification, and Monotone d for FBEDD;
  • "agreeable" (printed "$p_i\le p_j$ implies $d_i\le d_j$", which would force equal due dates for equal processing times) becomes the strict form $p_i<p_j\Rightarrow d_i\le d_j$, a weaker hypothesis;
  • "optimally solves" for FBEDD becomes "valid, and $T_{\max}$ at most that of every valid schedule";
  • "a consecutive partition problem" becomes the existence of a consecutive minimum-makespan feasible schedule.
• Not formalized: the $O(nB)$ and $O[nB\log_2(np_{\max})]$ running times, the bisection procedure, and the remark that $np_{\max}$ bounds $T_{\max}$.
• Trivializations ruled out: the goal's minimum ranges over all valid schedules, not only batch-EDD or consecutive ones (which would assume the milestones), and DP2 is the printed recursion, not a restatement of the optimum.
• Infrastructure needed: list-indexed schedules, exchange arguments on adjacent batches, and induction on prefix length for the recursion. The single-machine batch model is shared in spirit with missions 1 and 3 of this series. No published platform definition was reused, since nothing on batch machines exists yet.

Selected references

• C.-Y. Lee, R. Uzsoy, L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. https://doi.org/10.1287/opre.40.4.764
• Y. Ikura, M. Gimple, Efficient scheduling algorithms for a single batch processing machine, Operations Research Letters 5(2), 61–65, 1986. https://doi.org/10.1016/0167-6377(86)90104-5
• C. N. Potts, M. Y. Kovalyov, Scheduling with batching: A review, European Journal of Operational Research 120(2), 228–249, 2000. https://doi.org/10.1016/S0377-2217(99)00153-8

Motivation

Minimizing the weighted number of tardy jobs on a single machine, written $1\|\sum w_jU_j$ in later scheduling notation, is one of the basic due-date objectives: each job either meets its deadline or pays a fixed penalty, and the question is which jobs to sacrifice. Moore (Management Sci. 15, 1968) solved the unweighted case $p_j = 1$ with a greedy procedure. Lawler and Moore (Management Sci. 16, 1969) handled arbitrary weights by recasting the problem as a knapsack problem with nested prefix constraints and solving it by a recursion, their Equation (3). This is the classical pseudo-polynomial algorithm for the weighted problem; Lenstra, Rinnooy Kan and Brucker (Ann. Discrete Math. 1, 1977) showed that the weighted problem is NP-hard, so a pseudo-polynomial method is the expected kind of exact algorithm.

The paper's Sections 5 and 6 state the reduction in a few sentences: on-time jobs can be taken in deadline order, the problem is "equivalent" to the prefix-constrained knapsack, and (3) solves the latter. This mission turns those sentences into precise statements.

Setting

There are $n \ge 1$ jobs, processed by a single machine one immediately following the other from time $0$. Job $j$ has a nonnegative integer processing time $a'_j$, a nonnegative integer deadline $d_j$ and a penalty $p_j \ge 0$. A sequence $\sigma$ is an ordering of all jobs; job $j$ completes at time $C_j(\sigma)$, the total processing time of job $j$ and the jobs before it. Job $j$ is tardy in $\sigma$ if $C_j(\sigma) > d_j$, and the total loss of $\sigma$ is

$$W(\sigma) = \sum_{j \text{ tardy in } \sigma} p_j ,$$

the loss $c_j(t)$ being $0$ for $t \le d_j$ and $p_j$ for $t > d_j$.

The jobs are numbered by deadline, $d_1 \le d_2 \le \cdots \le d_n$. A 0–1 vector $x$ ($x_j = 1$: job $j$ on time; $x_j = 0$: tardy) is prefix-feasible if

$$a'_1x_1 + \cdots + a'_kx_k \le d_k \qquad (k = 1, \dots, n).$$

Equation (3) defines $f(j,t)$ for $j = 0, \dots, n$ and integer $t$:

$$f(j,t) = \begin{cases}\max\{f(j,t-1),\ f(j-1,t),\ p_j + f(j-1,t-a'_j)\}, & 0 \le t \le d_j,\\ f(j, d_j), & t > d_j,\end{cases}$$

with $f(0,t) = 0$ for $t \ge 0$ and $f(j,t) = -\infty$ for $t < 0$.

Formalization targets

Goal: the minimum weighted number of tardy jobs

With $d_1 \le \cdots \le d_n$ and $p_j \ge 0$, $f(n, d_n)$ is finite and

$$\min_{\sigma} W(\sigma) = \sum_{j=1}^n p_j - f(n, d_n).$$

This is the paper's claim that the problem "is solved by" its recursion, with the evaluation point made explicit.

Milestones (Section 5, Section 6, Eq. (3))

1. Section 5. For any sequence, the on-time jobs, sequenced in order of their deadlines and followed by the tardy jobs in arbitrary order, stay on time, and the total loss does not increase.
2. Section 6. Every sequence has a prefix-feasible $x$ with $\sum p_j - \sum p_jx_j \le W(\sigma)$, and every prefix-feasible $x$ has a sequence with $W(\sigma) \le \sum p_j - \sum p_jx_j$: the two problems have the same optimal value.
3. Eq. (3). For $0 \le j \le n$ and $t \ge 0$,

$$f(j,t) = \max\Bigl\{\textstyle\sum_{i \le j} p_ix_i : \sum_{i\le k} a'_ix_i \le d_k\ (k \le j),\ \sum_{i\le j} a'_ix_i \le t\Bigr\}.$$

The goal follows from milestones 2 and 3 at $j = n$, $t = d_n$.

Significance

The result is the exact algorithm for $1\|\sum w_jU_j$ with running time proportional to $n\,d_n$, and the reduction behind it (on-time jobs in earliest-deadline order, then a knapsack over the on-time set) is the template reused by later work on due-date objectives, including the two-agent and batching variants. The prefix-constrained knapsack itself reappears whenever a set of jobs must be feasible under nested capacity limits.

On formalization: the paper's argument is three sentences long and leaves several points implicit: the base cases of (3), the role of the deadline numbering, the sign of the penalties, and what "equivalent" means. A machine-checked development fixes each of them and yields a verified pseudo-polynomial algorithm for an NP-hard scheduling problem. To our knowledge none of these statements has a machine-checked proof; the platform's SchedComplexity.OneMachine.* items (Lenstra, Rinnooy Kan and Brucker) state the NP-hardness of the same problem in another model, MooreLateJobs.NumLate.* covers Moore's unweighted case, and TwoAgentSched.LateLate.lemma_7_1 is a two-agent analogue of milestone 1.

Difficulty

The obvious argument works with the set of on-time jobs and asserts that this set can be sequenced on time iff its earliest-deadline order is. That step is Jackson's rule, an exchange argument on lists that is not in Mathlib; it is where both milestone 1 and the first half of milestone 2 sit. The second half of milestone 2 needs the deadline numbering: for a job $k$ that is tardy, the prefix constraint at $k$ is not a completion-time constraint of any job, and only the monotonicity $d_i \le d_k$ for the last on-time job $i \le k$ bounds it. Milestone 3 is a dynamic-programming correctness proof in which the cap $f(j,t) = f(j,d_j)$ for $t > d_j$ and the $-\infty$ base cases must be tracked through a well-founded recursion on $(j, t)$.

Formalization scope

Jobs are Fin n, 0-based: Lean job $j$ is the paper's job $j+1$, and the paper's $f(j,\cdot)$ uses Lean job ⟨j-1, _⟩. Sequences are lists in the published model MooreLateJobs.Shared (IsSchedule Finset.univ l, completionTime, no idle time, start at $0$), which replaces the paper's permutation $\pi$; tardy jobs are the published MooreLateJobs.NumLate.lateSet (strictly $d_j < C_j$). Processing times and deadlines are natural numbers, penalties real. Vectors $x$ are Fin n → Bool. $f$ takes values in WithBot ℝ, with $\bot = -\infty$ and $p + \bot = \bot$; $+\infty$ never occurs.

Explicit readings of the paper's loose phrases:

• Integer data: (3) steps $t$ by $1$ and subtracts $a'_j$, so $a'_j$ and $d_j$ are nonnegative integers.
• Penalties $p_j \ge 0$ ("a penalty $p_j$ is exacted"); the goal, milestone 1 and milestone 2 assume it, milestone 3 does not need it.
• Deadline numbering ("ordering the jobs by deadlines") is Monotone d on the job index; assumed in the goal and milestone 2 only.
• Base cases of (3) are those of Equation (1), with $-\infty$ for a maximum: $f(0,t) = 0$ ($t \ge 0$), $f(j,t) = -\infty$ ($t < 0$). The dominated term $f(j,t-1)$ is kept as printed.
• "Equivalent" is the pair of inequalities of milestone 2, i.e. equal optimal values.
• "Solved by" means $f(n,d_n)$ is finite and $\sum p_j - f(n,d_n)$ is the least weighted number of tardy jobs (IsLeast over all schedules); $n \ge 1$ only so that $d_n$ exists.
• "Arbitrary order" of the tardy jobs in milestone 1 is a universal quantifier over the remaining lists.

Section 5 literally applies Equation (1) with $a_j = a'_j$, $\alpha_j(t) = 0$, $b_j = 0$, $\beta_j(t) = p_j$; read literally, that leaves the deadlines unenforced, so the mission formalizes the paper's own corrected form (3) instead. Trivializing formalizations are ruled out: the weighted number of tardy jobs is defined from completion times, not through $x$; the optimum is a minimum over sequences, not defined as $f$; (3) keeps its cap $f(j,t) = f(j,d_j)$; the goal assumes $p_j \ge 0$ and sorted deadlines, without which it is false.

Infrastructure: an exchange lemma for earliest-deadline order on lists (Jackson's rule, posed on the platform as MooreLateJobs.NumLate.jackson) and well-founded-recursion lemmas for WithBot ℝ maxima are reusable beyond this mission. Proofs of any milestone, and of Jackson's rule, are welcome.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1), 1969, 77–84. https://doi.org/10.1287/mnsc.16.1.77
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Tardy Jobs, Management Science 15(1), 1968, 102–109. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 1977, 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X

Motivation

Many single-machine scheduling problems have a structure that is easy to describe: the jobs must be processed in an order that is already known, and the only decisions are how and when to process each one. Lawler and Moore, in A Functional Equation and Its Application to Resource Allocation and Sequencing Problems (Management Science 16(1), 1969, 77–84), isolate this situation in its simplest form: each job has two processing modes, and each mode has its own processing time and loss as a function of the completion time. They solve it with a single functional equation, Eq. (1), closely related to the recursion for the knapsack problem.

The point of the paper is that Eq. (1) solves more than this fixed-order problem. Later sections apply it to resource allocation in critical-path scheduling and to several sequencing problems with deadlines, including minimization of the weighted number of tardy jobs, often written $1\|\sum w_jU_j$. Everything in those applications rests on the claim checked in this mission: that the recursion computes the minimum loss it is said to compute.

Setting

There are $n$ jobs, performed one at a time in the fixed order $1, 2, \dots, n$. Job $j$ can be performed in one of two modes. In the first mode it takes $a_j$ time units, and a loss $\alpha_j(t)$ is incurred if it is completed at time $t$. In the other mode it takes $b_j$ time units, with loss $\beta_j(t)$. Times are nonnegative integers.

A mode assignment $m$ picks a mode for each job, which fixes its processing time $p_j \in \{a_j, b_j\}$. A feasible timing of the first $j$ jobs is a vector of completion times $c_1, \dots, c_j$ with

$$c_{i-1} + p_i \le c_i \qquad (i = 1, \dots, j), \qquad c_0 = 0,$$

so each job starts at time $0$ or later and after its predecessor has finished; idle time between jobs is allowed. The total loss $L_j(m, c)$ is the sum of $\alpha_i(c_i)$ over the jobs $i \le j$ in the first mode and of $\beta_i(c_i)$ over the others. The problem asks for the mode assignment and timing of all $n$ jobs that minimize $L_n(m, c)$.

The paper's recursion is defined for $j = 0, \dots, n$ and integer $t$, with values in $\mathbb R \cup \{+\infty\}$:

$$f(0, t) = 0 \ (t \ge 0), \qquad f(j, t) = +\infty \ (t < 0),$$ $$f(j, t) = \min\{f(j, t-1),\ \alpha_j(t) + f(j-1, t-a_j),\ \beta_j(t) + f(j-1, t-b_j)\} \quad (j \ge 1,\ t \ge 0). \tag{1}$$

Formalization targets

Milestone: Eq. (1) computes the constrained minimum

For $0 \le j \le n$ and every integer $t$, let $\mathcal L(j, t)$ be the set of total losses of the first $j$ jobs over all mode assignments and feasible timings with $c_j \le t$. Then

$$f(j, t) = \min \mathcal L(j, t),$$

meaning: $f(j, t) = +\infty$ exactly when $\mathcal L(j, t)$ is empty, and otherwise $f(j,t)$ is an element of $\mathcal L(j,t)$ and a lower bound for it. No assumption is made on the losses.

Goal: $f(n, T)$ solves the problem

If every $\alpha_j$ and $\beta_j$ is monotone nondecreasing and

$$T = \sum_{j=1}^n \max\{a_j, b_j\},$$

then $f(n, T)$ is finite and equals the minimum of $L_n(m, c)$ over all mode assignments and all feasible timings of the $n$ jobs, with no deadline. This is the paper's sentence "The problem is solved by the calculation of $f(n, T)$, where $T$ is a sufficiently large number. For example, if all of the $\alpha_j$'s and $\beta_j$'s are monotone nondecreasing, we may choose $T = \sum_{j=1}^n \max\{a_j, b_j\}$."

Significance

The milestone is the correctness of a dynamic program: the value table computed by (1) coincides with the optimum of a combinatorial problem whose feasible set is infinite (timings are unbounded because of idle time). The goal turns that into a finite certificate for the unconstrained problem, with an explicit horizon. Downstream, the same equation with $b_j = 0$ and suitable losses is the paper's algorithm for the weighted number of tardy jobs (§5–6), and the other sequencing applications are specializations of (1) as well; a formal version of this mission is the base on which those reductions can be stated.

The result is classical and its proof is short on paper. It has not been formalized: no item on Prove2Me states a two-mode fixed-order recursion. The work this mission asks for is a machine-checked proof of the two statements above, from the paper's own definitions.

Difficulty

The paper gives no argument beyond "the usual dynamic programming argumentation". The recursion is in two variables: $f(j, \cdot)$ refers to itself at $t-1$ as well as to $f(j-1, \cdot)$, so the correspondence with timings is not a plain stage-by-stage principle of optimality. The edge cases are where a careless reading fails: $t = 0$, where $f(j, -1) = +\infty$; zero processing times $a_j = 0$ or $b_j = 0$, where $f(j-1, t-a_j)$ is evaluated at the same $t$; and $j = 0$, where the deadline constraint degenerates to $0 \le t$. The goal is harder than the milestone: the problem's feasible set is unbounded, and the horizon $T$ is only sufficient under monotone losses. Without monotonicity the goal is false: one job with $a = b = 1$, $\alpha(1) = 5$, $\alpha(t) = 0$ for $t \ge 2$ and $\beta \equiv 5$ has optimum $0$, attained only at completion time $2 > T = 1$, while $f(1, 1) = 5$.

Formalization scope

• Jobs are Fin n and 0-based: Lean job i is the paper's job $i+1$. The recursion f takes the number $j \in \{0,\dots,n\}$ of jobs done; for $j > n$ its value is $+\infty$ and is never used.
• Modes are Bool, with true the first mode ($a_j$, $\alpha_j$). Processing times are natural numbers and may be $0$. Losses are real-valued functions of the natural-number completion time.
• Integer time is an explicit reading: the paper's recursion steps $t$ by one, so time is discrete.
• $+\infty$ is ⊤ : WithTop ℝ, so $x + (+\infty) = +\infty$ as in the paper.
• Idle time is allowed, and the first job starts at time $0$ or later.
• "Minimum total loss" is read as an attained least element of the set of total losses, with $+\infty$ exactly when that set is empty. "The problem is solved by $f(n, T)$" is read as: $f(n, T)$ is finite, at most every feasible total loss, and attained.
• "Monotone nondecreasing" is Monotone on the completion time; it is a hypothesis of the goal only.

The optimum is defined from the scheduling problem itself (lossesBy, IsFeasible, totalLoss), never as $f$; statements in which the optimum is $f$ again, timings forced to have no idle time, an $\mathbb R$-valued $f$ with an arbitrary value for $t < 0$, or monotone losses assumed in the milestone are all ruled out by this choice of definitions.

Related platform items: GilmoreGomory61.CuttingStock.knapsack_dp_recursion (an unbounded-knapsack recursion) and the CriticalPath.CostCurve items (Kelley's continuous time–cost model) treat neighbouring recursions and models; neither states this problem. Proofs of the milestone and the goal, and reusable lemmas about the value function, are welcome.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://doi.org/10.1515/9781400835386
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102