The OR Formalization Drive

Why semi-Markov control matters

A decision maker may choose an action whenever a system changes state, even though the time until the next change is random. Maintenance and replacement decisions are examples: a repair choice changes both the next operating state and the length of time before another choice is available. A discrete-time Markov decision model gives every decision epoch the same duration. A semi-Markov decision process allows the holding time to depend on the current state, action, and next state. Kallenberg's Chapter 7 develops discounted and average-reward versions of this finite-state model, including a characterization of optimal discounted value through inequalities and a linear program (Kallenberg 1983, Chapter 7).

The mission focuses on the discounted part of that chapter. The result is known: Kallenberg proves it as Theorem 7.2.1. The formalization task is to state and eventually prove the result for the same policy class and the same general holding-time distributions. Those details matter because a stationary-policy-only version would omit the comparison that the theorem makes with all admissible policies.

Model and notation

Let $E$ be a nonempty finite state set. Each $i\in E$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is chosen, the next state is $j$ with probability $p_{iaj}\geq0$, with $\sum_jp_{iaj}=1$. Conditional on $j$, the nonnegative time until that transition has distribution $F_{iaj}$. The action earns a lump reward $r_{ia}$ immediately and a reward rate $s_{ia}$ during the ensuing sojourn. Neither the holding-time laws nor the reward rates are required to be identical across transitions (Kallenberg 1983, pp. 210–212).

Fix a positive continuous discount rate $\lambda$. The factor applied after elapsed time $t$ is $e^{-\lambda t}$. Assumption 7.2.1 requires the Laplace–Stieltjes transform of each conditional holding-time law to satisfy

$$L_{iaj}(\lambda):=\int_0^\infty e^{-\lambda t}\,dF_{iaj}(t)<1 \qquad(i,j\in E,\ a\in A(i)).$$

The assumption is strict for every triple; it does not require a particular parametric family. Define the one-epoch expected discounted reward and discounted transition entry by

$$r^*_{ia}=\sum_jp_{iaj}\int_0^\infty \left(r_{ia}+s_{ia}\int_0^t e^{-\lambda u}\,du\right)dF_{iaj}(t), \qquad p^*_{iaj}=p_{iaj}L_{iaj}(\lambda).$$

A policy $R$ is a sequence of randomized decisions. At each epoch its choice may depend on every previously observed state and chosen action and the current state. It does not observe previous sojourn times when choosing. Let $v_i^\lambda(R)$ be the expected sum of discounted lump and rate rewards from initial state $i$, as in equation (7.2.1). The DRD value vector is $v_i^\lambda=\sup_R v_i^\lambda(R)$, with the supremum over this full policy class. A real vector $w$ is DRD-superharmonic when

$$w_i\geq r^*_{ia}+\sum_jp^*_{iaj}w_j \qquad(i\in E,\ a\in A(i)).$$

These are Kallenberg's Definitions 7.2.1 and 7.2.2 (p. 214).

Formalization targets

Goal: the smallest superharmonic vector

Theorem 7.2.1 states that the value vector itself satisfies the superharmonic inequalities and lies below every other vector satisfying them:

$$v^\lambda\text{ is DRD-superharmonic},\qquad w\text{ is DRD-superharmonic}\Longrightarrow v_i^\lambda\leq w_i\quad(i\in E).$$

This is the mission goal. Its content includes both clauses: merely showing that every superharmonic vector bounds policy rewards would leave out the assertion that the value is superharmonic.

Supporting results

Lemma 7.2.1 expresses $v_i^\lambda(R)$ as a sum of expected discounted state-action occupancies. Theorem 7.2.2 says that a feasible action choice attaining equality in the value equation at every state yields an optimal pure stationary policy. Theorem 7.2.3 says that positive support in an optimal solution of the dual linear program (7.2.11) yields such a policy. Their statements and exact conditions are the mission's milestones (Kallenberg 1983, pp. 212, 216–217).

What the results provide

The goal turns a supremum over possibly history-dependent randomized policies into a finite system of inequalities indexed by available state-action pairs. The next two results explain how equality in those inequalities and an optimal linear-programming solution identify a pure stationary policy with the same value. Thus the finite programs are statements about the original semi-Markov process rather than a separate discounted matrix model (Kallenberg 1983, pp. 214–217).

Kallenberg supplies paper proofs. This mission supplies Lean statements and a shared model interface; the proposed theorem items still require machine-checked proofs. The model's arbitrary conditional holding-time measures, its distinction between the current reward and future discounted value, and its history-dependent policy class are reusable for other finite semi-Markov arguments. The average-reward section of Chapter 7 is outside this mission.

Main difficulty

The straightforward finite-state discounted equation concerns expected one-step rewards. The source value, however, is defined from rewards earned at random physical times, and a policy can react to its entire discrete history. Identifying these two descriptions requires accounting for the joint state, action, and elapsed-time law without giving the policy access to past holding times. Holding times may equal zero with positive probability; the strict transform assumption excludes a degenerate law concentrated entirely at zero, but it does not make each holding time strictly positive. A second issue is real-valuedness: all-policy suprema and integrals must represent the finite quantities in the source rather than Lean's default values on ill-posed inputs.

Formalization scope

