Operations Research

Motivation

A loss network carries calls that require capacity on one or more links. A call is accepted only when every required link has enough free circuits; otherwise it is lost. This makes the traffic on different links dependent even when calls on different routes arrive independently. Network operators need to know where capacity constraints bind and how offered traffic is converted into carried traffic. Kelly's 1991 survey develops a continuous optimization problem that identifies a characteristic flow vector and gives a linkwise description of blocking in this setting. Kelly, Loss networks (1991), §§1.2 and 2.1.

The paper begins with the equilibrium distribution of the discrete network and uses a continuous relaxation when analyzing its likely state. The resulting primal problem is useful beyond the original probability calculation because it links route flows, capacity constraints, and a convex dual. Theorem 2.8 collects the existence, uniqueness, and correspondence statements for these descriptions. This mission targets that theorem and the intermediate claims Kelly states in §2.1. Kelly (1991), pp. 327–329.

Setting

There are finitely many links $j$ and finitely many routes $r$. Link $j$ has $C_j$ circuits, and one call on route $r$ uses $A_{jr}$ circuits there, with $A_{jr}$ a nonnegative integer. Calls request route $r$ at positive offered rate $\nu_r$. The matrix $A$ need not be a zero–one incidence matrix: one call may use more than one circuit on a link. Kelly's fixed-routing model and its general integer matrix are described in §1.2. Kelly (1991), p. 321.

A real route-flow vector $x=(x_r)$ is primal feasible if $x_r\ge0$ for every route and $\sum_r A_{jr}x_r\le C_j$ for every link. The objective is

$$F(x)=\sum_r\bigl(x_r\log\nu_r-x_r\log x_r+x_r\bigr),$$

with $x_r\log x_r=0$ at $x_r=0$. The primal optimum maximizes $F$ over precisely this feasible set. This is the continuous problem (2.1), rather than an optimization over the integer-valued network state. Kelly (1991), p. 327, (2.1).

A nonnegative vector $y=(y_j)$ assigns one multiplier to each link. The dual objective is

$$D(y)=\sum_r\nu_r\exp\!\left(-\sum_jy_jA_{jr}\right)+\sum_jy_jC_j, \qquad y_j\ge0.$$

A blocking vector $B=(B_j)$ has $0\le B_j<1$. Its carried route flow is $\nu_r\prod_i(1-B_i)^{A_{ir}}$. The conditions on $B$ say that the total carried flow through link $j$ equals $C_j$ when $B_j>0$, and is at most $C_j$ when $B_j=0$. The multiplier and blocking coordinates are related by $B_j=1-e^{-y_j}$, equivalently $y_j=-\log(1-B_j)$. These are equations (2.3), (2.6), and (2.7). Kelly (1991), p. 328.

Formalization targets

Theorem 2.8: primal optimum, blocking solutions, and dual optima

The goal first asserts that the primal problem has exactly one optimizer. Every blocking solution must describe that same optimizer:

$$x_r=\nu_r\prod_j(1-B_j)^{A_{jr}}\quad\text{for every route }r.$$

It also asserts that a blocking solution exists, and that it is unique if $A$ has rank $J$, the number of links. Finally, the transformations $B_j=1-e^{-y_j}$ and $y_j=-\log(1-B_j)$ give a bijection between all blocking solutions and all dual optima. The formal goal includes both directions and both inverse identities, even when the dual optimizer is not unique. Kelly (1991), p. 329, Theorem 2.8.

Claims leading to the theorem

The milestone list follows Kelly's stated progression: unique primal attainment; the Lagrangian maximum and the dual value in (2.2); feasibility and complementary slackness in (2.4)–(2.5); the substitution (2.6); dual attainment; both directions of the blocking–dual correspondence; and strict convexity plus uniqueness under full row rank. One direction of the correspondence is an existing, proved platform theorem, KellyStochasticNetworks.dual_optimum_conditions; it is referenced directly. The other direction remains a new target. Kelly (1991), pp. 327–329.

Significance

The theorem makes the carried flow uniquely determined even when several blocking vectors or dual optimizers describe it. Under full row rank, it also identifies a unique linkwise blocking vector. Its correspondence lets a statement in the flow language be translated to a statement in the multiplier language without selecting a preferred optimizer. The interpretation following Theorem 2.8 explains the linkwise condition: positive blocking occurs only on a saturated link. Kelly (1991), p. 329, discussion after Theorem 2.8.

The mathematical result was proved in the source paper. The work here is to obtain machine-checked proofs of its exact finite-dimensional statements. The published Kelly–Yudovina definition KellyStochasticNetworks.dualObjective already represents the dual formula, and its proved optimum-conditions theorem supplies one direction of the correspondence. The remaining development would give reusable facts about separable entropy objectives, nonnegative linear capacity constraints, complementary slackness, and exponential coordinate changes. Those facts can support later loss-network formalizations without changing this mission's target.

Difficulty

The boundary $x_r=0$ requires care: the objective has a continuous value there, but its logarithmic derivative does not. Thus a calculation that differentiates the objective throughout the closed nonnegative cone does not justify the printed differentiability sentence on p. 327. Dual existence is another boundary issue. A nonnegative capacity permits $C_j=0$, while the paper's stated growth of the dual objective in every nonnegative coordinate can fail at that input. Any formal argument for the complete theorem must cover these domains accurately. Full row rank controls uniqueness of the dual coordinates; without it, the paper explicitly allows nonunique blocking solutions. Kelly (1991), pp. 327–329.

Formalization scope

Lean represents links by Fin J, routes by Fin R, $A_{jr}$ and $C_j$ by natural numbers, and $x_r$, $y_j$, $B_j$, and $\nu_r$ by real numbers. The primal feasible set includes both coordinatewise nonnegativity and every link-capacity inequality. The dual optimum is minimal over the nonnegative orthant, using the published dual objective. The finite sums and products have their usual empty-index values; no hidden nonemptiness assumption is imposed. Matrix rank is taken over the reals and compared with $J$, so the rank condition is full row rank.

The goal assumes $\nu_r>0$ and $C_j\ge1$ for every route and link. Positive rates give the logarithm in the primal objective its intended meaning. Positive capacities exclude a degeneracy in the dual-attainment and blocking parts of the theorem. The value at $x_r=0$ is the continuous extension $x_r\log x_r=0$; no differentiability assertion at that boundary is part of the formal target. Blocking values belong to $[0,1)$, so the inverse logarithm is evaluated on a positive number. A flow optimum always ranges over the exact primal feasible set, and a blocking solution always ranges over the full conditions (2.7); neither can be replaced by an arbitrary vector with a convenient equation.

A complete proof may require finite-dimensional convex analysis, strict concavity of the entropy term, attainment on a closed feasible set, the dual first-order condition, and facts about exponentials, logarithms, products, and matrix rank. The definitions and theorems are kept separate so work on these pieces can be reused. Contributions proving either a milestone or a reusable supporting lemma are in scope.

Selected references

