The OR Formalization Drive

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

Motivation

A firm may know salary bounds and the ranking of positions without having a reliable sample of individual salaries suitable for least-squares estimation. Charnes, Cooper and Ferguson used that kind of partial information to estimate a salary formula from ratings assigned to job factors. Their 1955 paper gives a model in which weights respect the job hierarchy while the implied salaries approach specified salary levels as closely as possible. It then turns the sum of absolute deviations into a linear program that can be handled by the methods available for constrained optimization. The setting and transformation are in §§4–6 of the published paper.

The question here is a precise one: does the transformed program have the same optimal value and the same optimal salary weights as the original absolute-deviation problem? This matters because a linear-program solution should answer the compensation-estimation problem stated before the transformation, even though the transformed program has additional variables and a different feasible set. The mission also records the paper's seven-position numerical example, where the reported salary formula can be checked directly against the table of factor ratings.

Setting

There are $n$ rated factors and $L\ge1$ job levels ordered from highest to lowest. The rating $x_{ik}$ is the amount of factor $i$ required at level $k$, and $a_i$ is the nonnegative weight assigned to that factor. The estimated salary at level $k$ is

$$S_k(a)=\sum_{i=1}^{n}a_i x_{ik}.$$

The salary formula applied to a person's factor amounts $y_i$ is $s=\sum_i a_i y_i$. For the ranked positions, feasible weights satisfy the four parts of the paper's system (2): each $a_i\ge0$; the top-level salary is at most the ceiling $s_M$; successive salaries descend, $S_{k+1}(a)\le S_k(a)$; and the bottom-level salary is at least the floor $s_m$. These are one-sided ceiling and floor bounds. They do not force the fitted salaries to equal the bounds.

The firm specifies target salaries $s_k$ at a finite set $K$ of levels, which includes the ceiling and floor levels in the examples and may include intermediate levels. The absolute-deviation objective of (3) is

$$D(a)=\sum_{k\in K}|S_k(a)-s_k|.$$

The original problem minimizes $D$ over the feasible weights. At a specified level, let $w_k=S_k(a)-s_k$. The split-variable program of (4)–(5) introduces $u_k,v_k\ge0$ with $w_k=u_k-v_k$ and minimizes $P(u,v)=\sum_{k\in K}(u_k+v_k)$. The split variables are constrained only for levels in $K$. The salary constraints (2) continue to apply to $a$. This is the paper's transformed linear program, with a feasible set that contains many choices of $(u,v)$ above the same weight vector Charnes, Cooper and Ferguson, §§4–5.

Formalization targets

Equivalence of the two programs

The main target is the paper's claim that the two problems have equal minimal values and that minimizers correspond §6, p. 143. In the formal statement, equal values are expressed by equality of attainable objective thresholds:

$$\forall t\in\mathbb R,\qquad [\exists a\text{ feasible}:D(a)\le t] \quad\Longleftrightarrow\quad [\exists(a,u,v)\text{ LP-feasible}:P(u,v)\le t].$$

The goal also says that $a$ minimizes $D$ exactly when the triple formed from $a$ and the positive and negative parts of $w$ minimizes $P$. Every LP minimizer projects to a minimizer of $D$. These clauses give the value and solution correspondence the authors use when they call the two problems equivalent.

Supporting claims and numerical result

Three milestones follow the paper's exposition. First, every feasible weight vector has a split-variable lift with the same objective. Second, every transformed feasible point projects to an original feasible weight vector with no larger original objective. Third, the minimal values agree §§5–6, pp. 141–143. Each is recorded under the unnumbered sentence from which it was extracted; the paper has no numbered lemmas.

Two companion statements record other claims: opposite coefficient columns cannot both occur among selected independent simplex columns, and the Table I data have the reported optimum. For the latter, targets are 16 at $R_1$, 10 at $R_5$, and 4 at $R_7$, measured in thousands of dollars. Equation (7) assigns weights $(4,0,0,16,0,4,0,28,0)/11$, yielding the minimum deviation $14/11$ §7, pp. 145–148. A further companion checks the redundant $R_2\le R_1$ ranking row.

Significance

