The OR Formalization Drive

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

Many decision problems in control, finance and engineering must hold against an uncertain parameter $\delta$ whose distribution is unknown, while samples of $\delta$ (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the $N$ observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen $\delta$ violate it?

The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on $N$ and the dimension $d$, and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than $d$ samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.

Timeline:

• 2005–2006, Calafiore and Campi: a convex scenario program in $\mathbb R^d$ has at most $d$ support constraints; first sample-size bounds.
• 2008, Campi and Garatti: the exact bound $\mathbb P^N\{V(x^*_N)>\epsilon\}\le\sum_{i=0}^{d-1}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$, with equality for fully-supported problems.
• 2018, Campi and Garatti: the wait-and-judge bound, Theorem 1 below, with the 2008 bound as a corollary.

Setting

The decision variable is $x\in\mathbb R^d$. A problem consists of a cost vector $c\in\mathbb R^d$, a convex domain $\mathcal X\subseteq\mathbb R^d$, convex constraint sets $\mathcal X_\delta\subseteq\mathbb R^d$ indexed by $\delta$ in a probability space $(\Delta,\mathcal F,\mathbb P)$, and convex tie-break functions $t_1,\dots,t_p$. Given an i.i.d. sample $\delta^{(1)},\dots,\delta^{(N)}$ with $N>d$, the scenario program is

$$\min_{x\in\mathcal X}\ c^{\mathsf T}x\quad\text{subject to}\quad x\in\bigcap_{i=1}^N\mathcal X_{\delta^{(i)}}.$$

Ties are broken by minimising $t_1$ among the minimisers, then $t_2$, and so on; the resulting solution is $x^*_N$.

• The violation of a point is $V(x)=\mathbb P\{\delta\in\Delta: x\notin\mathcal X_\delta\}$.
• A constraint is a support constraint if removing it changes the solution; $s^*_N$ is their number.
• Assumption 1: for every $m$ and every sample of size $m$, the program with those $m$ constraints has a unique tie-broken solution.
• Assumption 2 (non-degeneracy): for every $m$, with probability one, keeping only the support constraints does not change the solution.

The variational problem (10) is: for a function $\epsilon:\{0,\dots,d\}\to[0,1]$,

$$\gamma^*=\inf_{\xi\in C^d[0,1]}\xi(1)\quad\text{s.t.}\quad\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}\xi(t)\ge\binom Nk t^{N-k}\,\mathbf 1_{[0,1-\epsilon(k))}(t),\ \ t\in[0,1],\ k=0,\dots,d.$$

Formalization targets

Goal: Theorem 1 (p. 10)

For every $[0,1]$-valued $\epsilon(k)$, under Assumptions 1 and 2,

$$\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}\ \le\ \gamma^*.$$

The level $\epsilon$ is evaluated at the observed number of support constraints. The goal fixes no particular $\epsilon$, which keeps it stable under any later choice of levels.

Milestones (the proof of Theorem 1, Sect. 5.1)

1. $s^*_m\le d$ for every sample (quoted from [7]).
2. (14): $\mathbb P^N\{V(x^*_N)>\epsilon(k)\wedge s^*_N=k\}=\binom Nk\,\mathbb P^N\{A\}$, where $A$ adds "the first $k$ constraints are of support".
3. $A=B$ up to a null set, where $B$ concerns the program on the first $k$ samples.
4. (16): $\mathbb P^N\{A\}=\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$, with $F_k(v)=\mathbb P^k\{V(x^*_k)\le v\wedge s^*_k=k\}$.
5. (17): $\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}=\sum_{k=0}^d\binom Nk\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$.
6. (18): $\sum_{k=0}^{\min\{m,d\}}\binom mk\int_{[0,1]}(1-v)^{m-k}\,\mathrm dF_k(v)=1$ for every $m$.
7. Weak duality between the truncated moment problem (20) and its dual (21), giving (22).
8. (23): $\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}t^m=\binom mk t^{m-k}$ for $m\ge k$, and $0$ otherwise.
9. (24): the infimum of $p(1)$ over polynomials feasible for (10) equals $\gamma^*$.

Companions