• F. P. Kelly, Loss networks, The Annals of Applied Probability 1(3), 319–378, 1991. DOI: 10.1214/aoap/1177005872.

Motivation

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.

Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.

A short history of the model:

• Kanet (1981) minimized total absolute deviation from a common due date that is large enough not to constrain the schedule, by a sorting rule. The special case in the middle of §2.1 is the midtime version of this problem.
• Garey, Tarjan and Wilfong (1988) proved the problem with arbitrary preferred times NP-complete (THEOREM 1, this mission), and gave an $O(N\log N)$ algorithm for a fixed task order.
• Hall, Kubiak and Sethi (1991) proved that the common-due-date problem becomes NP-hard when the due date is restrictive. The reduction of THEOREM 1 already uses a common preferred midtime that is not large, together with one extra task that pins the right end.

Setting

There are $N$ tasks $T_1,\dots,T_N$. Task $T_i$ has a length $l_i$ and a preferred midtime $M_i$. A schedule $S$ assigns every task a starting time $s_i\ge0$ such that no two tasks overlap on the single processor: for $i\ne j$, either $s_i+l_i\le s_j$ or $s_j+l_j\le s_i$. Idle time is allowed. The actual midtime of $T_i$ is $m_i(S)=s_i+l_i/2$, and the total discrepancy of $S$ is

$$\mathrm{cost}(S)=\sum_{i=1}^N |m_i(S)-M_i| .$$

The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times $a_i$ are interchangeable through $a_i=M_i-l_i/2$.

Total discrepancy (the decision problem). Given $N,k\in\mathbb Z^+$ and $M_i,l_i\in\mathbb Z^+$, is there a schedule with $\mathrm{cost}(S)\le k$?

Even-odd partition. Given positive integers $x_1<x_2<\dots<x_{2n}$, can they be split into two sets of equal sum so that each set contains exactly one of $x_{2i-1},x_{2i}$ for every $i$?

The special case. For tasks $T_0,\dots,T_{2n}$ with $0<l_0<l_1<\dots<l_{2n}$ and one common preferred midtime $M>\sum_i l_i$, write $A(S)=\{T_i: m_i(S)<M\}$ and $B(S)=\{T_i:m_i(S)>M\}$. A schedule is ordered if, on each side of $M$, shorter tasks lie nearer to $M$. The bracket $[A_n,\dots,A_1,T_0@M,B_1,\dots,B_n]$ is the schedule that puts $T_0$ at midtime $M$ and packs the listed tasks against it in the listed order.

Formalization targets

Goal: THEOREM 1

$$\text{Partition is NP-complete}\ \Longrightarrow\ \text{Total discrepancy is NP-complete.}$$

The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.

Milestones, in attack order

1. Even-odd partition is in NP; the instance $x_1=1$, $x_{2i}=x_{2i-1}+y_i$, $x_{2i+1}=x_{2i}+1$ built from a Partition instance $Y$ is a yes-instance if and only if $Y$ is; and LEMMA 1, even-odd partition is NP-complete.
2. The special case: a minimum cost schedule has no gaps and is ordered; LEMMA 2 (some $m_i(S)=M$), LEMMA 3 ($|A(S)|=|B(S)|$), LEMMA 4 ($m_0(S)=M$), LEMMA 5 (swapping $A_i$ and $B_i$ in a bracket keeps the cost), LEMMA 6 ($\{A_i,B_i\}=\{T_{2i},T_{2i-1}\}$ in a minimum cost bracket), and the minimum cost

$$k=\sum_{i=1}^n(l_{2i}+l_{2i-1})\left(n-i+\tfrac12\right)+l_0\,n .$$

3. At the midtime $M=\frac12\sum_{i=0}^{2n}l_i$ used in the reduction, every schedule of $T_0,\dots,T_{2n}$ costs at least $k$; equality forces the ordered, gap-free form in item 2.
4. The reduction: the instance D with $l_0=x_1-1$, $l_i=x_i$, $l_{2n+1}=2$, $M_j=M=\sum_{i\le 2n}l_i/2$, $M_{2n+1}=2M+1$ has a schedule of cost at most $k$ if and only if $X$ has an even-odd partition. Total discrepancy is in NP.

Significance

THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at $M$, the $i$-th pair of lengths in the $i$-th positions on either side, either member on either side. This characterization holds independently of the reduction.

The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with $M=\sum_i l_i/2$, so they must be restated for every $M$. Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.

Difficulty

The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint $s_i\ge0$ never binds. In D the midtime is $M=\sum_{i=0}^{2n}l_i/2$, exactly half the total length, and the reduction works because the constraint binds. The tasks before $M$ must fit in $[0,M-l_0/2]$, and the extra task $T_{2n+1}$ must sit at $[2M,2M+2]$. Together these force the two sides to have equal total length. A proof that only cites the large-$M$ lemmas proves nothing about D. Conversely, dropping $s_i\ge 0$ makes the reduction false: put the shorter element of every pair after $M$.

The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of $X$, double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.

Formalization scope

• Everything is real-valued except the instance codes. Schedules have real starting times $s_i\ge0$, and integer data are cast to $\mathbb R$. Restricting to integer starting times would be a different problem and is not what is stated.
• Nonnegative starting times are a standing assumption. The paper uses them ("scheduled between 0 and $M-l_0/2$", p. 336) without writing them into the model. Nonoverlap is "one task finishes before the other starts", the reading of "intersect only at their endpoints".
• Tasks are indexed by Fin N from $0$. In the special case $T_i$ is index $i$, and the paper's $T_{2i-1},T_{2i}$ ($1\le i\le n$) are the indices $2k+1,2k+2$ for $k=i-1$.
• Languages use the published CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.
• The goal is not the combinatorial equivalence of milestone 4. It states NP-completeness, so it contains the polynomial-time computation of the reduction and membership in NP. Taking NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.
• Running times of the algorithms of §2.2–§2.4 are out of scope for this mission, as are all results after §2.1.

Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.

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.
• J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28(4):643–651, 1981. https://doi.org/10.1002/nav.3800280411
• N. G. Hall, W. Kubiak, S. P. Sethi, Earliness–tardiness scheduling problems, II: Deviation of completion times about a restrictive common due date, Operations Research 39(5):847–856, 1991. https://doi.org/10.1287/opre.39.5.847
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Why the timing of a markdown matters

A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.

The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.

Prices, demand, and admissible switches

Let $n\ge1$ be the initial stock and $t\ge0$ the time to go. The seller first charges price $p_1$ and may change once to a lower price $p_2$. Demands at the two prices are independent Poisson counts with positive rates $\lambda_1$ and $\lambda_2$. A lower price produces more arrivals, so $p_2<p_1$ and $\lambda_1<\lambda_2$. Feng and Gallego also assume that lowering the price increases the revenue rate: $p_1\lambda_1<p_2\lambda_2$. There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.