The equivalence justifies using a linear-program output as an estimate for the earlier salary problem: the transformed objective reaches the same value, and its optimal weight vectors solve the original problem. The numerical claim supplies a fully specified instance with seven job levels and nine factors, including the exact fitted salaries. Without the correspondence, optimizing the enlarged variable set could give no assurance that its weights minimize the deviations the firm intended to measure.

The mathematical result was argued in the 1955 paper; this mission asks for a machine-checked formulation and proof of that known result. The statements compile as open Lean theorems, so compilation alone does not establish their truth. Closing them would add a reusable treatment of absolute-deviation objectives under finite linear inequalities and an exact certificate for the paper's worked example. The consistency claim in the appendix is a separate mission because it concerns perturbations of another linear program, not this transformation.

Difficulty

The split-variable program permits $u_k$ and $v_k$ to be simultaneously positive even when their difference is fixed. Consequently, simply identifying the two feasible sets would misstate the transformation: one has extra degrees of freedom. A proof must relate their objective values and then account for optimal solutions on both sides. The numerical example has a separate difficulty. Substituting the reported weights verifies a feasible objective of $14/11$, but does not by itself rule out another feasible weight vector with a smaller deviation. The global lower bound is part of the companion theorem.

Formalization scope

The Lean development represents factor and level vectors by functions on Fin n and Fin L, and sums explicitly over finite indices. Paper level 1 is Lean index 0; paper level $L$ is the final Fin L index. The assumption $L\ge1$ is explicit because both the top and bottom level are named. No sign, monotonicity, or boundedness assumptions are imposed on the ratings beyond what the paper states. The weights are componentwise nonnegative. Intermediate target salaries enter the objectives through $K$ but add no constraints to (2), matching the paper's treatment of $R_5$.

A minimizer is a feasible point whose objective is no larger than that of every feasible point. The equality of minimal values uses the threshold formula above, so an empty feasible set cannot inherit a spurious real infimum. The transformed feasible set is exactly the split-variable system of (4)–(5); defining it as only the image of a chosen lift would make the principal comparison empty of content. The Table I constants are exact rational values in units of $1{,}000$. The paper rounds some displayed salaries, while Lean records their exact fractions. The generic column-independence companion is stated for an arbitrary finite matrix, with the basis and zero nonbasic coordinates explicit.

The shared definition module provides the salary map, feasibility predicates, objectives, minimizers, and example data. A full development can contribute proofs of the three milestones, the main equivalence, the column claim, the numerical lower bound, and the redundant-row fact. The finite absolute-deviation and split-variable statements can also serve later formalizations with other linear constraints.

Selected references

• A. Charnes, W. W. Cooper, and R. O. Ferguson, Optimal Estimation of Executive Compensation by Linear Programming, Management Science 1(2), 138–151, 1955. DOI 10.1287/mnsc.1.2.138.

Motivation

Minimum makespan scheduling on unrelated parallel machines, written $R\,||\,C_{\max}$, is one of the basic models of scheduling theory: $n$ jobs must each be run on one of $m$ machines, and the time a job takes depends arbitrarily on the machine. Lenstra, Shmoys and Tardos (CWI Report OS-R8714, 1987; journal version Math. Programming 46, 1990) gave a polynomial 2-approximation algorithm for this problem and, in the same paper, a matching limit from below: no polynomial algorithm can guarantee a factor smaller than $3/2$ unless $P = NP$ (their Corollary 2).

The two bounds have stood for more than three decades. Closing the gap between $3/2$ and $2$ for $R\,||\,C_{\max}$ is listed among the central open problems of approximation algorithms (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, open problem on unrelated machines; Schuurman and Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 1999). The lower bound of $3/2$ is the subject of this mission.

Timeline:

• 1979: Graham, Lawler, Lenstra and Rinnooy Kan introduce the classification $R\,||\,C_{\max}$.
• 1987/1990: Lenstra, Shmoys and Tardos prove NP-completeness of deciding makespan at most 3 (Theorem 4, giving the bound $4/3$) and at most 2 (Theorem 5, giving $3/2$), both by reduction from 3-dimensional matching.
• Since then: the $3/2$ hardness bound has not been improved for general $R\,||\,C_{\max}$; progress has concentrated on special cases such as the restricted-assignment problem.

Setting