Lean uses finite types for states and actions, with a nonempty available-action finset for each state. Conditional sojourn laws are probability measures on $\mathbb R$ with no mass on negative times. This includes arbitrary distributions on $[0,\infty)$ and permits an atom at zero. The model stores stochastic transition rows, lump rewards, and rate rewards. The discounted layer stores $\lambda>0$ and the source's strict per-triple transform inequality. The expected one-epoch reward uses a Lebesgue integral against each sojourn law.

Policy decision rules read a list of past state-action pairs and the current state. Finite-horizon value recursively integrates the original epoch reward and its holding-time discount; policy value is its limit. The coordinatewise supremum ranges over all such policies. The occupation sum of Lemma 7.2.1 is a separate theorem, not the definition of policy value. A proof must establish convergence and boundedness from Assumption 7.2.1 so that Lean's total limit, integral, and real-supremum operations have their intended meanings.

The dual program sums only over actions available in each state and uses strictly positive weights $\beta_j$, equality flow constraints, and nonnegative variables as printed. Its pure stationary selector must choose an available action with positive dual mass in every state. Contributions establishing the occupation identity, value bounds, Bellman inequalities, or dual decoding all fit the mission.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 7, pp. 210–227. Publisher repository.

Motivation

Every pure integer program, once its linear programming relaxation has been solved, can be relaxed further to a problem over a finite Abelian group: the nonbasic variables must satisfy a single congruence in the group of the optimal basis. R. E. Gomory introduced this relaxation in 1965 and studied the convex hull of its solutions in Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969), 451–558, doi:10.1016/0024-3795(69)90017-2). The facets of these group polyhedra are valid inequalities for every integer program whose basis produces the same group, and they became the source of cutting planes for integer programming: Gomory's mixed-integer cut and the later theory of corner polyhedra and subadditive valid inequalities descend from them.

The number of facets grows fast with the order of the group, so a list of facets for each group is not a usable description. Section 3D of the paper, "Lifting up Faces", gives a structural tool instead: facets of the polyhedron of a small group produce facets of the polyhedron of every larger group that maps onto it. This mission formalizes that construction (THEOREM 19) and its converse (THEOREM 20).

Setting

Let $\mathcal G$ be a finite Abelian group, written additively, with zero $\bar 0$ and order $D=|\mathcal G|$, and let $\mathcal G^+=\mathcal G-\{\bar 0\}$. For a right-hand side $g_0\in\mathcal G$, the group equation asks for nonnegative integers $t(g)$, $g\in\mathcal G^+$, with

$$\sum_{g\in\mathcal G^+}t(g)\cdot g=g_0 .$$

Its solution set is $T(\mathcal G,g_0)$; when $g_0=\bar 0$, the zero solution is excluded, as stipulated on p. 474. Each solution is a point of $\mathbb R^{\mathcal G^+}$, a space of dimension $n'=D-1$, and the master polyhedron $P(\mathcal G,g_0)$ is the convex hull of $T(\mathcal G,g_0)$. Gomory reads a solution $t$ as a path from $\bar 0$ to $g_0$ that uses the element $g$ exactly $t(g)$ times; with arc lengths $\pi(g)$ its length is $\pi\cdot t=\sum_g\pi(g)t(g)$.

An inequality $\pi\cdot t\ge\pi_0$, written $(\pi,\pi_0)$, is a face of $P(\mathcal G,g_0)$ when $\pi\ne0$, every $t\in T(\mathcal G,g_0)$ satisfies it, and the solutions on the hyperplane $\pi\cdot t=\pi_0$ generate that hyperplane: every point of it is a weighted sum, with total weight 1, of such solutions. A face is therefore a facet; Gomory says "face" throughout, and so does this mission. The solutions with $\pi\cdot t=\pi_0$ are the minimal paths.

Let $\psi$ be a homomorphism of $\mathcal G$ onto a second finite Abelian group $\mathcal H$, with kernel $\mathcal K=\psi^{-1}(\bar 0)$. A coefficient vector $\pi'$ on $\mathcal H^+$ is lifted to $\mathcal G^+$ by

$$\pi(g)=\pi'(\psi g),\qquad \pi'(\bar 0)=0,$$

so that every element of the kernel gets coefficient $0$.

Formalization targets

Goal: THEOREM 19 (p. 486)