• Theorem 2 (p. 11): for $\beta\in(0,1)$ and $\epsilon(k)=1-t(k)$, with $t(k)$ the unique root in $(0,1)$ of $\frac{\beta}{N+1}\sum_{m=k}^N\binom mk t^{m-k}-\binom Nk t^{N-k}=0$, the probability is at most $\beta$.
• The root lemma of Sect. 5.3, including its sign and divergence claims.
• $\gamma^*\le\sum_{i<d}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ for constant $\epsilon$ (Sect. 5.2).
• Corollary 1, the 2008 bound.

Significance

Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of $\epsilon(k)$, a user who finds $k\ll d$ support constraints obtains a level $\epsilon(k)$ comparable to that of a $k$-dimensional problem, which is far below the a-priori level for dimension $d$. The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.

The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:

• a formal account of scenario programs with lexicographic tie-break and of support constraints in the "changes the solution" sense;
• the exchangeability argument (14) on product measures;
• the representation (17) of a tail probability through generalized distribution functions;
• a weak-duality argument for a generalized moment problem. The 2008 bound itself is posed on the platform as an open problem under other hypotheses; Corollary 1 states it under this paper's assumptions.

Difficulty

The obvious approach bounds the probability for each value of $s^*_N$ separately by a binomial tail, then sums. This fails: the event $s^*_N=k$ is not known in advance, and summing the individual bounds over $k$ loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the $(d+1)$-tuple $(F_0,\dots,F_d)$. It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in $d+1$ measures, and solves it by duality.

Two steps carry most of the work. One is the almost-sure identity $A=B$, which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in $C^d[0,1]$. The bound $s^*_N\le d$ itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.

Formalization scope

• Spaces. The decision space is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from $0$. $\mathbb P$ is a probability measure and $\mathbb P^N$ is the product measure.
• Tie-break. The tie-broken solution is the lexicographic minimiser of $(c^{\mathsf T}x,t_1(x),\dots,t_p(x))$ and depends only on the feasible set, which is what makes the exchangeability step valid. A support constraint is one whose removal changes this solution; this is not the platform's earlier "removal lowers the cost" notion.
• Assumptions. Assumption 1 is required for every sample, Assumption 2 almost surely.
• Measurability. The paper takes measurability for granted (footnote 1). Here it is two explicit hypotheses: the relation $\{(x,\delta):x\in\mathcal X_\delta\}$ is measurable, and every solution map $\omega\mapsto x^*_m(\omega)$ is measurable. No event is assumed measurable directly.
• $F_k$. $F_k$ is the finite measure on $\mathbb R$ given by the law of $V(x^*_k)$ on the event $\{s^*_k=k\}$; it is not normalised.
• Problem (10). $C^d[0,1]$ is ContDiffOn ℝ d on $[0,1]$, with derivatives taken within $[0,1]$. $\gamma^*$ is a real infimum over a set that is nonempty ($\xi(t)=t^N$) and bounded below by $0$.
• Probabilities are compared with real quantities through ENNReal.ofReal.
• Theorem 2 is stated for every $\epsilon$ whose values $1-\epsilon(k)$ are roots of (11) in $(0,1)$, which by its first part is the paper's $\epsilon$.
• Added hypothesis. The constant-$\epsilon$ companion assumes $d\ge1$: at $d=0$, $\epsilon=0$ its inequality is false.

Ruled-out trivializations:

• The solution is never a free function of the sample.
• The goal does not mention $F_k$, moments or polynomials.
• Assumption 1 is not weakened to almost surely.
• $N>d$ is kept on Theorems 1, 2 and Corollary 1.
• The indicators keep the paper's open and closed ends: $[0,1-\epsilon(k))$ in (10), $(\epsilon(k),1]$ in (16)–(21).

Contributions welcome:

• the support-constraint bound under lexicographic tie-break, which is reusable for any convex scenario result;
• the exchangeability lemma on Measure.pi;
• the duality and density lemmas, which are pure analysis.

Selected references

• M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming 167 (2018). https://doi.org/10.1007/s10107-016-1056-9
• G. C. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102 (2005). https://doi.org/10.1007/s10107-003-0499-y
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51 (2006). https://doi.org/10.1109/TAC.2006.875041
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19 (2008). https://doi.org/10.1137/07069821X

Motivation