Write $N_1(s)$ for the observed sales count at the initial price by time $s$. If the price changes at deterministic time $s\in[0,t]$, let $J(n,t;s)$ be the expected total revenue. The count after the change is independent of $N_1(s)$, and their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$. The optimal value $J(n,t)$ allows the switch time $\tau$ to depend on the counts observed so far. An admissible $\tau$ lies between zero and $t$, is a stopping time for the history of $N_1$, and occurs before stock is exhausted almost surely. At $s=0$, $J(n,t;0)$ is the revenue from charging $p_2$ immediately. The paper defines these quantities in §3, pp. 1377–1379.

Formalization targets

The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence $x_1<x_2<\cdots$ of inventory-dependent thresholds. When $t\le x_n$, switching immediately earns the optimal value; when $t>x_n$, a correction $F(n,t)$ is added:

$$J(n,t)=\begin{cases} J(n,t;0),&t\le x_n,\\ J(n,t;0)+F(n,t),&t>x_n. \end{cases}$$

The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with $F(0,t)=0$. For $n\ge1$, set $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$, where $G$ is the Poisson-tail expression from §4.1. The threshold $x_n$ is the first nonnegative zero of $L(n,\cdot)$. A function $H(n,\cdot)$ satisfies $\partial_tH=-\lambda_1H+L$ for positive time and $H(n,x_n)=0$; $F$ is zero below $x_n$ and equals $H$ at and above it. If $y_n$ is the first zero of $G(n,\cdot)$, the theorem also gives $x_1=y_1$ and $x_n<y_n$ for $n>1$.

Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of $G$ in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.

What the result provides

The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.

The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.

Where the mathematics is difficult

The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory $n$ depends on the correction at stock $n-1$. Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of $G$, the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.

The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.

Formalization scope

Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.

The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.

For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.

Selected references

• Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

Motivation

A Markov decision process with finitely many states and decisions, a discount factor $\beta\in(0,1)$ and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).

The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its $t$-th arc with weight $\beta^t$. The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.

Setting

A deterministic stationary Markov decision process consists of a finite set $S$ of $n$ states, an initial state $s_0\in S$, and for each state $s$ a finite nonempty set $D_s$ of decisions. Decision $i\in D_s$ costs $c(s,i)\in\mathbb R$ and leads with certainty to the state $\mathrm{next}(s,i)$. Equivalently, it is a directed graph on $S$ with an arc $s\to\mathrm{next}(s,i)$ of weight $c(s,i)$ for each decision; parallel arcs and loops are allowed.

A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state $s$ and time $t=0,1,2,\dots$; it is stationary if $\delta(s,t)$ does not depend on $t$. From $s_0$ it produces the states $s_{t+1}=\mathrm{next}(s_t,\delta(s_t,t))$ and the discounted cost

$$J_\beta(\delta)=\sum_{t=0}^{\infty}\beta^t c\bigl(s_t,\delta(s_t,t)\bigr).$$

The optimal discounted cost is $J^*_\beta(s_0)=\inf_\delta J_\beta(\delta)$, the infimum over all policies $\delta(s,t)$.

A sigma is a walk $w_0=s_0,w_1,\dots,w_N$ along decisions $e_t\in D_{w_t}$ whose nodes $w_0,\dots,w_{N-1}$ are distinct and whose last node repeats an earlier one, $w_N=w_j$ with $j<N$: the walk from $s_0$ up to the first repetition of a node. It is a prefix of $j$ arcs followed by a cycle of $l=N-j\ge1$ arcs. Its discounted cost $c_\beta(P)$ is the discounted cost of the infinite walk that follows it and repeats its cycle forever.

In the min-plus semiring (addition is $\min$, multiplication is $+$, zero is $+\infty$), let $A_{uv}$ be the least cost of a decision from $u$ to $v$ ($+\infty$ if none), let $rA$ multiply every finite entry by $r$, and let

$$B_0=I,\qquad B_k=A\otimes\beta A\otimes\cdots\otimes\beta^{k-1}A ,$$

with $I$ the min-plus identity. The entry $(B_k)_{uv}$ is the least discounted cost $\sum_{t<k}\beta^t c_t$ of a $k$-arc walk from $u$ to $v$.

Formalization targets

Goal

For $0<\beta<1$,

$$J^*_\beta(s_0)=\min_{P\text{ sigma}}c_\beta(P)=\min\Bigl\{(B_k)_{s_0u}+\frac{\beta^{k}(B_l)_{uu}}{1-\beta^{l}}\;:\;u\in S,\ 0\le k\le n,\ 1\le l\le n,\ \text{both entries finite}\Bigr\},$$

with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).

Milestones

1. The closed form of the cost of a sigma (p. 446): $c_\beta(P)=\sum_{t<j}\beta^tc_t+\frac{\beta^j}{1-\beta^l}\sum_{t<l}\beta^tc_{j+t}$.
2. A stationary optimal policy exists (§2, p. 444; cited on p. 446). The general finite stochastic statement is on the platform as BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.
3. The path of a stationary policy, cut at its first repeated node, is a sigma with the same discounted cost, and every sigma arises this way (p. 446).
4. The products $B_j$ are the cheapest discounted $j$-arc walks (p. 447).

Significance

The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each $B_k$ is a product of $k$ min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).

On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.

Difficulty

The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies $\delta(s,t)$, and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary $k$-arc walks and closed $l$-walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has $k\le n$ and $l\le n$. Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of $\beta$ in two places.

Formalization scope

The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:

• The model is stationary and deterministic. A DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set $D_s$"; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.
• Policies are maps $\delta(s,t)$, time is $\mathbb N$ from $0$, and the optimum optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.
• Costs are tsums, which are junk ($0$) for non-summable series; every statement that sums costs assumes $0<\beta<1$, under which the series converge absolutely.
• A sigma is encoded as a lasso, $w_N=w_j$ with $j<N$. This includes $j=0$, a sigma whose cycle passes through $s_0$, which the printed form $(u_0,\dots,u_k,v_1,\dots,v_l,v_1)$ omits but the definition "a path from $u_0$ until the first repetition of a node" includes. The paper's $k$ is $j-1$.
• Corrected slips: (i) in the sigma display the cycle sum carries $\beta^{j-1}$, not $\beta^j$, for its $j$-th arc, and the indices are made consistent; (ii) the algorithm's expression is $\lambda+\beta^k\mu/(1-\beta^l)$ with $l\ge1$, not $\lambda+\beta^{k+1}\mu/(1+\beta^l)$ (one state with a loop of cost $1$ has optimum $1/(1-\beta)$, which the printed form misses); (iii) $B_0$, used but not defined, is the min-plus identity.
• Matrix entries are in Tropical (WithTop ℝ), so $+\infty$ is ⊤ and the product is Mathlib's matrix product over the tropical semiring.

Not formalized: membership in NC, the processor count $n^4$, the $\log^2 n+3\log n$ parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.

Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. https://doi.org/10.1287/moor.12.3.441
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, §7.3 (discounted problems, Proposition 7.3.1).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Ch. 6 (existence of stationary optimal policies for discounted models). https://doi.org/10.1002/9780470316887