If $\psi g_0\ne\bar 0$ and $(\pi',\pi_0)$ is a face of $P(\mathcal H,\psi g_0)$ with $\pi_0>0$, then

$$\Big(\pi,\pi_0\Big),\quad \pi(g)=\pi'(\psi g),\quad\text{is a face of } P(\mathcal G,g_0).$$

For instance, the face $t_1\ge1$ of $P(\mathcal G_2,(1))$ lifts through reduction mod 2 to the face $t_1+0t_2+t_3+0t_4+t_5\ge1$ of $P(\mathcal G_6,(5))$ (p. 488).

Milestones

1. Face criterion (p. 469, proof of THEOREM 7). For $\pi_0>0$, $(\pi,\pi_0)$ is a face iff it is valid on $T$ and $n'$ linearly independent solutions satisfy $\pi\cdot t=\pi_0$.
2. Pushing paths forward (p. 486). A solution $t$ for $\mathcal G$ maps to the solution $\tau(h)=\sum_{g\in\psi^{-1}h}t(g)$ for $\mathcal H$ of the same length; hence the lifted inequality is valid.
3. Lifted minimal paths (p. 487). From a minimal path $\tau$ for $\mathcal H$ and a kernel element $k$, the path $T_k(\tau)$ is a minimal path for $\mathcal G$.
4. Rank $D-1$ (pp. 487–488). The lifted inequality has $D-1$ linearly independent minimal paths.

Further result: THEOREM 20 (p. 489)

Conversely, a face $(\pi,\pi_0)$ of $P(\mathcal G,g_0)$ with $\pi_0>0$ and $\pi(g)=0$ for some $g\ne\bar0$ is the lift of a face of $P(\mathcal H,\psi g_0)$ for some $\psi$ of $\mathcal G$ onto a group $\mathcal H$ with $\psi g=\bar 0$.

Significance

THEOREMS 19 and 20 together say that the faces of $P(\mathcal G,g_0)$ with $\pi_0>0$ and a zero coefficient are exactly the faces lifted from proper quotients of $\mathcal G$. A catalogue of these positive-right-hand-side faces therefore only needs the faces with all coefficients positive; the rest come from smaller groups. Gomory uses this to explain the tables of Appendix 5: for $\mathcal G_{2,2}$ and $\mathcal G_{2,2,2}$ every such face is a lift of the single nontrivial face of $P(\mathcal G_2,(1))$, and for a direct sum $\mathcal G=\mathcal K_1\oplus\mathcal K_2$ every face of the polyhedron of a summand not containing $g_0$ extends to a face for $\mathcal G$ (p. 489). The same idea, sending facets of one group problem to facets of another by a homomorphism, recurs in the later theory of group relaxations and infinite group problems.

Both theorems are proved in the paper. To the knowledge of this mission, neither the group polyhedra, their faces nor the lifting theorem has a machine-checked formalization; the platform's other "lifting" results (lifted cover facets of the knapsack polytope, cone lifts of convex sets) are different notions. The mission produces a reusable definition layer for master group polyhedra and their faces, stated once for an arbitrary finite Abelian group, and a formal version of the passage between faces of a group and of its quotients.

Difficulty

Validity of the lifted inequality is a one-line computation (milestone 2). The content is that the lift is a facet: one must exhibit $D-1$ affinely independent solutions on the hyperplane, while the quotient face only supplies $|\mathcal H|-1$ of them. A solution of the quotient problem does not determine a solution for $\mathcal G$; coset representatives must be chosen and the path closed by a kernel element, and the kernel coordinates, which all have coefficient zero, must still be filled to full rank.

The obvious reduction, "a facet pulls back to a facet under a surjective map", fails here because the map from $\mathcal G$-paths to $\mathcal H$-paths is a linear projection from dimension $D-1$ to $|\mathcal H|-1$ and does not lift independence by itself. It also fails at $\pi_0=0$: with $\mathcal G=\mathbb Z_6$, $\mathcal H=\mathbb Z_3$, $g_0=1$, the face $t(1)\ge0$ of $P(\mathbb Z_3,(1))$ lifts to $t(1)+t(4)\ge0$, which is valid but not a face of $P(\mathbb Z_6,(1))$.

Formalization scope

The formalization uses one definition file for an arbitrary finite Abelian group ([AddCommGroup G] [Fintype G] [DecidableEq G]), instantiated at both $\mathcal G$ and $\mathcal H$. It commits to the following readings:

• Vectors are indexed by the subtype $\{g\mid g\ne\bar0\}$, so $\bar0$ has no coordinate and the dimension of T-space is $|\mathcal G|-1$ for each group separately; solutions are $\mathbb N$-valued, nonzero, and cast to $\mathbb R$. When $g_0\ne\bar0$, the group equation already excludes the zero vector.
• "Generated by the points on the hyperplane" means that the affine span of the tight solutions equals the hyperplane $\{x:\pi\cdot x=\pi_0\}$; $\pi\ne0$ is part of the definition and $\pi_0\ge0$ is not (THEOREM 6 proves it).
• Paths are vectors and "minimal path" means a solution with $\pi\cdot t=\pi_0$.
• $\pi'(\bar0)=0$ is built into the lift; "onto" is Function.Surjective ψ, and $g_0\notin\mathcal K$ is $\psi g_0\ne\bar0$.
• Added hypothesis $\pi_0>0$ in THEOREM 19 and the rank milestone: the page omits it, and the $\mathbb Z_6\to\mathbb Z_3$ example above shows the statement is false without it.
• The face criterion is THEOREM 7's "basic feasible solution" unfolded into $n'$ linearly independent tight solutions, stated for the master polyhedron only and for nontrivial groups, where $n'>0$.
• Pushing a path forward uses $\psi g_0\ne\bar0$, the standing hypothesis of THEOREM 19, so the pushed path cannot become the excluded zero solution.
• The lifted path $T_k(\tau)$ puts its closing $1$ on the kernel element $g_0-\sum_{g\notin\mathcal K}t_k(g)\cdot g$ itself, and adds nothing when that element is $\bar0$.
• In THEOREM 20, "nontrivial" is $\pi_0>0$, the printed $(\pi_1,\pi_0)$ is read as $(\pi,\pi_0)$, and the conclusion requires $\psi g=\bar0$ for the given zero coefficient: without it the identity map would satisfy the statement.

A formalization that proves only validity of the lift, or that defines faces without the generation condition (so that every valid inequality is a "face"), would be trivial and is ruled out by the definition of IsFace.

The development needs finite sums over fibres of $\psi$, a choice of coset representatives, and a rank argument for a block matrix with full-rank diagonal blocks. The definitions of $T$, $P(\mathcal G,g_0)$ and face are reusable for any further result on master group polyhedra. Proofs of the milestones in any order, alternative proofs of the face criterion, and a proof of THEOREM 20 are welcome.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. doi:10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proceedings of the National Academy of Sciences 53 (1965), 260–265. doi:10.1073/pnas.53.2.260
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. doi:10.1007/BF01584976

Motivation

A finite Markov decision system asks how to choose actions while a changing state controls which actions are available. The choice can affect both the reward now and the distribution of future states. In a total-reward problem, the process can continue indefinitely; if transitions are substochastic, it can also terminate. Kallenberg's treatment of positive dynamic programming connects this control problem to a finite linear program and uses an optimal flow to identify a policy that is optimal from every initial state Kallenberg, Chapter 3.

The connection matters when an optimizer is easier to compute as state-action frequencies than as an infinite sequence of decisions. A policy may depend on the entire observed history and may randomize at every decision. The theorem under study says that, when the dual linear program has an extreme optimal solution, its positive coordinates identify a pure stationary policy as good as every such general policy. This assertion includes models in which the selected policy is not transient Kallenberg, Theorem 3.5.2 and Example 3.5.1.

Setting

Let $E=\{1,\ldots,N\}$ be a nonempty finite state space. At state $i$, one chooses an action from the nonempty finite set $A(i)$. Action $a\in A(i)$ earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}\ge0$. The sum $\sum_jp_{iaj}$ is at most one; any missing probability represents termination. Positive dynamic programming imposes $r_{ia}\ge0$ for every admissible state-action pair Kallenberg, Section 2.2 and Assumption 3.5.1.