A solution of a scenario optimization program is chosen after observing finitely many uncertain constraints. Its future reliability depends on constraints that were not sampled. The usual advance question asks how many samples are needed to make every output reliable. Campi and Garatti instead ask what can be certified after solving the program, when the number of sampled constraints that actually determined its solution is visible. Their wait-and-judge result uses that observed number to set a violation threshold. This mission concerns their extension from convex programs in finite-dimensional spaces to programs over an arbitrary decision set, with no convexity requirement.

The generic extension matters when a dimension bound on the number of influential constraints is unavailable. A decision may be a combinatorial object, a function, or an element of an infinite-dimensional space. The paper allows the support count to range from zero to the full sample size $N$, and its threshold includes the case of $N$ support constraints. The paper's Section 6 gives the model and its two probability guarantees.

Setting

Let $S$ be a set of decisions. A subset $X\subseteq S$ is the domain; a real function $f:S\to\mathbb R$ is the cost. An uncertain outcome $\delta$ belongs to a measurable space $\Delta$ with probability measure $P$, and imposes a constraint set $X_\delta\subseteq S$. For a sample $\omega=(\delta^{(1)},\ldots,\delta^{(N)})$ of $N$ independent outcomes, the program minimizes $f(x)$ over $x\in X$ that belongs to every sampled $X_{\delta^{(i)}}$. The sample law is $P^N$. There is no algebraic or topological condition on the feasible sets or on $f$.

A fixed finite sequence of real tie-break functions is minimized lexicographically after the original cost. This selects one solution $x_N^*(\omega)$ whenever the program has a selected minimizer. Assumption 1 requires existence and uniqueness for every finite sample, including the empty one. A sampled constraint is a support constraint if removing it changes this selected solution. The number of support constraints is $s_N^*(\omega)$. Assumption 2 says that, with probability one, keeping only the support constraints gives the same selected solution. Both assumptions are part of the source's generic setting; they are substantive restrictions even though the sets and cost are otherwise arbitrary.

The violation of a decision is $V(x)=P\{\delta:x\notin X_\delta\}$. Thus $V(x_N^*)$ is the probability that a fresh constraint rejects the computed solution. Since the solution and support count depend on the sample, the wait-and-judge event uses a threshold function $\varepsilon$ evaluated at the observed count, $\{V(x_N^*)>\varepsilon(s_N^*)\}$. For each $k\ge0$, the paper also uses a generalized distribution function $F_k(v)=P^k\{V(x_k^*)\le v,\ s_k^*=k\}$. It need not have total mass one.

Formalization targets

Variational bound, Theorem 3

For any $N\ge1$ and any $[0,1]$-valued $\varepsilon$ on $\{0,\ldots,N\}$, let $\gamma^*$ be the infimum of feasible values $q(1)$ over real polynomials of degree at most $N$ satisfying

$$\frac{q^{(k)}(t)}{k!}\ge {N\choose k}t^{N-k}{\bf1}_{[0,1-\varepsilon(k))}(t),\qquad 0\le k\le N,\quad 0\le t\le1.$$

The goal is the paper's Theorem 3:

$$P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\gamma^*.$$

The polynomial value retains the full dependence on the chosen threshold function. The source prints an extraneous $d$ in Theorem 3's range for $k$; its generic setting and variational problem use $0\le k\le N$.

Explicit confidence bound, Theorem 4

For $0<\beta<1$, the paper's Theorem 4 defines $t(k)\in(0,1)$ as the unique root of

$$\frac{\beta}{N+1}\sum_{m=k}^{N}{m\choose k}t^{m-k}-{N\choose k}t^{N-k}=0\qquad(0\le k<N).$$

With $\varepsilon(k)=1-t(k)$ for $k<N$ and $\varepsilon(N)=1$, its conclusion is

$$P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\beta.$$

The terminal value $\varepsilon(N)=1$ is essential because the paper gives examples with $s_N^*=N$ and $V(x_N^*)=1$.

Significance

Theorem 3 makes the observed support count a usable statistic for assessing the solution's future constraint violation without a dimension bound. Theorem 4 turns it into a certificate at any chosen confidence parameter $\beta$. The confidence threshold depends on the count seen after the program is solved. These statements do not claim that every generic program satisfies Assumptions 1–2; they say what follows for programs that do.