Motivation

Scheduling jobs on parallel machines under precedence constraints is the core model of project and parallel-processing scheduling: a job may start only after its predecessors have finished. Two criteria dominate the literature, the makespan $C_{\max}$ (when does the last job finish?) and the total completion time $\sum_j C_j$ (how long do jobs wait on average?). Knowing that one criterion is at least as hard as the other lets a hardness proof for one transfer to the other without a new reduction from a combinatorial problem.

Brucker, Lenstra and Rinnooy Kan's report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; later in Annals of Discrete Mathematics 1, 1977) collected the complexity status of the standard scheduling problems and stated a set of elementary reductions among them as Theorem 1. Part (l) reduces makespan to total completion time for identical machines with precedence constraints and bounded processing times.

Timeline.

• 1971–1972: Cook (doi:10.1145/800157.805047) and Karp (doi:10.1007/978-1-4684-2001-2_9) introduce NP-completeness and polynomial reducibility.
• 1975: Ullman (doi:10.1016/S0022-0000(75)80008-0) proves that the makespan problems $n|2|I,\mathit{prec},1\le p_{j1}\le 2|C_{\max}$ and $n|m|I,\mathit{prec},p_{j1}=1|C_{\max}$ are NP-complete, by reductions from 3-SATISFIABILITY.
• 1975: Brucker, Lenstra and Rinnooy Kan state Theorem 1(l); their Table III (p. 13) applies it to Ullman's two problems and concludes that the corresponding total completion time problems are NP-complete.

Setting

An instance has $n$ jobs $J_1,\dots,J_n$, a number $m \ge 1$ of identical machines, a processing time $p_j$ for each job, and a precedence relation $<$ on the jobs: $J_j < J_k$ means that $J_k$ may start only after $J_j$ has completed. Each job is one operation, processed without interruption on any one machine. For a constant $p_*$, the class $n|m|I,\mathit{prec},1\le p_{j1}\le p_*$ requires $1 \le p_j \le p_*$ for every job and an acyclic precedence relation.

A schedule assigns to every job a machine and a starting time $B_j \in \mathbb N$; the completion time is $C_j = B_j + p_j$. It is feasible if two jobs on the same machine never overlap and $J_j < J_k$ implies $C_j \le B_k$.

Following the paper, each optimization problem is replaced by its recognition version. Problem $P'$ asks, for an instance and a threshold $y'$, whether some feasible schedule has $C_{\max} = \max_j C_j \le y'$. Problem $P$ asks, for an instance of the same class and a threshold $y$, whether some feasible schedule has $\sum_j C_j \le y$ (all weights $w_j = 1$).

$P'$ is reducible to $P$, written $P' \propto P$, if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 1(l)

For every constant $p_* \ge 1$,

$$n'|m|I,\mathit{prec},1\le p_{j1}\le p_*|C_{\max} \;\propto\; n|m|I,\mathit{prec},1\le p_{j1}\le p_*,w_j=1|\textstyle\sum w_jC_j .$$

Milestones