3-dimensional matching. There are three disjoint sets $A = \{a_1,\dots,a_n\}$, $B = \{b_1,\dots,b_n\}$, $C = \{c_1,\dots,c_n\}$ and a family $F = \{T_1,\dots,T_m\}$ of triples, each with one element of $A$, one of $B$ and one of $C$. A matching is a subfamily $F'$ with $|F'| = n$ whose union is $A \cup B \cup C$. In Lean an instance is a map $T : \mathrm{Fin}\,m \to \mathrm{Fin}\,n \times \mathrm{Fin}\,n \times \mathrm{Fin}\,n$, and HasMatching T says that a matching exists.

The scheduling model. Machines are $\mathrm{Fin}\,m$, jobs are $\mathrm{Fin}\,N$, and $p_{ij}$ is the positive integer processing time of job $j$ on machine $i$. A schedule $\sigma$ assigns each job to 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. These are the published definitions MatousekLP.Scheduling.load and makespan.

The instance of Theorem 5. The triples containing $a_j$ are the triples of type $j$; let $t_j$ be their number. From $T$ the paper builds a scheduling instance with $m$ machines, machine $i$ corresponding to $T_i$, and with

1. $2n$ element jobs, one for each $b_k$ and each $c_l$;
2. $t_j - 1$ dummy jobs of type $j$, for each $j$.

If $T_i = (a_j, b_k, c_l)$, machine $i$ processes the element jobs of $b_k$ and $c_l$ in time $1$, each dummy job of type $j$ in time $2$, and every other job in time $3$. In Lean the processing-time matrix is P T.

A $\rho$-approximate schedule of an instance is a schedule $\sigma$ with $C_{\max}(\sigma) \le \rho\, C_{\max}(\tau)$ for every schedule $\tau$ of the same instance.

Formalization targets

Goal: Corollary 2 (p. 8)

For every instance $T$, every $\rho < 3/2$, and every $\rho$-approximate schedule $\sigma$ of the instance of Theorem 5 built from $T$,

$$C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.$$

This is the mathematical content of "for every $\rho < 3/2$ there is no polynomial $\rho$-approximation algorithm unless $P = NP$": a $\rho$-approximate answer on the reduced instance decides 3-dimensional matching.

Theorem 5 (p. 7)

For every instance $T$,

$$\exists\,\sigma:\ C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.$$

Milestones from the proof of Theorem 5 (pp. 7–8)

1. If every $t_j \ge 1$, then $\sum_j (t_j - 1) + n = m$: there are $m - n$ dummy jobs.
2. A matching yields a schedule with makespan at most $2$.
3. A schedule with makespan at most $2$ yields a matching.

Significance

The result. Theorem 5 shows that $R\,||\,C_{\max}$ is NP-hard already when every processing time lies in $\{1,2,3\}$ and the target makespan is $2$. Corollary 2 turns this into the best known inapproximability bound for the problem, $3/2$, which sits opposite the paper's own factor-2 algorithm. The same reduction pattern (machines as triples, dummy jobs that pin machines down) is reused in many later hardness proofs for scheduling and assignment problems.

Formalizing it. The result is proved on paper; no machine-checked version is known to exist. A formal proof requires the full combinatorial argument behind the reduction, including the counting of machines per type and the case where some element of $A$ lies in no triple, which the paper does not discuss. Together with mission 1 of this series (the factor-2 algorithm), it fixes both ends of the $[3/2, 2]$ gap in one formal library.

Difficulty

The construction is short, but the converse direction carries the weight: from an arbitrary schedule with makespan at most $2$ one must recover a matching, although nothing in the schedule singles out the triples that form it. The obvious first idea, to read the matching off the machines that receive unit-time jobs, fails as it stands: a machine may receive one unit-time job or none, and the argument must exclude this for every schedule, including the degenerate instances in which some $a_j$ lies in no triple or triples repeat. For Corollary 2, the passage from the real-valued approximation guarantee to the threshold $2$ depends on the strict inequality $\rho < 3/2$; at $\rho = 3/2$ the statement is no longer implied by Theorem 5.

Formalization scope

