Operations Research

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

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

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

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$,

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$,

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

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

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

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:

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 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

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 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

The goal is the paper's Theorem 3:

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

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

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.