A formal development must make the statistical objects and the analytic value agree exactly: the solution must come from the feasible set and the fixed tie-break rule, the support count must record changes of solution, and $\gamma^*$ must be the value of the derivative-constrained polynomial problem. The reusable outputs include the generic scenario model, its generalized violation distributions, and the finite moment and dual formulations. The statements are known results of Campi and Garatti; this mission asks for machine-checked proofs of those results and their selected intermediate claims.

Difficulty

The observed support count is data-dependent. Conditioning on $s_N^*=k$ therefore cannot be treated as conditioning on a fixed subset of $k$ sample coordinates. Symmetry across possible support subsets must agree with the selected solution under removal of nonsupport constraints. Assumption 2 is what rules out a degenerate change of solution when only support constraints remain. In the generic setting the possible count grows with $N$, so the distributional characterization has one measure $F_k$ for every $k\ge0$ and moment equations for every sample size. The resulting infinite family must still be related to the finite degree-$N$ polynomial value in (31). No convexity or finite-dimensional geometry is available to supply a fixed support bound.

Formalization scope

Lean represents the decision set by an arbitrary type $S$, with a measurable structure only to state the paper's implicit measurability convention. Samples are functions Fin N → Δ with zero-based indices and product law Measure.pi. The published generic violation definition is reused. The domain, constraint family, cost, finite lexicographic tie-break, selected solution, support set, and $F_k$ are defined locally. A Nonempty S instance provides an unused fallback value to the total solution selector; Assumption 1 already implies that $S$ is nonempty.

The source takes measurability for granted in a footnote. Here the constraint relation is jointly measurable, every solution map is measurable, and each support event is measurable. These pins assign probabilities to the events the paper uses. The $F_k$ are finite measures on $\mathbb R$, so the paper's Stieltjes integrals are represented as integrals over $(\varepsilon(k),1]$ or $[0,1]$ against those measures. The polynomial class $\mathcal P_N$ means degree at most $N$, matching the $N+1$ coefficients in (36). The value $\gamma^*$ is a real infimum; a separate sanity proof gives a feasible polynomial and a zero lower bound on all feasible values.

The goal retains Assumptions 1–2 and states the actual tail bound. It does not assume the moment equations or a favorable value of $\gamma^*$, and no support count is fixed in advance. Contributions toward the distributional decomposition, the moment equations, the finite weak-duality inequality, the polynomial identity, and the explicit-root theorem are within scope.

Selected references

• M. C. Campi and S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. DOI: 10.1007/s10107-016-1056-9. The mission uses the authors' accepted manuscript, especially Sections 6–7 and Theorems 3–4.

Motivation

An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of $1-1/e$ for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).

The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.

Setting

There are $n$ boys, represented by rows, and $n$ girls, represented by columns. A bipartite graph $G\subseteq[n]\times[n]$ records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of $G$. This assumption supplies an offline benchmark of $n$ matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.

Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order $n,n-1,\ldots,1$. A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance $p(A)$ is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).

The paper's hard family begins with the complete upper-triangular graph $T_n$, where row $i$ is adjacent to column $j$ exactly when $i\le j$. Its columns arrive from largest to smallest. Relabeling the rows by a permutation $\pi$ gives an instance $T_\pi$ that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write $V_{T_n}(n,\varnothing)$ for RANDOM's expected number of matches on $T_n$, beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).

Formalization targets

Main theorem

For every $\varepsilon>0$, there is one threshold $N$ such that, for every $n\ge N$ and every randomized online algorithm $A$ on $n$ rows and columns, a graph $G$ with a perfect matching satisfies

$$\mathbb E_A[|M(G)|]\le (1-e^{-1}+\varepsilon)n.$$

The threshold is uniform over algorithms. The graph may depend on $A$. This is the quantified upper-bound reading of Theorem 2's $p(A)\le n(1-1/e)+o(n)$ (Karp, Vazirani, and Vazirani, 1990, Theorem 2).

Milestone statements

Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted $T_n$ with RANDOM's expected size on $T_n$. Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit

$$\lim_{n\to\infty}\frac{V_{T_n}(n,\varnothing)}{n}=1-e^{-1}.$$

Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).

Significance

Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from $n$ is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.

Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.

Difficulty

For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the $o(n)$ claim in Lemma 16.

Formalization scope

Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order $n,\ldots,1$ is represented by zero-based order $n-1,\ldots,0$; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.

RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For $n=0$, the matching and RANDOM value are zero; the main theorem is eventual in $n$ and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's $o(n)$ in Theorem 2 is stated as $\forall\varepsilon>0,\exists N,\forall n\ge N$ with $N$ before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.

Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.

Selected references

• Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, pp. 352–358, 1990. DOI: 10.1145/100216.100262.

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

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

Minimum makespan scheduling on unrelated parallel machines asks for an assignment of $n$ jobs to $m$ machines, where job $j$ takes $p_{ij}$ time units on machine $i$, so that the largest machine load is as small as possible. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) it is $R\,\|\,C_{\max}$. It models load balancing across heterogeneous processors, workers or production lines, and it is a standard test case for linear-programming rounding.

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714; Mathematical Programming 46, 1990) gave a polynomial 2-approximation algorithm for $R\,\|\,C_{\max}$ and showed that no polynomial algorithm achieves a ratio below $3/2$ unless P = NP. They also asked which restrictions on the processing times keep the problem hard. Their Section 5 answers this when only two distinct processing times occur:

• all $p_{ij}=1$: trivial;
• all $p_{ij}\in\{1,\infty\}$: bipartite cardinality matching;
• all $p_{ij}\in\{1,2\}$: polynomial by matching techniques (Theorem 6);
• all $p_{ij}\in\{p,q\}$ with $p<q$, $2p\ne q$: NP-hard (Theorem 7).

Theorem 7 is the paper's last result and closes this classification. Its proof generalizes the reduction of Theorem 4, which handles the case $\{1,3\}$, from 3-dimensional matching to $q$-dimensional matching.

Setting

Machines are indexed by $i\in\{1,\dots,m\}$ and jobs by $j$. A schedule $\sigma$ assigns every job to exactly one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$, and the makespan $C_{\max}(\sigma)$ is the largest load.