A policy $R=(\pi^1,\pi^2,\ldots)$ assigns an action distribution after each finite history. The history records the initial state and all states and actions observed so far. Write $C$ for this full policy class. A pure stationary policy $f^\infty$ always chooses one fixed admissible action $f(i)$ whenever it visits $i$.

Starting from state $i$, let $v_i(R)$ be the expected total reward of $R$, and let $v_i=\sup_{R\in C}v_i(R)$. Because the rewards are nonnegative, the finite-horizon expected totals increase to $v_i(R)$; both policy and optimal values may be $+\infty$. A real vector $w=(w_i)$ is TMD superharmonic if $w_i\ge r_{ia}+\sum_jp_{iaj}w_j$ for each $i$ and $a\in A(i)$ Kallenberg, Definition 3.3.1.

For given weights $\beta_j>0$, equation (3.5.2) is a linear program over nonnegative state-action flows $x_{ia}$. It maximizes $\sum_{i,a}r_{ia}x_{ia}$ subject to

$$\sum_{a\in A(j)}x_{ja}-\sum_{i\in E}\sum_{a\in A(i)}p_{iaj}x_{ia}\le\beta_j\qquad(j\in E).$$

The set $E_x=\{i:\sum_{a\in A(i)}x_{ia}>0\}$ records the states with positive flow Kallenberg, Notation 3.1.1 and equation (3.5.2).

Formalization targets

Superharmonic value

Theorem 3.5.1 identifies $v$ as the smallest nonnegative TMD-superharmonic vector. The original superharmonic definition ranges over real vectors; the value must also be allowed to take $+\infty$. The formal statement gives both the extended superharmonic inequalities for $v$ and its componentwise bound by every nonnegative real superharmonic vector:

$$0\le v_i,\qquad v_i\ge r_{ia}+\sum_jp_{iaj}v_j,\qquad v_i\le w_i\quad\text{for every nonnegative real superharmonic }w.$$

This is the numbered milestone of the mission Kallenberg, Theorem 3.5.1.

Policy from an extreme optimal dual flow

The main goal is Theorem 3.5.2. Suppose $x^*$ is an extreme point of the feasible region of (3.5.2) and has objective at least as large as every feasible flow. Then every pure stationary rule $f$ choosing $x^*_{i,f(i)}>0$ on $E_{x^*}$, with arbitrary admissible actions outside $E_{x^*}$, is total optimal:

$$v_i(f^\infty)=v_i=\sup_{R\in C}v_i(R)\qquad(i\in E).$$

The goal records the finite-optimum case by requiring an actual optimal solution $x^*$; it makes no extra assumption that every policy is transient Kallenberg, Theorem 3.5.2.

Significance

The theorem converts an extreme optimal state-action flow into one decision rule that is optimal simultaneously for all starting states. Since $C$ includes policies that change with time, use full histories or randomize, it establishes that those freedoms cannot improve the total-reward value when the stated dual optimizer exists. The positive model also reveals when extended values matter: outside the finite-optimum case, the dual objective may be unbounded and an optimal total reward may be infinite Kallenberg, pp. 78–83.

A formal development of this result must keep the policy class and the linear program in the same model. It provides reusable definitions of a finite substochastic control system, finite-history probabilities, extended total rewards, state-action flows and superharmonic vectors. The result is proved in the book; the mission asks for a machine-checked proof of its statement, not for a new optimization theorem. The draft statements are open goals until such proofs are supplied.

Difficulty