1. A trivial upper bound. Every instance of $P'$ with $n'$ jobs has a feasible schedule with $C_{\max} \le n'p_*$.
2. The construction and the forward direction. For $0 \le y' \le n'p_*$ let $n'' = (n'-1)y'$, $n = n'+n''$ and $y = ny' + \tfrac12 n''(n''+1)$, and add $n''$ unit-time jobs $J_{n'+k}$, each required to follow every original job and every earlier added job. If $P'$ has a schedule with $C_{\max} \le y'$, the new instance has a feasible schedule with $\sum_j C_j \le y$.
3. The backward direction. If every feasible schedule of $P'$ has $C_{\max} > y'$, every feasible schedule of the new instance has $\sum_j C_j > y$.

Significance

The result. Theorem 1(l) makes the total completion time problem at least as hard as the makespan problem in the same class. Combined with Ullman's NP-completeness results and Theorem 1(b) (reducibility transfers NP-completeness), it shows that minimizing $\sum_j C_j$ on identical machines with precedence constraints is NP-complete, already for two machines with $p_j \in \{1, 2\}$ and for unit processing times on $m$ machines. These are two rows of the paper's Table III.

Formalizing it. The result is proved on one page of a typewritten report; no machine-checked version exists. The mission produces a scheduling model for identical machines with precedence constraints, binary languages for the two recognition problems, and the reduction in Cook's Turing-machine model. The proof's displayed bounds contain a misprinted index range, which the formal statements correct.

Difficulty

The two criteria are not monotonically related: a schedule with a smaller makespan can have a larger total completion time than one with a larger makespan. So the obvious reduction, keeping the instance and asking for $\sum_j C_j \le n'y'$, is not an equivalence: a no-instance of $P'$ can have a schedule with small total completion time. The instance has to be changed so that the total completion time is governed by the makespan, and the comparison of the two thresholds must be exact, including the strict inequality on the "no" side, which depends on integral completion times and positive processing times.

The main formal difficulty lies in the reduction itself. A polynomial-time Turing machine must decode the binary instance, check that it belongs to the class (including acyclicity of the precedence relation), compare $y'$ with $n'p_*$, and write out an instance with $n'' = (n'-1)y'$ additional jobs and a quadratic-size precedence matrix. The size of that output is polynomial only because $p_*$ is a constant: a version with $p_*$ part of the input would make $n''$ exponential in the input length.

Formalization scope

• Jobs and machines are indexed from $0$ (Fin n, Fin m). Starting times are natural numbers; Section 3 derives all times from processing orders on nonnegative integer data, and both criteria are regular. "$C_{\max} \le y$" is written as "$C_j \le y$ for every $j$".
• The precedence relation is a Boolean matrix. Its acyclicity and $m \ge 1$ are part of the problem class; the paper leaves both implicit, and the claim "any instance has a solution with $C_{\max} \le n'p_*$" fails without them.
• $p_*$ is a constant of the class and a parameter of both languages, not part of the input. All weights in the target problem equal $1$ and are not written.
• The threshold $y = ny' + \tfrac12 n''(n''+1)$ is stated in $\mathbb Q$ exactly as printed in the milestones; it is an integer, and the reduction uses its natural-number value.
• The paper's displayed bounds $n'y' + \sum_{k=n'+1}^{n}(y'+k) = y$ and $y' + \sum_{k=n'+1}^{n}(y'+1+k) = y$ have a misprinted index range (the sums must run over $k = 1,\dots,n''$). The milestones state the end-to-end bounds $\sum_j C_j \le y$ and $\sum_j C_j > y$.
• "$C_{\max} > y'$" in the backward direction is read as the negation of the forward hypothesis: no feasible schedule of $P'$ has $C_{\max} \le y'$.
• "Reducible" is Cook's polynomial-time many-one reducibility from the published definition CookPvsNP_defs; numbers are written in binary with the alphabet and code encNats of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). The unit-time model ResourceScheduling.Chain.Model (Błażewicz, Lenstra and Rinnooy Kan) has the same feasibility conditions but unit processing times and real start times, so the model here is defined anew.
• A trivializing formalization is ruled out: the goal asserts a polynomial-time computable map, not the bare equivalence, and codes of instances outside the class are excluded from both languages, so the reduction cannot exploit malformed inputs.
• Contributions welcome: proofs of the three milestones, a Turing-machine library for arithmetic on binary codes (reusable across this series), and a proof of the goal from the milestones.

Selected references

• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; published in Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
• J. D. Ullman, NP-complete scheduling problems, Journal of Computer and System Sciences 10 (1975) 384–393. doi:10.1016/S0022-0000(75)80008-0
• S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9

Motivation

In a no-wait flow shop every job passes through the machines $M_1,\dots,M_m$ in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of Hall and Sriskandarajah (doi:10.1287/opre.44.3.510). The question of how hard it is to schedule such a shop well is the question this mission formalizes.

Brucker, Lenstra and Rinnooy Kan settled it for the case in which the number of machines is part of the input. In their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977, doi:10.1016/S0167-5060(08)70743-X), Theorem 5 reduces DIRECTED HAMILTON PATH to the no-wait flow shop. Both minimizing the makespan $C_{\max}$ and minimizing the total completion time $\sum C_j$ are thereby NP-complete.

Timeline.

• 1964: Gilmore and Gomory solve the two-machine no-wait flow shop with makespan in polynomial time (doi:10.1287/opre.12.5.655).
• 1972: Wismer (doi:10.1287/opre.20.3.689) and Reddi and Ramamoorthy (doi:10.1057/jors.1972.52) show that no-wait makespan minimization is a travelling-salesman problem with arc weights computed from the processing times.
• 1972: Karp proves DIRECTED HAMILTON CIRCUIT NP-complete (doi:10.1007/978-1-4684-2001-2_9).
• 1975: Brucker, Lenstra and Rinnooy Kan reduce DIRECTED HAMILTON CIRCUIT to DIRECTED HAMILTON PATH (their Theorem 2(d)), and DIRECTED HAMILTON PATH to $n|m|F,\textit{no wait}|C_{\max}$ and to $n|m|F,\textit{no wait},w_j=1|\sum w_jC_j$ (Theorem 5).
• 1984: Röck shows that the problem stays NP-hard for three machines (doi:10.1145/62.65).

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines. Job $J_\ell$ needs processing time $p_{\ell i}\in\mathbb N$ on machine $M_i$. Write

$$q_{\ell i}=\sum_{r=1}^{i}p_{\ell r},\qquad q_{\ell 0}=0,$$

for the time job $J_\ell$ spends on its first $i$ machines. Because a job never waits, a schedule is determined by the start times $B_\ell\in\mathbb N$. The operation of $J_\ell$ on $M_i$ occupies $[B_\ell+q_{\ell,i-1},\,B_\ell+q_{\ell i})$, and job $J_\ell$ completes at $C_\ell=B_\ell+q_{\ell m}$. A schedule is feasible when no two distinct jobs occupy the same machine at the same time. The delay

$$c_{jk}=\max_{1\le i\le m}\{q_{ji}-q_{k,i-1}\}$$

is the least gap $B_k-B_j$ that lets $J_k$ follow $J_j$ on every machine.

A directed graph $G=(V,A)$ on $V=\{0,\dots,n-1\}$ has a Hamilton path if its vertices can be ordered $\sigma(0),\dots,\sigma(n-1)$ with every $(\sigma(i),\sigma(i+1))\in A$.

From $G$ the paper builds an instance with $n$ jobs and $m=n(n-1)+2$ machines. Each ordered pair $(j,k)$ of distinct jobs is assigned a middle machine $\iota(j,k)\in\{2,\dots,m-1\}$, and the partial sums $q_{\ell i}$ are perturbed from $i\mu$ by $\pm\lambda$ or $\pm(\lambda+1)$ on the machines $\iota(\ell,\cdot)$ and just before the machines $\iota(\cdot,\ell)$, depending on whether the pair is an arc. The parameters satisfy $\lambda\ge1$ and $\mu\ge2\lambda+3$.

Formalization targets

Goal (Theorem 5)

$$\text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait}|C_{\max}\quad\text{and}\quad \text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait},w_j=1|\textstyle\sum w_jC_j,$$

where $\propto$ is polynomial-time many-one reducibility between the binary-coded recognition languages.

Milestones, in the order the proof uses them

1. Eq. (9): $c_{jk}$ is the least gap between $B_j$ and $B_k$ for which $J_k$ follows $J_j$ on every machine.
2. The travelling-salesman reformulation: if all processing times are positive, a feasible schedule with $C_{\max}\le y$ (resp. $\sum C_\ell\le y$) exists iff some job order has path length (resp. summed completion times along the path) at most $y$.
3. An admissible ordering $\iota$ exists for every $n\ne2$.
4. All processing times of the construction are at least $1$.
5. The delays of the construction: $c_{jk}=\mu+2\lambda$ if $(j,k)\in A$, and $\mu+2\lambda+2$ otherwise.
6. Theorem 5(a), the equivalence: $G$ has a Hamilton path $\iff$ $C_{\max}\le(n-1)(\mu+2\lambda)+m\mu$.
7. Theorem 5(b), the equivalence: $G$ has a Hamilton path $\iff$ $\sum_jC_j\le\tfrac12n(n-1)(\mu+2\lambda)+nm\mu$.
8. Theorem 2(d), off the goal's path: $G'$ has a Hamilton circuit iff the graph obtained by splitting a vertex $v'$ into $v'$ and a new sink $v''$ has a Hamilton path.

Significance

The result. Theorem 5, together with the NP-completeness of DIRECTED HAMILTON PATH, places both no-wait criteria among the NP-complete problems once $m$ is part of the input. The Gilmore–Gomory algorithm for two machines therefore cannot be extended to arbitrary $m$ unless P = NP, and heuristics and exact exponential methods for no-wait shops are justified. The reduction also gives a structural fact of independent use: every directed graph can be realized, up to two arc-weight values, as the delay matrix of a no-wait flow shop.

Formalizing it. The result has been proved for fifty years; to our knowledge no machine-checked version exists. This mission produces a checked no-wait flow shop model, a checked travelling-salesman reformulation of it, the correctness of the paper's construction, and a polynomial-time reduction in an explicit Turing-machine model. It also records a gap in the printed proof: the ordering $\iota$ the paper calls easy to construct does not exist for $n=2$.

Difficulty

Three steps are not routine.

1. The passage from schedules to job orders assumes that the order in which jobs start is the order in which they visit every machine. With zero processing times this fails, so the reformulation needs the positivity milestone.
2. Computing the delays requires a case analysis over all machines and all pairs of perturbations. The property of $\iota$ is exactly what keeps the "$+$" and "$-$" cases from colliding, and the constants $\lambda\ge1$, $\mu\ge2\lambda+3$ are tight enough that the comparison must be done carefully.
3. The goal asks for an actual Turing machine with a polynomial step bound. It has to build $\iota$ for every $n\ne2$ and handle $n\le2$ separately. The equivalences alone do not give this.