• Machines are Fin m; 3DM elements are Fin n; a 3DM instance is T : Fin m → Fin n × Fin n × Fin n, so a triple may repeat. A matching is a set of $n$ triple indices covering every $a_j$, $b_k$, $c_l$ (the covering form of the paper's definition, which forces disjointness).
• The jobs of the reduced instance are the sum type $\mathrm{Fin}\,n \oplus \mathrm{Fin}\,n \oplus \Sigma_j\,\mathrm{Fin}(t_j - 1)$. They are enumerated by a fixed bijection with $\mathrm{Fin}\,N$ so that the published MatousekLP.Scheduling.makespan applies. All statements quantify over every schedule, so the choice of bijection is irrelevant.
• $t_j - 1$ is natural-number subtraction. When some $t_j = 0$ (a case the paper leaves aside), type $j$ has no dummy job; the reduced instance then has neither a matching nor a schedule of makespan at most $2$, so Theorem 5 and Corollary 2 hold as stated, with no hypothesis $t_j \ge 1$. Only the dummy-count milestone assumes $t_j \ge 1$.
• Processing times are natural numbers cast to $\mathbb R$; makespans are real.
• Not formalized: "polynomial" (running time of an algorithm and of the reduction), membership in NP, "NP-complete" and "unless $P = NP$". Theorem 5 is stated as the reduction's equivalence; Corollary 2 is stated as the fact that any $\rho$-approximate schedule of the reduced instance, $\rho < 3/2$, decides 3-dimensional matching. The reduction is evidently polynomial, but this is not stated.
• The approximation hypothesis compares $\sigma$ with every schedule $\tau$ of the same reduced instance; a goal in which $\sigma$ is an arbitrary schedule, or is bounded against an unrelated quantity, would be a different statement. The strict inequality $\rho < 3/2$ is essential and kept.
• Contributions welcome: proofs of the three milestones, of Theorem 5 from them, and of Corollary 2; reusable lemmas about integer-valued makespans and about sum-type job sets.

Selected references

• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (FOCS 1987); the version cited for every theorem number in this mission.
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• 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
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem [SP1]).
• P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, Journal of Scheduling 2 (1999) 203–213. https://doi.org/10.1002/(SICI)1099-1425(199909/10)2:5<203::AID-JOS26>3.0.CO;2-5
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

Motivation

Finite-horizon Markov decision processes ask which decisions minimize accumulated cost over a specified number of stages. In a stationary process, the same costs and transitions apply at every stage. This compact input can describe a horizon $T$ much larger than the state set, so a method that processes all $T$ stages one by one may take time exponential in the length of the written horizon. Papadimitriou and Tsitsiklis identified this issue while comparing sequential and parallel algorithms for decision processes. For the deterministic stationary case, their Theorem 5 states an NC classification, supported by a finite structural description of a cheapest long walk. Papadimitriou and Tsitsiklis (1987)

The structural description is the subject of this mission. It connects a policy optimization problem to bounded-length graph objects and an exact cost identity. This is useful independently of a particular model of parallel computation: it says which shorter walk and cycle costs determine the answer even when the horizon is very large. Papadimitriou and Tsitsiklis (1987), p. 447

Setting

Let $S$ be a finite nonempty set of states, with $n=|S|$, and fix an initial state $s_0$. At each state $s$, a finite nonempty set $D_s$ contains the available decisions. A decision $d\in D_s$ has a certain successor state $\operatorname{next}(s,d)$ and a real cost $c(s,d)$. The model is stationary: these data do not depend on time. The corresponding directed graph has one arc for each decision. It may have loops and parallel arcs, because distinct decisions can share endpoints. This is the deterministic graph translation made in §3 of the paper. Papadimitriou and Tsitsiklis (1987), pp. 444–445

A policy is a function $\delta(s,t)\in D_s$ of both state and time. Starting at $s_0$, it produces $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. In the convention of the paragraph before Theorem 5, horizon $T$ means $T$ decisions and therefore a walk with $T$ arcs. Its cost is

$$J_T(s_0,\delta)=\sum_{t=0}^{T-1}c(s_t,\delta(s_t,t)),\qquad J_T^*(s_0)=\inf_\delta J_T(s_0,\delta).$$

A walk records the states and the decision arc used at each step; states may repeat. A simple path has no repeated state. A simple cycle has positive length, returns to its starting state, and has no other repeated state. A closed walk may repeat states internally and need not be a simple cycle. The distinction matters because the structural claim uses a simple cycle, whereas the computation in the target identity uses a cheapest closed walk of a chosen length.

Formalization targets