A finite linear program has finitely many variables, while the value compares a flow-derived rule with every infinite, history dependent policy. A comparison restricted to stationary or transient policies would miss the main assertion. The proof also has to treat zero-flow states: the dual solution does not prescribe an action there, yet the theorem permits every admissible choice. Finally, the superharmonic milestone permits an infinite value, while the linear program itself uses real coordinates. A development must connect those representations without turning an infinite reward into an arbitrary default real value.

Formalization scope

Lean represents states as Fin N with $N>0$, and each $A(i)$ as a nonempty finite subset of a finite action type. The transition rows sum to at most one. Histories carry past states and actions, and the first action has internal index zero, corresponding to the book's time one. Policy probabilities are nonnegative, vanish outside $A(i)$ and sum to one. The expected reward of a finite horizon is a finite sum over histories; nonnegative total reward is its supremum in EReal. The value takes the supremum over the full policy type, not over a restricted policy subclass.

Dual flow coordinates exist only for admissible state-action pairs. Extreme points are taken in the feasible set of (3.5.2) in those coordinates, and its balance constraints retain the source's $\le\beta_j$ direction. The goal quantifies over every admissible pure rule satisfying the positive-flow condition. These choices exclude the vacuous shortcut of defining the value using only pure stationary policies or assuming optimality as a hypothesis.

The mathematical infrastructure includes finite policy histories, state-action occupancy probabilities, extended nonnegative reward limits, the real flow polyhedron and its extreme points. The history and flow definitions can support later work on other finite decision models. Contributions to those foundational results and to the full comparison with history dependent policies are within the mission's scope. The negative-reward regime of Section 3.6, whose claims involve average optimality and recurrent classes in an extended stochastic model, requires its own representation and is outside this positive-reward target.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository.

Motivation

Shop scheduling asks how to process a set of jobs, each a sequence of tasks on prescribed machines, so that all work is completed as early as possible. The flow shop, in which every job visits the machines in the same order, is the most studied of these models in operations research. For two machines, Johnson's rule (1954) computes a schedule of minimum finish time in $O(n\log n)$ time, and for two machines allowing interruptions (preemption) does not help. Garey, Johnson and Sethi (Math. Oper. Res. 1976) and Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum report BW 43/75, 1975; Ann. Discrete Math. 1977) showed that the non-preemptive problem becomes NP-complete with three machines.

Gonzalez and Sahni (Operations Research, 1978) extended this picture to preemptive schedules. Their Theorem 1 shows that minimizing the finish time of a three-machine flow shop is NP-complete with or without preemption, even when every job has at most two tasks of nonzero length. When every job has only one task the problem is trivial, so this is the simplest NP-complete case of the flow-shop finish-time problem. The result explains why no exact polynomial algorithm is expected and motivates the approximation results in the second half of the same paper.

Timeline:

• 1954: Johnson, two-machine flow shop, optimal non-preemptive rule.
• 1975: Brucker, Lenstra, Rinnooy Kan: non-preemptive three-machine flow shop NP-complete, including the case of two nonzero tasks per job (the paper's Corollary 1, which it says "is also obtained in [1]").
• 1976: Garey, Johnson, Sethi: non-preemptive three-machine flow shop NP-complete even when the problem size is the sum of the task lengths.
• 1978: Gonzalez, Sahni: the preemptive three-machine flow shop is NP-complete, by a reduction from PARTITION that also covers the non-preemptive case with two nonzero tasks per job.

Setting

A flow shop has $m\ge1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ must be processed on $P_j$ for $t_{j,i}\ge 0$ time units, and it can start only after task $j-1$ of the same job is completed. Task times may be zero. The schedule starts at time $0$.

A preemptive schedule gives every task a finite set of pieces $(s,f)$ with $0\le s<f$: the task is processed on its processor during $[s,f)$. Pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$, and every piece of a task starts after every piece of the earlier tasks of the same job has ended. A non-preemptive schedule processes every task in at most one piece. For a schedule $S$, $f_i(S)$ is the time at which job $i$ is completed and the finish time is $\mathrm{FT}(S)=\max_i f_i(S)$.

PARTITION. A multiset $S=\{a_1,\dots,a_n\}$ of nonnegative integers has a partition if some set $u$ of indices satisfies $\sum_{i\in u}a_i=\tfrac12\sum_{i=1}^n a_i$.

The instance FS. With $T=\sum_i a_i$, the flow shop $\mathrm{FS}$ has $m=3$ processors and $n+2$ jobs:

$$t_{\cdot,i}=(a_i,0,a_i)\ (1\le i\le n),\qquad t_{\cdot,n+1}=(T/2,\,T,\,0),\qquad t_{\cdot,n+2}=(0,\,T,\,T/2),$$

and the threshold is $\tau=2T$. Every job has at most two nonzero tasks.

Formalization targets

Goal: Theorem 1 (p. 38)

For every $n$ and every $a_1,\dots,a_n\in\mathbb N$:

$$\mathrm{FS}\ \text{has at most two nonzero tasks per job},$$ $$\big(\exists\,S'\ \text{preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition},$$ $$\big(\exists\,S'\ \text{non-preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition}.$$

Milestones

• Lemma 1(a) (p. 39): a partition of $S$ yields a non-preemptive schedule of FS with $\mathrm{FT}=2T$ (Figure 1).
• Observations (i)–(ii) (p. 39): in any preemptive schedule with $\mathrm{FT}\le 2T$, task $t_{1,n+1}$ ends by $T$ and task $t_{3,n+2}$ starts no earlier than $T$.
• Lemma 1(b) (p. 39): if $S$ has no partition, every preemptive schedule of FS has $\mathrm{FT}>2T$.
• Lemma 1 (p. 38): the preemptive equivalence.
• Corollary 1 (p. 39): the non-preemptive equivalence.

Significance

The result. The equivalence shows that a polynomial-time algorithm deciding whether a three-machine flow shop (with two nonzero tasks per job) has a schedule of finish time at most $\tau$, preemptive or not, would decide PARTITION in polynomial time. With membership in NP (the paper's Lemma 2) it gives NP-completeness of both versions. It also marks the boundary with the polynomial cases: $m=2$ (Johnson's rule), and jobs with a single task.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no machine-checked proof of this reduction exists, and the platform has no formal model of preemptive shop schedules. The mission produces one: a piece-based preemptive schedule with zero task times, which subsumes the non-preemptive case, together with the first formal NP-hardness reduction for preemptive flow shops on the platform.

Difficulty

Direction (a) asks for one explicit schedule. Direction (b) must rule out every preemptive schedule of FS, and preemption is exactly what makes this delicate: a task may be split into any finite number of pieces placed anywhere on its processor, so the naive intuition that a failed partition leaves "unusable gaps" is no longer evident, since pieces of different jobs can be interleaved to fill gaps. A correct argument must therefore be an accounting of processor time over the pieces, valid for any number and position of pieces, and it must treat zero-length tasks, which occupy no processor time but still delay the next task of their job. Finally, the non-preemptive equivalence is not a formal consequence of the preemptive one alone: it uses that (a) produces a non-preemptive schedule and that (b) holds for all preemptive schedules, which include the non-preemptive ones.

Formalization scope

• Processors are Fin 3 ($P_1,P_2,P_3$ = 0, 1, 2), jobs of FS are Fin n ⊕ Fin 2 (Sum.inr 0 is job $n+1$, Sum.inr 1 is job $n+2$). Task times are real numbers; the PARTITION data are a : Fin n → ℕ, and "has a partition" is $2\sum_{i\in u}a_i=\sum_i a_i$ in $\mathbb N$.
• A schedule is a Finset of pieces $(s,f)$ per task with the four conditions of the Setting. Non-preemptive means at most one piece per task. Zero tasks have no pieces and occupy no processor time. $f_i(S)$ and $\mathrm{FT}(S)$ are maxima with baseline $0$.
• Explicit constants: $T=\sum_i a_i$, the times $T/2$ and $T$ of jobs $n+1,n+2$, and the threshold $\tau=2T$, as on p. 39. Lemma 1(a) states finish time exactly $2T$, as the paper does.
• Not formalized: "NP-complete", the reducibility relation "$\alpha$", membership in NP (Lemma 2, p. 40) and the polynomial computability of FS from $S$. The paper states Theorem 1, Lemma 1 and Corollary 1 as complexity claims. Their proofs establish the equivalences above for the constructed instance, and those equivalences are what is formalized.
• No trivializing reading is admitted: the statements concern the specific instance FS built from $a$, not an arbitrary flow shop, and the schedule model rules out overlapping pieces and out-of-order tasks while still allowing zero tasks. A sorry-free check confirms that Figure 1 is a valid non-preemptive schedule of FS for $S=\{1,1\}$.
• Reusable beyond this mission: the flow-shop model with preemptive pieces, and PARTITION. Proofs of the milestones and a proof of the goal from them are welcome.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum report BW 43/75, 1975; Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

In a job shop, each job has an ordered list of tasks, and each task must use a specified machine. A production planner may be able to interrupt a task and resume it later, yet still be unable to find a short schedule efficiently. Gonzalez and Sahni studied how the ability to preempt changes the difficulty of minimizing the time at which all jobs are complete. Their 1978 paper establishes complexity results for flow shops and job shops and then examines approximation schedules when exact optimization is difficult (Gonzalez and Sahni, 1978).

This mission concerns the paper's two-machine construction from 3-PARTITION. It is the reduction used for their claim that finding an optimal preemptive or non-preemptive finish-time schedule remains NP-complete when input size is measured by the sum of task lengths. The formal target isolates the decision equivalence proved for the constructed instance. It gives solvers a precise schedule statement to establish without conflating the scheduling theorem with the separate complexity-class argument.

Setting

A 3-PARTITION input $C$ comprises an integer $t\ge0$, a positive integer target $B$, and $s=3t$ positive integer sizes $a_1,\ldots,a_s$. A valid input satisfies

$$\sum_{i=1}^{s}a_i=tB,\qquad B/4<a_i<B/2\quad(1\le i\le s).$$

It has a 3-partition when the $s$ indices can be assigned to $t$ disjoint groups, each containing exactly three indices and having total size $B$. The strict bounds rule out groups of other cardinalities at that sum and are part of the source problem, not a convenience added for formalization. When $t=0$, the input has no sizes or groups and the empty grouping is a solution.

The paper builds a job shop $JS(C)$ with machines $P_1,P_2$ and $s+1$ jobs. For $1\le i\le s$, job $i$ has a task of length $a_i$ on $P_1$, followed by a task of length $a_i$ on $P_2$. The last job, $s+1$, has $2t$ tasks, each of length $B$. Its tasks alternate between the machines, starting on $P_2$. This last order matters: reversing it would produce a different construction. The source gives the decision threshold $\tau=2tB$ (Lemma 7, p. 44).

A non-preemptive schedule gives each task one continuous processing interval. A preemptive schedule may divide an operation into finitely many positive-length intervals. In either case, jobs obey their task order, distinct pieces on the same machine do not overlap, and processing starts at or after time zero. Write $FT(S)$ for the time at which all tasks of schedule $S$ have finished. The paper allows the same job to revisit a machine, as the final job does here.

Formalization targets

Lemma 7: the constructed instance

For every valid $C$, the main goal states both the paper's preemptive equivalence and the non-preemptive form established by its two directions:

$$\begin{aligned} \exists S\text{ preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition},\\ \exists S\text{ non-preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition}. \end{aligned}$$

The milestones follow the source's proof text: the schedule supplied by a solution in Lemma 7(a), the timing forced on the final job, the exclusion of short preemptive schedules in Lemma 7(b), and the preemptive equivalence stated in the proof. The final-job milestone describes the occupied time slots of the paper's Figure 4, independently of how many adjacent pieces a formal schedule uses.

Significance

The equivalence transfers the distinction between solvable and unsolvable 3-PARTITION inputs to an exact finish-time threshold in a job shop with only two machines. It also establishes the non-preemptive decision equivalence for this construction, because a solution yields a non-preemptive schedule while an unsolvable input rules out even the more permissive preemptive schedules. These facts supply the scheduling part of the paper's strong NP-completeness claim; membership in NP is handled separately by Lemma 6 (pp. 44–45).

The result is proved in the source paper. The work proposed here is a machine-checked development of its explicit reduction equivalence and the finite-piece scheduling model needed to state it. The milestone theorems expose statements that can be reused when formalizing other preemptive scheduling reductions. The shared job-shop instance and 3-PARTITION input are already published definitions; the particular reduction instance and preemptive schedule predicate are new local definitions.

Difficulty

Preemption makes a task's processing time distributable across intervals. Merely checking that each machine has enough total capacity does not characterize feasible schedules: every job's operations must still occur in order, and pieces of different jobs must avoid one another on each machine. The converse direction must constrain every preemptive schedule that meets the threshold, not only a schedule having the visual pattern in Figure 4. A schedule can also represent one uninterrupted interval as several adjacent pieces, so piece count alone cannot express the source's timing claim.

Formalization scope

Machines are Fin 2, with $P_1$ numbered $0$ and $P_2$ numbered $1$. Jobs are Fin (3t+1); the final job is index $3t$. Its zero-based operation $i$ uses machine $1$ for even $i$ and machine $0$ for odd $i$. The definition uses the published JobShopLTAS.Core.Instance for ordered operations, machines, real processing times, and non-preemptive feasibility. It uses the published ResourceScheduling.Chain.ThreePartition for $t,B,a_i$, validity, and solutions. Those objects have the same conventions as the paper here. The local preemptive model uses finitely many positive-length pieces per task, whose durations sum exactly to that task's processing time. The threshold is the explicit real cast of $2tB$; no real infimum or division by a possibly zero optimum appears.

The goal is specific to the instance the paper constructs from each valid input. A free job-shop instance, a freely chosen schedule, or an extra hypothesis that the input has a solution would erase the reduction's content. Validity carries $B>0$, total $tB$, and both strict bounds on each $a_i$. The case $t=0$ remains in scope: the constructed job has no tasks and its finish-time threshold is zero. All existing tasks have positive length whenever the input is valid, so the published non-preemptive predicate's treatment of zero-length tasks does not affect this mission.

The paper states “3-Partition $\alpha$ preemptive JOFT with $m=2$” and connects it to NP-completeness for preemptive and non-preemptive scheduling when complexity is measured by the sum of task lengths. The Lean theorem states the proof's two decision equivalences with constant $2tB$ and machine count $2$. It does not formalize $\alpha$ as a polynomial-time many-one reduction, the unary task-length measure, NP-completeness, or Lemma 6's NP-membership argument. Contributions that establish the reduction statements, the schedule construction, or general finite-piece scheduling facts are within scope.

Selected references

• Teofilo Gonzalez and Sartaj Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 1978, pp. 36–52. DOI: 10.1287/opre.26.1.36.

Motivation

Flow shops and job shops are the basic models of multi-stage production: every job passes through several machines, and each machine handles one task at a time. Gonzalez and Sahni (Operations Research 26(1), 1978) showed that minimizing the finish time of such shops is NP-complete even with preemption, and then asked how well simple heuristics do. One of the two objectives they study is the mean flow time, the average completion time of the jobs, which measures how long a job spends in the shop on average.

Their Lemma 9 analyses the most natural rule for that objective, shortest processing time first (SPT): process the jobs in order of nondecreasing total work. For a single machine SPT is optimal (Smith 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 76, which the paper cites). Lemma 9 shows that with $m$ processors the same rule loses at most a factor $m$, and the paper's Example 2 shows that the factor $m$ is attained in the limit.

Setting

A job shop has $m\ge1$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ is a finite sequence of tasks; each task names the processor that must process it and a processing time $p\ge0$. The tasks of a job are processed in their order: a task may start only after the job's previous task has completed. A flow shop is the special case in which every job has $m$ tasks and its $k$-th task runs on $P_k$.

A non-preemptive schedule gives every task a start time $s\ge0$; the task then occupies its processor during $[s,s+p)$, and two distinct tasks on one processor never overlap. The finish time $f_i(S)$ of job $i$ in schedule $S$ is the time at which all tasks of job $i$ have been completed, and the mean flow time is

$$\mathrm{MFT}(S)=\frac1n\sum_{i=1}^n f_i(S).$$

An OMFT schedule $S^*$ is a feasible schedule of least mean flow time.

Let $L_i$ be the sum of the task times of job $i$. An SPT order is a listing $\sigma(0),\dots,\sigma(n-1)$ of the jobs with $L_{\sigma(0)}\le\dots\le L_{\sigma(n-1)}$, ties broken arbitrarily. The SPT schedule processes the jobs in that order: each job in turn, each positive-time task starting at the later of the completion of the job's previous task and the latest completion of a task already placed on its processor. A zero-time task completes when its preceding task completes and leaves the processor available.

Formalization targets

Goal: Lemma 9

For every job shop, every SPT order $\sigma$ with SPT schedule $S$, and every feasible non-preemptive schedule $\tau$,

$$\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau),$$

so that $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ for an OMFT schedule $S^*$. A separate item states the same bound for flow shops.

Milestones

The milestones follow the paper's proof of Lemma 9 on p. 47:

1. the SPT schedule is a feasible schedule;
2. the job in position $k$ of the SPT schedule finishes by $\sum_{j\le k}L_{\sigma(j)}$;
3. in any feasible schedule, if $i_1,\dots,i_n$ is the order in which the jobs finish, then $f_{i_k}\ge\sum_{j\le k}L_{i_j}/m$;
4. a prefix sum of any listing of the $L_i$ is at least the corresponding prefix sum of the sorted listing;
5. $\mathrm{MFT}(S^*)\ge\frac1n\sum_{k=1}^n\sum_{j=1}^k L_j/m$.

Significance

Lemma 9 is one of the earliest performance guarantees for a shop-scheduling heuristic under a sum objective. It shows that a rule computable by one sort, $O(n\log n)$ plus a linear pass, is within a factor equal to the number of machines, independently of the number of jobs. This is better than the factor $n$ that Lemma 8 of the same paper gives for an arbitrary busy schedule, whenever $m<n$. Example 2 of the paper shows that the factor cannot be improved for SPT. Lower bounds of the work-per-machine type used here recur in later approximation results for total completion time in shops and on parallel machines.

The result has been proved since 1978. As far as a search of the Prove2Me catalogue shows, it has not been machine-checked. This mission adds a machine-checked statement of the SPT schedule as an algorithm, not as an arbitrary schedule with a property. It also adds the guarantee for job shops with arbitrary task sequences, of which flow shops are a special case.

Difficulty

The arithmetic of the proof is short. The work is in two places. The SPT schedule is a concrete construction, a fold over jobs and tasks that updates processor availability, so the bound on its finish times has to be carried through an invariant of that construction. The lower bound on every feasible schedule needs a packing argument: tasks on one processor that complete by a given time have total length at most that time. That argument is not available in Mathlib in a form that applies here. The tempting shortcut of comparing the two schedules job by job fails: the optimal schedule need not finish jobs in SPT order, so the comparison must go through sums of sorted prefixes.

Formalization scope

• Instance and feasibility. The job data come from the published JobShopLTAS.Core.Instance (jobs Fin n, processors Fin m, tasks Fin (μ j), real processing times $\ge0$). The local IsPaperFeasibleSchedule requires nonnegative starts, in-job order, and no overlap of positive-time tasks on the same processor. Zero-time tasks occupy no processor interval. The paper assumes $m\ge1$, and the scheduling theorems carry that hypothesis.
• Finish time and MFT. $f_i$ is the maximum completion time over the tasks of job $i$, with baseline $0$; MFT divides by $n$, and for $n=0$ both sides are $0$.
• The SPT schedule is the list schedule constructed by the heuristic, for every SPT order, so ties are broken in every possible way. Zero-time tasks do not advance processor availability. It is not "any feasible schedule whose jobs finish in SPT order", a reading under which an optimal schedule would qualify and the goal would be trivial.
• The optimum. The paper's "Let $S^*$ be an OMFT schedule" is stated as "for every feasible non-preemptive schedule $\tau$". This is equivalent and does not assume that an optimum exists.
• Ratios multiplied out. $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ is stated as $\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau)$, and the proof's bounds divided by $m$ are multiplied by $m$. No division by a possibly zero quantity occurs.
• Constants. The only constant is the factor $m$, the number of processors.
• Not formalized. The running time of SPT, the comparison with Lemma 8 and its remark "it is assumed that $m<n$" (not a hypothesis of Lemma 9), and the tightness Example 2.
• Milestones 2 and 4 are stated for every listing $\sigma$ and every pair of listings; they are combinatorial facts about list schedules and sorted sums that are reusable beyond this mission. Proofs of any milestone, and a reusable packing lemma for non-overlapping intervals, are welcome.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106
• K. Jansen, R. Solis-Oba, M. Sviridenko, Makespan Minimization in Job Shops: A Linear Time Approximation Scheme, SIAM J. Discrete Math. 16(2), 288–300, 2003 (source of the job-shop definition reused here). https://doi.org/10.1137/S0895480199363908