Formalization scope

Jobs and machines are $0$-based (Fin n, Fin m); cum p ℓ i is the paper's $q_{\ell i}$, and the machine indices $\iota(j,k)$ are the paper's $1$-based indices. Start times are natural numbers, and release dates are $0$. Section 3 computes times from processing orders on integer data, and every criterion is regular, so real start times would not change the yes-instances. A zero-length operation occupies the empty interval. $C_{\max}\le y$ is stated as $C_\ell\le y$ for every job. The delays, the partial sums of the construction and its processing times are computed in $\mathbb Z$. The instance uses their conversion to $\mathbb N$, which is exact by milestone 4. The threshold of Theorem 5(b) is compared in $\mathbb Q$, as printed.

The paper's loose phrases are made explicit as follows:

• "scheduled directly after" means "precedes on every machine";
• "equivalent to solving the TRAVELLING SALESMAN problem" means the two threshold equivalences of milestone 2, with the $\sum C_j$ version as the reading of "constructed as in (a)";
• "such an ordering can easily be constructed" is stated for $n\ne2$, the only case in which it is true.

Directed graphs are Boolean adjacency matrices. A graph with $0$ or $1$ vertices has a Hamilton path, and a one-vertex graph has a Hamilton circuit iff it has a loop.

The goal is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs, with polynomial time measured on Cook's one-tape Turing machines. Instances are coded with the alphabet BSym and binary code encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). A graph is coded as $n$ followed by its adjacency matrix; a flow-shop instance as $n$, $m$, the matrix $(p_{\ell i})$ and the threshold $y$.

Stating only the equivalences 6–7 and calling the result "reducible" would drop polynomiality; the goal therefore asserts PolyReducible. The target languages contain exactly the no-wait flow-shop instances, with no waiting allowed, so the reduction cannot land in a looser problem. The parameters $\lambda,\mu$ always carry $\lambda\ge1$, $\mu\ge2\lambda+3$.

Contributions are welcome at every level:

• the general travelling-salesman reformulation, which is reusable for any no-wait flow-shop result;
• the combinatorial existence of $\iota$;
• the arithmetic of the construction;
• Turing-machine infrastructure for computing arithmetic list transformations in polynomial time, which every reduction in this series needs.

Selected references

• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9
• P. C. Gilmore, R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12 (1964) 655–679. doi:10.1287/opre.12.5.655
• D. A. Wismer, Solution of the flowshop-scheduling problem with no intermediate queues, Operations Research 20 (1972) 689–697. doi:10.1287/opre.20.3.689
• S. S. Reddi, C. V. Ramamoorthy, On the flow-shop sequencing problem with no wait in process, Operational Research Quarterly 23 (1972) 323–331. doi:10.1057/jors.1972.52
• H. Röck, The three-machine no-wait flow shop is NP-complete, Journal of the ACM 31 (1984) 336–345. doi:10.1145/62.65
• N. G. Hall, C. Sriskandarajah, A survey of machine scheduling problems with blocking and no-wait in process, Operations Research 44 (1996) 510–525. doi:10.1287/opre.44.3.510
• S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047

Motivation

Minimizing total weighted tardiness on a single machine, written $n|1||\sum w_jT_j$, is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference problem for branch-and-bound methods and dominance rules throughout the 1960s and 1970s.

Close relatives are easy: with equal weights and a common due date, shortest-processing-time order is optimal. Whether the weighted problem admits a polynomial algorithm was open until the report of Brucker, Lenstra and Rinnooy Kan in 1975. Their Theorem 4(d) shows that KNAPSACK reduces to it, so the problem is NP-hard. The unweighted case $n|1||\sum T_j$ is listed there as open (Section 5) and was settled only later by Du and Leung (1990).

Timeline:

• 1972: Karp proves KNAPSACK NP-complete (Karp 1972).
• 1975: Brucker, Lenstra and Rinnooy Kan, Mathematisch Centrum Report BW 43/75, Theorem 4(d), reduce KNAPSACK to $n|1||\sum w_jT_j$ (journal version: Annals of Discrete Mathematics 1, 1977).
• 1977: Lawler gives a pseudopolynomial algorithm for $n|1||\sum T_j$ and shows that $n|1||\sum w_jT_j$ is strongly NP-hard (Lawler 1977).
• 1990: Du and Leung prove $n|1||\sum T_j$ NP-hard (Du & Leung 1990).

Setting

A KNAPSACK instance consists of positive integers $a_1,\dots,a_t$ and $b$. It is a yes-instance if some subset $S\subseteq T=\{1,\dots,t\}$ satisfies $\sum_{j\in S}a_j=b$. Write $A=\sum_{j\in T}a_j$ and $a_*=\max_{j\in T}a_j$.

An instance of $n|1||\sum w_jT_j$ consists of $n$ jobs. Job $j$ has a processing time $p_j$, a weight $w_j$ and a due date $d_j$, all nonnegative integers, and every job is available at time $0$. A schedule gives each job a start time $B_j\in\mathbb N$, and no two jobs may overlap on the machine. Job $j$ completes at $C_j=B_j+p_j$ and has tardiness $T_j=\max\{0,C_j-d_j\}$. The instance with threshold $y$ is a yes-instance if some schedule satisfies $\sum_jw_jT_j\le y$. A processing order $\pi=(\pi(1),\dots,\pi(n))$ determines the schedule without idle time, in which $C_{\pi(k)}=\sum_{i\le k}p_{\pi(i)}$.

Reducibility (Section 2 of the paper) is polynomial-time many-one reducibility between the recognition versions. A polynomial-time Turing machine must map codes of KNAPSACK instances to codes of scheduling instances so that yes-instances map exactly to yes-instances.

The paper's construction has $n=t+t'$ jobs: for $j\in T$, $p_j=\tau+a_j$, $w_j=\tau+a_j+1$, $d_j=t\tau+b$; for each of the $t'$ dummy jobs, $p_j=\tau$, $w_j=\tau+1$, $d_j=t\tau+b$. The threshold is $y=\tfrac12t'(t'+1)\tau(\tau+1)+(t'+1)\tau(A-b)+t'$, with $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ and $\tau>2t'+A$. The proof is phrased in terms of $c_\pi=C_{\pi(t)}-(t\tau+b)$, the amount by which the $t$-th job of the order misses the common due date.

Formalization targets

Goal: Theorem 4(d)

$$\text{KNAPSACK}\;\propto\;n|1||\textstyle\sum w_jT_j,$$

stated as CookPvsNP.PolyReducible SchedComplexity.OneMachine.knapsackLang wtLangMult. The scheduling side uses the multiplicity encoding of the paper's Remark (p. 23), in which a class of identical jobs is written once together with its cardinality.

The equivalence and its claims