The first milestone identifies $J_T^*(s_0)$ with the minimum cost of a $T$-arc walk from $s_0$. The next milestones record a decomposition into a simple path and simple cycles, the restriction on cycles repeated more than $n$ times, and the existence of a cheapest walk with a short prefix and one repeated simple cycle. These are claims in the paragraph preceding Theorem 5, with corrections to the printed exchange and its connectivity justification documented in the formal statements. Papadimitriou and Tsitsiklis (1987), p. 447

For $l\le T$ and $u\in S$, let $w_{l,u}$ be the cheapest $l$-arc walk from $s_0$ that visits $u$. Let $r_{k,u}$ be the cheapest closed $k$-arc walk at $u$. Only choices for which these walks exist are included. The mission's goal is

$$J_T^*(s_0)=\min_{\substack{l\le T,\ l<n^3,\ u\in S,\\1\le k\le n,\ k\mid T-l}}\left(w_{l,u}+\frac{T-l}{k}\,r_{k,u}\right),\qquad T>n^2.$$

The $l<n^3$ bound is the paper's finite compression claim. The divisibility condition makes $(T-l)/k$ an integer number of cycle copies. The goal states an exact value, with the inner minima taken over genuine walks and the outer optimum still taken over all policies. Papadimitriou and Tsitsiklis (1987), p. 447

Significance

The identity replaces an optimization over arbitrarily many time-dependent policy decisions with costs of walks having fewer than $n^3$ arcs and closed walks of at most $n$ arcs. It gives the mathematical statement that must hold before the paper's proposed parallel calculation can be trusted. It also applies when several different decisions have the same endpoints, because each decision remains a separate weighted arc. Papadimitriou and Tsitsiklis (1987), pp. 445, 447

The paper proves the result informally and states the NC classification. The mission seeks machine-checked proofs of the graph and cost statements, including the printed argument's delicate boundary cases. The local proposal contains open Lean theorem statements, not proofs. Reusable outcomes include a decision-walk representation, a cycle decomposition that preserves the multiset of arcs, and finite-horizon policy-to-walk equivalence. A related published result, TropicalLA.exists_repeat, detects repetition for dense max-plus matrices; it does not state this weighted multigraph decomposition or the min-cost identity.

Difficulty

The obstacle is preserving both walk feasibility and the exact number of arcs when repeated cycles are rearranged. A cycle may be the only connection to other parts of a walk, so deleting its last copy can invalidate the remaining sequence. The printed exchange paragraph also reverses the cost-improving direction and appeals to a no-ties perturbation without carrying it through the bounded-prefix conclusion. Those issues affect the claimed $n^3$ bound; merely knowing that a long walk repeats a vertex does not establish the target identity. Papadimitriou and Tsitsiklis (1987), p. 447

Formalization scope

Lean represents $S$ and each $D_s$ as finite types and uses real costs. The decision sets are nonempty, making policies and arbitrarily long walks available. Policies depend on state and time, as in §2. A walk stores its decisions as well as its states, so loops and parallel arcs are represented. Cycle decompositions preserve endpoints, length, cost, and the multiset of decision arcs. A loop is a simple cycle of length one. Time starts at zero, and an $l$-arc walk has states at indices $0,\ldots,l$.

The paper's general finite-horizon definition sums costs from $0$ through $T$, while the Theorem 5 paragraph explicitly asks for a $T$-arc walk. This mission follows the latter convention: decisions occur at $0,\ldots,T-1$. The goal also imposes $l\le T$, which the printed loop leaves implicit, and uses a closed walk for $r_{k,u}$ because that is what the length-$k$ graph calculation computes. It does not assume distinct walk costs. The condition $T>n^2$ is retained from the paper even though related identities may hold in other ranges. Papadimitriou and Tsitsiklis (1987), pp. 444, 447

Theorem 5's NC membership, processor and parallel-time bounds, the membership-in-P discussion, log-space reductions, PSPACE membership, and Corollaries 1–2 are outside this mission. Mathlib does not supply the PRAM and complexity-class framework those claims require. The target is the exact cost identity behind the algorithm. Defining the optimum directly as the right-hand minimum, restricting policies to stationary policies, or allowing an empty policy class would trivialize or change it. Contributions proving the milestones, the goal, or reusable walk and cycle facts are welcome.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. DOI: 10.1287/moor.12.3.441

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