$q$-dimensional matching. An instance is a ground set $U$ of $qn$ elements and a family $S_1,\dots,S_m$ of $q$-element subsets of $U$. A matching is a subfamily $F'\subseteq\{1,\dots,m\}$ with $|F'|=n$ and $\bigcup_{i\in F'}S_i=U$; its members are then pairwise disjoint.

The instance of Theorem 7. Fix natural numbers $0<p<q$ that are relatively prime. Build a scheduling instance with $m$ machines, machine $i$ corresponding to $S_i$, and two kinds of jobs:

• $qn$ element jobs, one per $u\in U$, with $p_{iu}=p$ if $u\in S_i$ and $p_{iu}=q$ otherwise;
• $p(m-n)$ dummy jobs, each taking $q$ time units on every machine.

Every processing time lies in $\{p,q\}$.

The instance of Theorem 4. For disjoint sets $A=\{a_1,\dots,a_n\}$, $B$, $C$ of the same size and triples $T_i=(a_j,b_k,c_l)$, $i=1,\dots,m$, there are $3n$ element jobs, one per element of $A\cup B\cup C$, and $m-n$ dummy jobs. Machine $i$ processes the element jobs of $a_j$, $b_k$, $c_l$ in one time unit and every other job in three time units. A 3-dimensional matching is a subfamily of $n$ triples covering $A\cup B\cup C$.

Formalization targets

Goal: Theorem 7 (p. 8; proof pp. 8–9)

For relatively prime $0<p<q$ and a family of $q$-subsets $S_1,\dots,S_m$ of a $qn$-element set, the instance above has all processing times in $\{p,q\}$, and

$$\exists\,\sigma:\ C_{\max}(\sigma)\le pq \quad\Longleftrightarrow\quad \exists\,F'\subseteq\{1,\dots,m\}:\ |F'|=n,\ \bigcup_{i\in F'}S_i=U .$$

Milestones

1. Theorem 4 (p. 7): on the 3-dimensional matching instance with times in $\{1,3\}$, a schedule with makespan at most $3$ exists iff a matching exists.
2. Matching gives a schedule (pp. 8–9): if $S$ has a matching, some schedule has $C_{\max}\le pq$.
3. No idle time, two kinds of machine (p. 9): in every schedule with $C_{\max}\le pq$, three things hold. Every load equals $pq$. Every element job runs at length $p$, on a machine whose tuple contains it. Each machine processes either exactly $q$ element jobs and no dummy job, or exactly $p$ dummy jobs and no element job.

Significance

The result. Theorems 6 and 7 together say exactly which two-valued restrictions of $R\,\|\,C_{\max}$ are tractable. Up to scaling, the polynomial case is $\{1,2\}$, and every other pair $\{p,q\}$ with $p<q$ is NP-hard. Theorem 4 is the base case. It also yields Corollary 1 of the paper: no polynomial $\rho$-approximation with $\rho<4/3$ exists unless P = NP. Reductions of this "no idle time" kind are a standard template for hardness of restricted-assignment and two-value scheduling, a line still active in the study of the restricted assignment problem and of the "graph balancing" special case.

Formalizing it. The result is proved, in two short paragraphs. The proof leaves to the reader the construction of the schedule from a matching and the "easy number theoretic argument" behind the converse, and both become explicit here. The development also produces reusable pieces: a $q$-dimensional matching definition over an arbitrary family of $q$-sets, and two reduction instances built on the published load and makespan of MatousekLP.Scheduling.Schedule. To our knowledge no machine-checked proof of these reductions exists.

Difficulty

The forward direction is a direct construction. The converse is where care is needed. A schedule with makespan at most $pq$ may a priori place an element job on a machine whose tuple does not contain it, at length $q$, and may mix element and dummy jobs on one machine. Looking at one machine at a time does not exclude either: a single machine can carry such a mixed load below $pq$. What excludes them is a property of the whole schedule together with the arithmetic of $p$ and $q$. The hypotheses are sharp for this step: for $p>q$ element jobs are cheaper on foreign machines, and for $\gcd(p,q)>1$ a load $ap+bq=pq$ with $a,b>0$ becomes possible.

Formalization scope

• Model. Machines are Fin m. Schedules are maps from jobs to machines. Load and makespan are those of the published MatousekLP.Scheduling.Schedule, with natural-number processing times cast to $\mathbb R$. The jobs are enumerated as Fin (q * n + p * (m - n)) (Theorem 7) and Fin (3 * n + (m - n)) (Theorem 4), element jobs first, through finSumFinEquiv.
• Ground set and family. The ground set is Fin (q * n) and the family is indexed by machines, so repeated tuples are allowed. The $q$-partite structure of $q$-dimensional matching is not imposed: the reduction does not use it, and statements over all families of $q$-sets contain the $q$-partite case. Theorem 4 keeps the tripartite structure, with triples of indices in Fin n × Fin n × Fin n.
• Threshold. The thresholds are exactly $pq$ and $3$, with "makespan at most".
• Complexity wording not formalized. "NP-hard" (Theorem 7) and "NP-complete" (Theorem 4) are not formalized: membership in NP, polynomial size of the reductions, and the hardness of the matching problems are not stated. What is stated is the equivalence each reduction establishes.
• Hypotheses. Theorem 7's goal assumes $0<p<q$, $\gcd(p,q)=1$ and $|S_i|=q$. The paper's general case $\gcd(p,q)=g>1$ is its stated "without loss of generality": divide all times by $g$, which divides every makespan by $g$. It is not part of the formal statement. The paper's hypothesis $2p\ne q$ is dropped because the reduction does not use it. With coprime $p<q$ it excludes only $(p,q)=(1,2)$, where the equivalence still holds but the source problem is bipartite matching. The formal goal is therefore stronger than the paper's.
• Edge cases. For $m<n$, natural-number subtraction gives no dummy jobs; both sides of each equivalence are false when $n\ge1$. This stands in for the paper's "trivial 'no' instance". For $n=0$ the empty family is a matching and the dummy jobs fill the machines exactly.
• No trivialization. The goal is an equivalence about a constructed instance whose processing times are given by explicit definitions. Neither side is assumed, the schedule is quantified over all maps from jobs to machines, and the instance is not a free parameter pinned by hypotheses.
• Welcome contributions. Besides the milestones: counting lemmas relating a machine's load to the numbers of jobs of each length on it, and lemmas on the makespan of MatousekLP.Scheduling.Schedule (it bounds every load; it is attained when $m\ge1$), which are reusable across scheduling reductions.

Selected references

• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Amsterdam, 1987 (the version formalized here); journal version in Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem SP1).
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3 (the schedule, load and makespan definitions reused here). https://doi.org/10.1007/978-3-540-30717-4