Each milestone is a statement of the paper's proof (pp. 20–21) about the construction above, for every admissible $\tau$:

• removal of idle time: every schedule is matched or improved by the schedule without idle time of some processing order;
• KNAPSACK has a solution iff some order has $C_{\pi(t)}=t\tau+b$; moreover $-b\le c_\pi\le A-b$;
• identities and bounds (2)–(7) for the tail sums $\sum_{j>t}v_{\pi(j)}(C_{\pi(j)}-C_{\pi(t)})$;
• claims (A) $c_\pi=0\Rightarrow\exists\pi'$ with $c_{\pi'}=0$ and $\sum w_jT_j\le y$; (B) $c_\pi>0\Rightarrow\sum w_jT_j>y$; (C) $c_\pi<0\Rightarrow\sum w_jT_j>y$;
• the equivalence: KNAPSACK has a solution iff the constructed instance has a schedule with $\sum w_jT_j\le y$.

Significance

The theorem places $n|1||\sum w_jT_j$ among the NP-hard problems, so (unless P = NP) the research on it has to aim at enumerative methods, pseudopolynomial algorithms or approximation, not at an exact polynomial algorithm. Together with the companion reductions of Theorem 4, it drew the boundary between easy and hard single-machine problems that the later classification of Lageweg, Lawler, Lenstra and Rinnooy Kan made systematic.

The result is proved in the paper, and Lawler's later strong NP-hardness proof supersedes it. No machine-checked proof is known to exist. A formal proof adds three things. It makes the paper's "it is easily seen" steps and the encoding argument of the Remark explicit. It produces a reusable single-machine tardiness model with processing orders. It also fixes a gap in the printed construction: the printed $t'$ need not be an integer.

Difficulty

The equivalence is not a local exchange argument. The threshold $y$ must separate orders with $c_\pi=0$ from all others, and the objective is a quadratic function of the order. The orders with $c_\pi=0$ can still differ in $\sum w_jT_j$ by the cross terms $\sum a_{\pi(j)}a_{\pi(k)}$ and by how the late jobs are arranged. The construction therefore needs a slack $t'$ that absorbs these terms, and a scale $\tau$ large enough that a nonzero $c_\pi$ always costs more than the slack. Keeping exact track of every constant, including $t'$ and $y$, is where errors creep in.

Polynomiality is a second, separate difficulty. The construction has $\Theta(t^2a_*^2+tA)$ jobs, which is exponential in the binary length of the KNAPSACK input. The goal holds only for the encoding of the Remark, and a solver must also produce an explicit polynomial-time Turing machine.

Formalization scope

• Jobs of the order-based statements are Fin n, numbered from $0$; a processing order is Equiv.Perm (Fin n) with π i the paper's $\pi(i+1)$. posCompletion p π k is the paper's $C_{\pi(k)}$ for the 1-based position $k$.
• Start times are in $\mathbb N$. Every criterion is regular and the paper determines schedules by processing orders, so integer start times lose nothing. Tardiness and $\sum w_jT_j$ are computed in $\mathbb Z$; the bounds with halves are stated over $\mathbb R$ exactly as printed.
• Corrected gap: the printed $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ is a half-integer when $(t+1)(A-b)$ is odd. The formalization uses its ceiling and computes $y$ from the same $t'$.
• $\tau$ is quantified over all integers with $\tau>2t'+A$; the positivity of the $a_j$ and $0<b<A$ are hypotheses, as the paper assumes them.
• Explicit readings of the paper's loose phrases: "we may assume [no idle time]" becomes a theorem that the schedule without idle time of some order is at least as good as any schedule; "easily seen" becomes the equivalence with $C_{\pi(t)}=t\tau+b$; "for some $\pi$" in (5) and (7) becomes a reordering that keeps the first $t$ positions, and so keeps $c_\pi$; "we may assume $0<b<A$" is a hypothesis of the milestones but not of the goal, whose reduction must handle every KNAPSACK instance.
• Reducibility is CookPvsNP.PolyReducible from the published CookPvsNP_defs. Codes use the alphabet BSym and the binary numerals encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). KNAPSACK is restricted to positive integers, so that encoding's subsetSumLang is not reused.
• The goal must not be weakened to the bare equivalence: polynomial-time computability of the reduction is part of the statement. The one-copy-per-job encoding of the target is ruled out: the paper does not claim polynomiality for it, and the goal uses the multiplicity encoding instead.
• Welcome contributions: proofs of the claims, a reusable lemma that idle time can be removed for regular criteria, and Turing-machine constructions for arithmetic on binary numerals, which the sibling missions of this series also need.

Selected references

• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://ir.cwi.nl/pub/9725 , https://doi.org/10.1016/S0167-5060(08)70743-X
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• E. L. Lawler, A "pseudopolynomial" algorithm for sequencing jobs to minimize total tardiness, Annals of Discrete Mathematics 1 (1977) 331–342. https://doi.org/10.1016/S0167-5060(08)70742-8
• J. Du, J. Y.-T. Leung, Minimizing total tardiness on one machine is NP-hard, Mathematics of Operations Research 15 (1990) 483–495. https://doi.org/10.1287/moor.15.3.483
• S. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling problems. Their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, Report BW 43/75, 1975; journal version in Annals of Discrete Mathematics 1, 1977) introduced the four-field notation $n|m|\ell,\lambda|k$ that, in refined form, is still the standard classification of scheduling problems, and proved NP-completeness of the "easiest" hard problems by explicit reductions.

Single-machine problems with due dates sit right at that boundary. Minimizing the maximum lateness $L_{\max}$ is solved by Jackson's earliest-due-date rule (1955), and minimizing the number of late jobs by Moore's algorithm (1968). Theorem 4 of the report shows that small changes to these problems — one release date, job weights, or due dates turned into deadlines under a weighted completion-time objective — make them NP-complete, by reduction from KNAPSACK. This mission formalizes four of those reductions, parts (b), (c), (e) and (f) of Theorem 4.

Timeline, as far as this mission is concerned:

• 1955: Jackson — $n|1||L_{\max}$ is solved by sequencing in order of nondecreasing due dates.
• 1968: Moore — $n|1||\sum U_j$ (unit weights, no release dates) is solvable in polynomial time.
• 1972: Karp — KNAPSACK (in the subset-sum form used here) is NP-complete; Karp also notes the reduction to $n|1||\sum w_jU_j$, which the report cites for part (e).
• 1975: Brucker, Lenstra and Rinnooy Kan — Theorem 4: KNAPSACK reduces to ten scheduling problems, including the four single-machine problems of this mission.

Setting

A single-machine instance consists of $n\ge1$ jobs $J_1,\dots,J_n$. Job $J_j$ needs $p_{j1}$ units of processing on the machine $M_1$, has a weight $w_j$, a release date $r_j$ and a due date $d_j$; all data are nonnegative integers. A schedule assigns to each job a starting time $B_j\ge r_j$ such that the occupied intervals $[B_j,B_j+p_{j1})$ of distinct jobs are disjoint. Idle time is allowed; a job with $p_{j1}=0$ occupies an empty interval. The completion time is $C_j=B_j+p_{j1}$, the lateness is $L_j=C_j-d_j$ (possibly negative), and $U_j$ is $0$ if $C_j\le d_j$ and $1$ otherwise. The criteria are

$$L_{\max}=\max_j L_j,\qquad \sum w_jC_j=\sum_{j=1}^n w_jC_j,\qquad \sum w_jU_j=\sum_{j=1}^n w_jU_j .$$

The problem class is written in the $\lambda$ field: by default every $r_j=0$; $r_n\ge0$ allows a nonzero release date for the last job $J_n$ only; $w_j=1$ fixes unit weights; $L_{\max}\le0$ admits only schedules that meet every due date. A problem is turned into a yes/no question by asking whether a schedule with value $\le y$ exists.

KNAPSACK (Theorem 2(b) of the report): given positive integers $a_1,\dots,a_t,b$, is there a subset $S\subseteq T=\{1,\dots,t\}$ with $\sum_{j\in S}a_j=b$? Write $A=\sum_{j\in T}a_j$.

A problem $P'$ is reducible to $P$, $P'\propto P$, if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ whose answer is the same.

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

$$\mathsf{KNAPSACK}\propto n|1|L_{\max}\le0|\textstyle\sum w_jC_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0|L_{\max},$$ $$\mathsf{KNAPSACK}\propto n|1||\textstyle\sum w_jU_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0,w_j=1|\textstyle\sum w_jU_j ,$$

as polynomial-time many-one reductions between languages of binary strings.

Milestones: the four yes-instance equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A$, and the paper's constructions:

• 4(c): $n=t+1$; $r_j=0$, $p_{j1}=a_j$, $d_j=A+1$ for $j\in T$; $r_n=b$, $p_{n1}=1$, $d_n=b+1$. KNAPSACK has a solution iff some schedule has $L_{\max}\le0$.
• 4(f): the same instance with unit weights; KNAPSACK has a solution iff some schedule has $\sum U_j\le0$.
• 4(e): $n=t$; $p_{j1}=w_j=a_j$, $d_j=b$. KNAPSACK has a solution iff some schedule has $\sum w_jU_j\le A-b$.
• 4(b): $n=t+1$; $p_{j1}=w_j=a_j$, $d_j=A+1$ for $j\in T$; $p_{n1}=1$, $w_n=0$, $d_n=b+1$. KNAPSACK has a solution iff some schedule meeting all due dates has

$$\sum w_jC_j\le y=\sum_{j,k\in T,\ j\le k}a_ja_k+A-b .$$

Significance

The result. Combined with the NP-completeness of KNAPSACK, the four reductions show that the four problems are NP-hard (in the ordinary sense; they admit pseudo-polynomial algorithms). Part (c) shows that Jackson's rule cannot be extended to a single nonzero release date unless P = NP; part (f) does the same for Moore's algorithm; part (e) explains why weights are essential in the late-jobs problem; part (b) shows that deadlines turn the weighted completion-time problem, solved by Smith's ratio rule without them, into a hard one. These are entries of the complexity tables that every later scheduling classification builds on.

Formalizing it. The reductions are classical and proved on paper, in a few lines each: for (c), (e) and (f) the report gives only the construction and a figure. None of them has a machine-checked proof. A complete formalization supplies the explicit equivalence over all feasible schedules (including schedules with idle time and arbitrary processing order), the handling of the inputs the proof sets aside by "we may assume that $0<b<A$", and the polynomial-time computability of the constructions in a Turing-machine model.

Difficulty

Each equivalence has an easy direction: a subset $S$ with sum $b$ gives the schedule "jobs of $S$, then $J_n$, then the rest" (Figures 4 and 7 of the report). The other direction must rule out every feasible schedule, not only the idle-free ones in the displayed order. The report gives no argument for this direction in (c), (e) and (f), and for (b) only a computation for idle-free schedules of one shape. The equivalences are false outside $0<b<A$ in some cases (for (c), any $b>A$ makes every schedule on time), so the goal's reduction must treat those inputs separately.

The heavier part is polynomial-time computability: the reduction must be a function on strings, computed by a one-tape Turing machine within a polynomial number of steps, that parses a binary-coded KNAPSACK instance, computes $A$ and the threshold (for (b), a sum of $O(t^2)$ products), and writes the coded scheduling instance — and maps malformed strings outside the target language.

Formalization scope

• Model. Jobs are Fin n (0-based; $J_n$ is the last index), with $n>0$ in each target language. Starting times are natural numbers: Section 3 computes them from processing orders on integer data, and since all criteria here are regular and release dates survive left shifts, real starting times give the same yes-instances. Feasibility requires disjoint occupied intervals, including empty intervals when $p_{j1}=0$. Idle time is allowed. Lateness is an integer.
• Problem classes are binding. $r_n\ge0$ means at least one job and release date $0$ for every job except the last; $L_{\max}\le0$ in (b) is a constraint on schedules, not the criterion. Instances outside the class are not in the target language.
• Thresholds. $y\in\mathbb N$ in all four languages; for $L_{\max}$ this restricts to nonnegative thresholds, enough for the paper's $y=0$. "$L_{\max}\le y$" is stated as "$L_j\le y$ for all $j$".
• Codes. An instance with threshold $y$ is the list $n$, then $p_{j1},w_j,r_j,d_j$ per job, then $y$, each number in binary.
• Reducibility. "Reducible" (Section 2) is read as Karp reducibility, CookPvsNP.PolyReducible from the published definition CookPvsNP_defs. The alphabet and binary number codes are those of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann); its SUBSET SUM language is not reused because it admits zero sizes, while the paper's KNAPSACK is over positive integers.
• Explicit readings of loose phrases. "We may assume that $0<b<A$" becomes a hypothesis of each milestone and an obligation on the goal's reduction. "Cf. reduction (i) and Figure 4", "Cf. Karp [19] and Figure 7" and "The equivalence follows immediately" become the stated equivalences over all feasible schedules. Reduction (c) does not specify weights; the shared construction uses unit weights.
• Not trivializable. The equivalences are stated for the paper's explicit constructions, not for an existentially chosen instance; the target languages enforce the problem class; and the goal demands polynomial-time computability, not only the equivalence.
• Infrastructure. A Turing-machine library for arithmetic on binary codes (parsing, addition, multiplication, comparison) is reusable across all seven missions of this series and across every reduction posed in the same framework. Contributions of such general lemmas are welcome.

Parts (a), (d) and (g)–(j) of Theorem 4 are formalized in other missions of this series.

Selected references

• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum, Report BW 43/75, Amsterdam, 1975; journal version: J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
• R. M. Karp, Reducibility among combinatorial problems, in: Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
• J. M. Moore, An n job, one machine sequencing algorithm for minimizing the number of late jobs, Management Science 15 (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.