Linear Optimization

Graph Theory Theoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms III: Every Directed Uniform Multicommodity Flow Problem Has Ω(𝒮/log n) ≤ f ≤ 𝒮Research Paper

Motivation

Many graph problems in routing, VLSI layout and scheduling ask for a cut that separates a lot of demand while cutting little capacity. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest flow equals the smallest cut. For several commodities sharing one network this equality fails, and the question becomes how far apart the two quantities can be. Leighton and Rao (J. ACM 46 (1999), extending their FOCS 1988 paper) proved that for uniform demands the gap is at most logarithmic in the number of nodes, and turned the proof into approximation algorithms for a range of NP-hard cut problems.

Their §2.4 extends the result to directed networks, where every edge carries flow in one direction only. The directed version is the one behind their approximation algorithms for directed problems, most prominently the minimum feedback arc set problem (§3 of the paper), where the cut structure of a digraph, not of its underlying undirected graph, is what matters.

Timeline. Ford and Fulkerson (1956): max-flow = min-cut for one commodity. Hu (1963): equality for two commodities in undirected graphs. Shahrokhi and Matula (1990, circulated 1986): the uniform concurrent flow problem and its LP dual. Leighton and Rao (FOCS 1988; J. ACM 1999): $\Omega(\mathcal S/\log n)\le f\le\mathcal S$ for uniform and product demands, undirected and directed, tight up to the constant for undirected uniform problems. Klein, Rao, Agrawal and Ravi (1990s) and Linial, London and Rabinovich (1995) extended the undirected theorem to general demands with an $O(\log k)$ gap. For directed graphs with general demands the gap is polynomial in $n$ (Chuzhoy and Khanna 2009), so the uniform-demand directed theorem is the setting where a logarithmic gap holds.

Setting

A directed network is a finite vertex set $V$ with $n=|V|$ nodes and a capacity $C(u,v)\ge0$ for each ordered pair, with $C(u,u)=0$ ; there is an edge directed from $u$ to $v$ when $C(u,v)>0$ . For $U\subseteq V$ write $\bar U=V\setminus U$ and let $C(U,\bar U)=\sum_{u\in U,\,v\in\bar U}C(u,v)$ be the capacity of the edges directed from $U$ to $\bar U$ .

The directed uniform multicommodity flow problem (directed UMFP) has one commodity for every ordered pair $(u,v)$ with $u\ne v$ , each with demand $1$ . A concurrent flow of value $\lambda$ routes $\lambda$ units of every commodity simultaneously, each edge carrying flow only in its own direction, with total flow on the edge $u\to v$ at most $C(u,v)$ . The max-flow $f$ is the largest such $\lambda$ .

The ratio cost of a cut is $C(U,\bar U)/(|U|\,|\bar U|)$ , and the min-cut is

\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.

A distance function assigns a length $d(u,v)\ge0$ to each directed edge; $d(u,v)$ then also denotes the length of a shortest directed path from $u$ to $v$ , its total weight is $W=\sum_{u,v}C(u,v)\,d(u,v)$ , and the distance constraint is $\sum_{(u,v)\in V^2}d(u,v)\ge1$ . The sets $\mathcal N^\Delta_{\mathrm{in}}(v,G)$ and $\mathcal N^\Delta_{\mathrm{out}}(v,G)$ are the nodes from which $v$ can be reached, respectively which can be reached from $v$ , by a directed path of length at most $\Delta$ . Logarithms are to base $2$ .

In Lean these are DiNetwork, diCutCap, diRatio, diMinCut, diDemand, IsDiConcurrentFlow, diMaxFlow, diDist, diTotalWeight, SatisfiesDiConstraint, inBall and outBall, in the namespace LeightonRao.Directed.

Formalization targets

Goal: Theorem 12 (p. 804)

There is an absolute constant $c>0$ such that every directed UMFP on $n\ge2$ nodes satisfies

c\,\frac{\mathcal S}{\log n}\le f\le\mathcal S.

The constant is left unfixed, as in the paper's $\Omega(\cdot)$ ; any improvement of the constant leaves the goal intact.

Milestones

Weak duality (p. 804): every concurrent flow of value $\lambda$ has $\lambda|U||\bar U|\le C(U,\bar U)$ for every proper cut.
LP duality (§2.2, p. 796, used for directed graphs in §2.4): every feasible distance function has $W\ge f$ , and an optimal one has $W=f$ .
Lemma 13 (p. 804): for every $\Delta>0$ , an ordered partition $V_1,\dots,V_r$ whose backward edges (from $V_i$ to $V_j$ , $j<i$ ) have capacity at most $8W\log n/\Delta$ , each part containing a node whose in- and out-balls of radius $\Delta$ are at least as large as the part.
Corollary 14 (p. 806): with $\Delta=1/4n^2$ , either a node whose in- and out-balls both have at least $2n/3$ nodes, or a directed cut of ratio cost at most $8W\log n/(\Delta(n/6)(5n/6))$ .
Lemma 15 (p. 806): a set $T$ with $|T|\ge2n/3$ and $\sum_{u\notin T}d(T,u)\ge1/4n$ or $\sum_{u\notin T}d(u,T)\ge1/4n$ gives a directed cut of ratio cost at most $12W$ .
Lemma 16 (p. 807): a distance function satisfying the distance constraint gives a directed cut of ratio cost at most $\tfrac{1152}{5}W\log n$ .

Significance

The result. Theorem 12 says that the directed sparsest cut and the directed uniform concurrent flow agree within an $O(\log n)$ factor. Since the flow is an LP, this gives an $O(\log n)$ -approximation for the directed uniform sparsest cut, and through divide and conquer, polylogarithmic approximations for directed problems such as minimum feedback arc set and minimum directed cut linear arrangement (§3 of the paper). It is also the case in which a logarithmic flow–cut gap survives for digraphs: with arbitrary demands, the directed gap is polynomial.

Formalizing it. The theorem has been proved since 1988, but no part of it is formalized: Mathlib has no multicommodity flows, no directed path metrics over real lengths, and no region-growing arguments. This mission produces the directed concurrent-flow model, its LP duality, and the directed region-growing decomposition of Lemma 13, each reusable beyond this paper (directed multicut, feedback arc set, low-diameter decompositions of digraphs).

Difficulty

The obvious route copies the undirected proof: grow a ball around a node until the capacity on its boundary is small compared with the capacity inside, cut it off, and repeat. In a digraph this fails at two places. A ball of small out-radius can have large in-radius, so a piece cut off by out-distances is not small in the sense needed later; and cutting off a piece only controls the edges leaving it in one direction, so edges pointing back into earlier pieces are not paid for. Lemma 13 has to bound the capacity of all backward edges of an ordered partition while keeping each part inside both an in-ball and an out-ball around one of its own nodes. The final averaging step also changes: the undirected argument sums $d(T,u)+d(T,v)$ over symmetric pairs, which has no directed counterpart, so the distance constraint over ordered pairs has to be split between distances into one set and out of another.

Formalization scope

Vertices form a Fintype with decidable equality, and every goal-level statement assumes $n\ge2$ . Commodities are ordered pairs with demand $1$ ; a flow is in arc form, $f_{st}(i,j)\ge0$ with conservation, and the capacity constraint is per directed edge. The max-flow is the supremum (sSup) of the achievable values $\lambda\ge0$ ; the min-cut is an infimum over nonempty proper subsets, since the ratio is $0/0$ otherwise. Shortest-path distances are infima over directed walks (lists of vertices along edges of positive capacity); for nonnegative lengths these equal shortest-path lengths. An unreachable pair would get Lean's junk value $0$ , so every statement using $d(u,v)$ assumes strong connectivity ( $C(U,\bar U)>0$ for every proper $U$ ), the directed analogue of the paper's standing assumption on p. 789; the balls are defined through the existence of a walk and need no such assumption. $W$ counts each directed edge once, and the distance constraint sums over ordered pairs. "We can find" is read as existence; running times are not formalized. The $\Omega$ of Theorem 12 is one absolute constant chosen before the network; the explicit constants $8$ , $1152/5$ and $12$ of the milestones are the ones computed in the paper's proofs.

Two printed slips are corrected and disclosed: Lemma 13 (1) prints $1\le j<i<r$ where the proof uses $i\le r$ , and the proof's last line prints $|\mathcal N^\Delta_{\mathrm{out}}(v,G)|\le|V_i|$ where the statement has $\ge$ .

The statement cannot be trivialized by a degenerate cut or flow: cuts range over nonempty proper subsets, the flow's capacity constraint is directional, and the goal's constant is quantified before the network, so a constant depending on $n$ does not count.

Needed infrastructure: LP duality for the concurrent flow LP (or a direct proof of the max-flow/distance duality), shortest directed paths with real lengths, and the region-growing bookkeeping. Contributions to any milestone are welcome, as are alternative proofs of Lemma 13 by continuous region growing.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
N. Linial, E. London and Yu. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
J. Chuzhoy and S. Khanna, Polynomial flow-cut gaps and hardness of directed cut problems, J. ACM 56(2):6, 2009. https://doi.org/10.1145/1502793.1502795

8 thms2 active usersReviewed

Graph Theory Theoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms II: Every Product Multicommodity Flow Problem with k Commodities Has Ω(𝒮/log k) ≤ f ≤ 𝒮Research Paper

Why multicommodity max-flow and min-cut

For a single commodity, the Ford–Fulkerson theorem says that the maximum flow between two nodes equals the minimum capacity of a cut separating them. Many routing and partitioning problems involve many source–sink pairs at once, and for those the equality fails: the largest fraction of every demand that can be routed simultaneously can be strictly smaller than the sparsest cut. Leighton and Rao (J. ACM 1999, building on their FOCS 1988 paper) proved that the gap is at most logarithmic for broad classes of demand patterns, and turned the proof into the first $O(\log n)$ -approximation algorithms for sparsest cut, balanced separators, minimum feedback arc set, crossing number and VLSI layout problems.

This mission formalizes Section 2.3 of the paper: the extension of the uniform max-flow min-cut theorem to product multicommodity flow problems (PMFPs), where the demand between two nodes is the product of their node weights.

Timeline.

1956: Ford and Fulkerson, single-commodity max-flow = min-cut.
1963: Hu, equality for two commodities.
1988: Leighton and Rao (FOCS), $\Theta(\log n)$ gap for uniform demands; the product-demand extension, pointed out to them by Shmoys, Tardos and Sinclair, appears in the journal version (1999), Theorem 7.
1993–1995: Klein–Agrawal–Ravi–Rao, Garg–Vazirani–Yannakakis, Linial–London–Rabinovich and Aumann–Rabani extend the $O(\log k)$ gap to arbitrary demands with $k$ commodities.

Setting

A network is a finite vertex set $V$ with a symmetric capacity $C(u,v)\ge0$ on each pair, zero on the diagonal; $\{u,v\}$ is an edge when $C(u,v)>0$ . For $U\subseteq V$ , the cut capacity is $C(U,\bar U)=\sum_{u\in U,\,v\notin U}C(u,v)$ . The network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$ .

A PMFP is given by a node weighting $\pi:V\to\mathbb R_{\ge0}$ . Write $\mathcal P$ for the set of nodes with $\pi(u)\ne0$ , $p=|\mathcal P|$ , and $\pi(U)=\sum_{u\in U}\pi(u)$ . As in the paper, the weights are normalized so that $\pi(V)=p$ . Every pair $\{u,v\}$ is a commodity with demand $\pi(u)\pi(v)$ ; there are $k=\binom p2$ commodities with nonzero demand. The uniform problem is $\pi\equiv1$ .

The max-flow $f$ is the largest $\lambda$ such that $\lambda\pi(u)\pi(v)$ units of every commodity can be routed simultaneously, with the total flow on each edge (both directions) at most its capacity. The min-cut is

\mathcal S=\min_{U:\ \pi(U)>0,\ \pi(\bar U)>0}\frac{C(U,\bar U)}{\pi(U)\,\pi(\bar U)},

the quotient being the weighted ratio cost of the cut $\langle U,\bar U\rangle$ .

The dual objects are distance functions: lengths $d(e)\ge0$ on the edges, with total weight $W=\sum_eC(e)d(e)$ ; $d(u,v)$ is the shortest-path distance and $d(T,u)=\min_{t\in T}d(t,u)$ . The weighted distance constraint is $\sum_{\{u,v\}\in\mathcal P^2}\pi(u)\pi(v)d(u,v)\ge1$ .

Formalization targets

Goal: Theorem 7 (pp. 801–802)

There is an absolute constant $c>0$ such that every normalized PMFP with $p\ge2$ on a connected network satisfies

\frac{c\,\mathcal S}{\log_2\max(k,2)}\le f\le\mathcal S .

The goal leaves the constant unfixed, which is the paper's $\Omega(\cdot)$ .

Milestones, in the order the proof uses them

Weak duality (§1.2, pp. 789–790): $f\,\pi(U)\pi(\bar U)\le C(U,\bar U)$ for every cut with positive weight on both sides.
LP duality for the PMFP (p. 802 with p. 796): distance functions satisfying the weighted constraint have $W\ge f$ , and one attains $W=f$ .
Lemma 8 (p. 802): a partition whose components meeting $\mathcal P$ have radius at most $\Delta$ and whose cross capacity is at most $4W\log p/\Delta$ .
Corollary 9 (p. 802): either a set $T$ of radius $1/2p^2$ with $\pi(T)\ge2p/3$ , or a cut of weighted ratio cost $O(W\log p)$ .
Lemma 10 (p. 802): a heavy set $T$ far on average from the remaining weight yields a cut of weighted ratio cost $O(W)$ .
Lemma 11 (p. 803): a distance function satisfying the weighted constraint yields a cut of weighted ratio cost $O(W\log p)$ .

Stronger companions

$\mathcal S\le36\log_2\max(k,2)\cdot f$ , the constant of the paper's proof.
Theorem 7 without the normalization $\pi(V)=p$ , which the paper assumes "without loss of generality".

Significance

Theorem 7 bounds the multicommodity flow–cut gap by $O(\log k)$ for every product demand pattern, so an optimal dual distance function certifies a cut within $O(\log k)$ of the sparsest weighted cut. The paper itself applies it to reversible Markov chains (§3.27, p. 827). There the node weights are the stationary probabilities, and Theorem 7 shows that the inverse conductance and the resistance of a chain agree up to a $\Theta(\log p)$ factor, where $p$ is the number of states with positive stationary probability.

Theorem 7 was proved in 1988–1999 and is subsumed, up to the constant, by the general $O(\log k)$ bound for arbitrary demands (Linial–London–Rabinovich 1995; Aumann–Rabani 1998). It has no machine-checked proof, and neither has any of its milestones. A complete development would also be the first formal treatment on Prove2Me of concurrent multicommodity flow, its LP dual, and region-growing (low-diameter) decompositions, which recur across approximation algorithms and metric embeddings.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the work. Rounding an optimal dual distance function to a cut fails directly: thresholding distances from a single node gives no control on the ratio when the weight is spread out. The paper's argument needs a decomposition of the graph into components of small radius that cuts little capacity, with a loss of only $\log p$ , not $\log n$ : the regions must be grown from weighted nodes only, while the many zero-weight nodes still sit inside the graph and its capacities. It must then separately handle the case where one component carries two thirds of the weight. Formally, the LP duality step alone requires a strong-duality statement for a linear program with one constraint per path, exponentially many, which Mathlib does not provide in this form.

Formalization scope

All objects live in the namespace LeightonRao.Product in a single definitions file.

Network and graph. A network is a symmetric nonnegative capacity function on a finite type with zero diagonal. The graph has an edge where the capacity is positive.
Commodities. One commodity per ordered pair $u\ne v$ , with demand $\tfrac12\pi(u)\pi(v)$ each way (the paper's footnote 7). The total demand of a pair is then $\pi(u)\pi(v)$ , and the demand separated by $U$ is $\pi(U)\pi(\bar U)$ .
Max-flow. Flows are arc flows per commodity. The max-flow is the supremum of the feasible values $\lambda\ge0$ .
Min-cut. The min-cut ranges only over cuts with $\pi(U)>0$ and $\pi(\bar U)>0$ . On the other cuts the paper's quotient is undefined; reading it with Lean's division by zero would make $\mathcal S=0$ and the goal trivial.
Distances, radius, cross capacity. Graph distances are infima of walk lengths. The radius of a component is measured by walks inside the component. Cross capacity is the capacity between different parts of a Finpartition.
Logarithms. $\log$ is $\log_2$ (the paper's footnote 3). For $p=2$ there is one commodity and $\log k=0$ , so the goal uses $\log_2\max(k,2)$ .
Constants. The $O(\cdot)$ constants of the milestones are the ones computed in the paper's proofs: $36$ in Corollary 9 and Lemma 11, $6$ in Lemma 10.
Hypotheses added to the page, each disclosed in its statement:
- $\Delta>0$ in Lemma 8, where the page says $\Delta\ge0$ but divides by $\Delta$ ;
- $p\ge2$ in Lemma 8, which is false for $p=1$ ;
- the weighted ratio cost in Lemma 10, as its proof and its use in Lemma 11 require.
Not formalized. The polynomial-time content of "we can find" is not formalized; each such claim is an existence statement.

Contributions are welcome at every level:

proofs of the milestones;
a general strong-duality lemma for concurrent flow, reusable for the uniform, directed and short-path missions of this series;
a reusable region-growing decomposition lemma.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
T. Leighton and S. Rao, An approximate max-flow min-cut theorem for uniform multicommodity flow problems with applications to approximation algorithms, FOCS 1988, 422–431. https://doi.org/10.1109/SFCS.1988.21958
N. Garg, V. V. Vazirani and M. Yannakakis, Approximate max-flow min-(multi)cut theorems and their applications, SIAM J. Comput. 25(2):235–251, 1996. https://doi.org/10.1137/S0097539793243016
N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
Y. Aumann and Y. Rabani, An O(log k) approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27(1):291–301, 1998. https://doi.org/10.1137/S0097539794285983
F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620

8 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Linear Programming and Markov Decision Chains 2: Representatives of Average Optimal Stationary Policies Are Optimal Dual Solutions, and Every Optimal Dual Solution Gives an Average Optimal PolicyResearch Paper

Motivation

A finite Markov decision process may have several recurrent classes under one policy. In that setting, its long-run reward depends on the initial state, and a single stationary distribution does not describe the whole decision problem. Hordijk and Kallenberg developed a linear program with two families of variables to handle this multichain case. Their Theorem 8 relates policies to feasible points of that program in both directions: optimal stationary policies give optimal dual solutions, and every optimal dual solution gives an average optimal stationary policy. This relationship explains why the dual program represents the original sequential decision problem rather than merely bounding its value. Hordijk and Kallenberg (1979)

An earlier frequency formulation associated stationary randomized policies with one family of occupation variables in a more restricted Markov-chain setting. The present theorem uses both $x$ and $y$ variables, and its policy comparison covers history-dependent randomized decisions. The corresponding formalization therefore addresses the finite multichain model of the 1979 paper, with its own dual equations and representative map. Hordijk and Kallenberg (1979), §§1 and 3.3

Setting

Let $E$ be a nonempty finite set of states. At state $i$ , an action $a$ is chosen from a nonempty finite set $A(i)$ . It earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}$ . The transition probabilities are nonnegative and sum to one over $j$ . A general policy $R$ may randomize and use the complete past history. Its average reward $\phi_i(R)$ is the liminf, as the horizon grows, of expected total reward divided by the horizon when the initial state is $i$ . The optimal value $\phi_i$ is the supremum of $\phi_i(R)$ over all such policies. A policy is average optimal when it attains that value at every state. These are the conventions of §2.1 of the paper. Hordijk and Kallenberg (1979), p. 353

A stationary randomized policy $\pi^\infty$ chooses each admissible action $a$ at state $i$ with a fixed probability $\pi_{ia}$ , independently of the epoch and history. Its transition matrix is $P(\pi)_{ij}=\sum_{a\in A(i)}\pi_{ia}p_{iaj}$ , and its reward vector is $r(\pi)_i=\sum_{a\in A(i)}\pi_{ia}r_{ia}$ . The Cesàro limit matrix $P^*(\pi)$ and deviation matrix $D(\pi)$ describe the recurrent and transient behavior of this finite chain. In particular, $\phi(\pi^\infty)=P^*(\pi)r(\pi)$ . Hordijk and Kallenberg (1979), p. 359

Fix positive state weights $\beta_j$ summing to one. The primal linear program minimizes $\sum_j\beta_j\widetilde\phi_j$ over pairs $(\widetilde\phi,\widetilde u)$ that are superharmonic: for every $i$ and $a\in A(i)$ , the first vector dominates its one-step expected continuation, and the sum of the two vectors dominates one-step reward plus the continuation of the second. The dual linear program maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative $x_{ia}$ and $y_{ia}$ satisfying the two flow equations (3) and (4). Variables are present only for admissible state-action pairs. The set $E_x$ consists of states where $\sum_a x_{ia}>0$ . Hordijk and Kallenberg (1979), pp. 356–357

For a feasible dual point $(x,y)$ , the associated policy $\pi(x,y)$ normalizes the $x$ row at states in $E_x$ and the $y$ row at other states. Conversely, equation (6) constructs a representative $(x(\pi),y(\pi))$ of a stationary randomized policy. Its $x$ coordinates use $\beta^TP^*(\pi)$ . Its $y$ coordinates use $\beta^TD(\pi)+\gamma^TP^*(\pi)$ , where $\gamma$ is zero at transient states and is chosen separately on each recurrent class by a maximum formula. The formalization restricts that formula's denominator to the recurrent class, as required by the subsequent nonnegativity calculation; the printed unrestricted denominator has a two-state counterexample. Hordijk and Kallenberg (1979), pp. 359–360

Formalization targets

Optimality correspondence

The goal is Theorem 8, with both directions in one statement:

\pi^\infty\text{ average optimal}\ \Longrightarrow\ (x(\pi),y(\pi))\text{ dual optimal}, \qquad (x,y)\text{ dual optimal}\ \Longrightarrow\ \pi^\infty(x,y)\text{ average optimal}.

The second implication applies to every optimal dual point. It produces the stationary randomized policy given by the printed normalization rule, including its existence as a valid policy. The first implication uses the particular representative defined by equation (6). Neither direction imposes an extreme-point condition. Hordijk and Kallenberg (1979), Theorem 8, p. 360

Supporting results

The milestones state the least-superharmonic characterization of $\phi$ ; the positivity that makes the dual-to-policy normalization meaningful; the stationary gain identity; feasibility and objective value of the representative; and Propositions 4 and 5, which describe tight actions and identify $E_x$ with the recurrent states of $P(\pi(x,y))$ . Each is a statement about the same finite model and the same primal–dual pair. Hordijk and Kallenberg (1979), pp. 356–361

Significance

The theorem establishes an exact relation between two ways of expressing average optimality. The LP direction turns an optimal stationary policy into a dual optimum with a concrete state-action representation. The converse says an arbitrary optimal dual point can be read as an average optimal policy, even when its $x$ coordinates vanish at some states. Proposition 5 specifies what those vanishing coordinates mean for the induced chain: those states are transient. These statements permit optimization over a finite LP while preserving the policy interpretation of its solutions. Hordijk and Kallenberg (1979), Theorem 8 and Proposition 5

The result was proved in 1979; this mission asks for a machine-checked proof of its precise finite-state statement. The shared MDP model and the limit and deviation matrix definitions already exist as published formal objects. The new work is the correspondence for Hordijk and Kallenberg's dual equations, with the representative, its class-wise correction, and the connection to liminf average reward. The definitions of stationary policy mixtures, admissible-pair LP coordinates, and finite-chain recurrence can support later results about average-reward optimization.

Difficulty

Normalizing $x$ alone does not define a policy at every state: its row sum can be zero. The dual program's second variable $y$ supplies the action weights there, and the feasibility equations must ensure its row sum is positive. In the other direction, the natural $\beta^TD(\pi)$ term in $y(\pi)$ need not be nonnegative. The correction $\gamma$ is chosen by a maximum over each recurrent class, while transient states require a different case. These issues remain in a multichain process even though the state and action sets are finite. Hordijk and Kallenberg (1979), pp. 359–361

Formalization scope

Lean uses finite types for states and actions, a nonempty state type, and a nonempty admissible action set at every state. The published StationaryMDP definition provides real rewards and stochastic transition rows. General policies are its history-dependent randomized AvgHRPolicy values; average reward is its liminf reward, and optimal gain is the supremum over that entire policy class. The mission defines its own average-optimality predicate because the published Puterman predicate uses a stronger limsup comparison. For finite rewards, the liminf gains and their supremum are bounded real numbers.

Stationary randomized weights are nonnegative, sum to one on each $A(i)$ , and vanish outside $A(i)$ . The dual variables are functions on the subtype of admissible state-action pairs. The primal and dual optima mean feasible points attaining the relevant objective against every other feasible point. The paper's positive, normalized $\beta$ remains explicit. The raw formula for $\pi(x,y)$ is used only with a feasible dual point, and the policy-well-definedness milestone supplies its nonzero denominators. The representative uses a maximum over the ergodic class of each recurrent state, with the class-restricted denominator needed by the paper's proof; replacing $\gamma$ by zero or by one global maximum would change the target.

The known matrix objects $P^*$ and $D$ are imported from the published Blackwell development. Their convergence and identities are theorem obligations, not assumptions hidden in definitions. Contributions proving the finite-chain identities, representative feasibility, complementary slackness, and the final policy comparison are within scope. A statement restricted to a unichain model, an extreme dual point, or a pure selected action would not establish this theorem.

Selected references

A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. DOI: 10.1287/mnsc.25.4.352.

13 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 2: The Greedy Forward Dual Solution Is Optimal and Its Value Is the Lot-Sizing CostResearch Paper

Motivation

Economic lot sizing asks when to produce goods across a finite planning horizon when demand in each period is known. Producing in a period incurs a fixed setup charge and a marginal cost per unit, while goods may be produced before the period in which they are needed. Such a decision has to balance paying another setup charge against producing more units earlier. The model is a standard setting for studying how dynamic programming and linear optimization describe the same planning decision. Wagelmans, Van Hoesel and Kolen study faster algorithms for this model and, in Section 4, connect the optimal lot-sizing cost to a greedy solution of a dual program Wagelmans et al. (1992).

The dual connection is useful in its own right. It supplies a certificate for the cost returned by the forward dynamic program: a feasible dual vector attains that cost. The paper allows demand to vanish in some periods, which makes the dual values at those periods free and forces care in defining the dynamic program. The mission targets precisely that case.

Setting

There are periods $1,\ldots,n$ . Demand $d_t$ and setup cost $f_i$ are nonnegative for the periods in the horizon. The marginal production cost $c_i$ is any real number. Write $d_{i,j}=\sum_{t=i}^j d_t$ for cumulative demand from $i$ through $j$ . Values at period zero and beyond the horizon are bookkeeping only; every optimization constraint concerns periods $1,\ldots,n$ .

The forward lot-sizing cost $F(j)$ describes the least cost of serving periods $1,\ldots,j$ under the zero-inventory property cited by the paper. Its recursion starts with $F(0)=0$ . If $d_j=0$ , no new production is needed and $F(j)=F(j-1)$ . If $d_j>0$ , the last production setup may occur at some $i\le j$ , giving

F(j)=\min_{1\le i\le j}\bigl(f_i+c_i d_{i,j}+F(i-1)\bigr).

This piecewise definition matters even when only one period has zero demand. Taking the displayed minimum at $d_j=0$ would charge a setup that need not occur.

Program D′ chooses free real values $v_1,\ldots,v_n$ to maximize $\sum_{t=1}^n d_tv_t$ , subject to

\sum_{t=i}^n d_t\max\{0,v_t-c_i\}\le f_i \qquad(1\le i\le n).

“Free” means there is no nonnegativity constraint on $v_t$ . The paper obtains D′ from the dual of the linear relaxation of its simple plant location formulation, using the variables of Formulation III Wagelmans et al., pp. S147, S152–S153. The mission takes D′ as the defined optimization problem.

The greedy forward rule visits periods in increasing order. At a period with $d_j>0$ , the chosen value is the minimum of the upper bounds left by the constraints indexed $i\le j$ :

v_j=\min_{1\le i\le j} \left(c_i+\frac{f_i-\sum_{t=i}^{j-1}d_t\max\{0,v_t-c_i\}}{d_j}\right).

When $d_j=0$ , the rule places no restriction on $v_j$ . This matches the paper's statement that it may be assigned an arbitrary value. One concrete recursive vector in the definitions sets each such value to zero, but the goal covers every assignment.

Formalization targets

The goal says that every vector satisfying the greedy rule is feasible for D′, agrees with the dynamic-programming cost at every prefix, and is optimal among all feasible D′ vectors:

\sum_{t=1}^j d_tv_t=F(j)\quad(1\le j\le n), \qquad \sum_{t=1}^n d_tu_t\le\sum_{t=1}^n d_tv_t \quad\text{for every feasible }u.

The milestone path follows the Section 4 statements: feasibility of the greedy vector; decreasing greedy values across positive-demand periods; the prefix upper bound for any feasible dual vector; and Equation (2), which expresses a greedy prefix value using a minimizing production period. Equation (2) is stated with the induction hypothesis that appears immediately before it in the paper. The goal combines these claims without treating the desired value identity as a hypothesis.

Significance

The result identifies a dual certificate whose value matches the forward lot-sizing cost. It also explains why a greedy forward assignment can solve D′ despite each constraint linking the current value with all later periods. The full-horizon identity recovers the cost $F(n)$ , and the comparison with every feasible vector makes the word “optimal” precise. The paper additionally says that this dual computation directly provides an optimal primal solution; this mission does not encode that reconstruction because it would require the primal formulation and its correspondence to $F$ Wagelmans et al., p. S153.

A formal proof would provide a reusable finite-horizon certificate theorem for this dual formulation and a careful treatment of empty and zero-demand prefixes. The paper's result is already proved mathematically. The Lean files in this proposal state the goal and its milestones; their theorem proofs remain to be supplied by solvers. Related platform goals about the convex hull of other lot-sizing formulations and the Federgruen–Tzur forward algorithm concern different objects, so they are credited as neighboring work rather than imported as this theorem.

Difficulty

A current greedy value is limited by every earlier production index, and feasibility must still hold for the entire horizon, not merely for the constraints truncated at the current period. Equality with $F(j)$ also has to survive periods with zero demand, where the dual coordinate is unrestricted but its weighted contribution vanishes. The forward recurrence has a separate branch at exactly those periods. A formulation that assumes every demand is strictly positive would avoid the delicate case and would miss a feature the authors explicitly retain.

Formalization scope

Lean represents the horizon by natural-number indices $1,\ldots,n$ and the demand, setup, marginal-cost and dual sequences by functions $\mathbb N\to\mathbb R$ . Finite sums use closed intervals; the sum before period $j$ uses $[i,j)$ , so it is empty when $i=j$ . Minima are over the nonempty finite set $\{1,\ldots,j\}$ , only when $j\ge1$ . The horizon $n=0$ has empty sums and no constraints. The cost and dual values are real, with no sign condition on $c_i$ or $v_i$ .

Several informal phrases are made explicit. “The solution is feasible” means every D′ constraint through $n$ holds. “Optimal” includes feasibility, every prefix identity, and comparison with every feasible dual vector. “Can be given an arbitrary value” is represented by no greedy-rule condition at zero demand; the theorem quantifies over all vectors that satisfy the positive-demand conditions. The paper states monotonicity for consecutive nonzero-demand periods; the milestone uses any two positive-demand periods, skipping zero-demand positions so it holds for every choice of their dual values. The weak-duality milestone spells out the paper's reference to “duality and the structure of D′” as an inequality for each feasible vector and prefix.

The identification of $F$ with the optimum of the primal lot-sizing model relies on the zero-inventory property cited by the authors and is not separately formalized. Neither the equivalence of Program D and D′ nor the recovery of a primal production plan is an item here. The paper's running-time claims, including $O(n^2)$ for the greedy forward algorithm and $O(n\log n)$ for its backward algorithm, are outside the scope: the paper does not fix a machine model or constants for them. A definition of $F$ as the optimum of D′ would make the value identity circular; the proposal defines it by the paper's forward recursion instead. The backward algorithm of pp. S153–S155 belongs to a separate development.

Selected references

A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1, 1992, S145–S156. DOI

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming: The Set-Inclusive LP Has the Same Feasible Set as the LP of Support FunctionalsResearch Paper

Motivation

A linear program $\max c\cdot x$ subject to $Ax\le b$ , $x\ge 0$ assumes that the constraint matrix $A$ is known exactly. In practice the columns of $A$ — the activity vectors, describing how much of each resource one unit of activity $j$ consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision $x$ should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.

The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.

Setting

Fix integers $m,n\ge0$ . Vectors in $\mathbb R^m$ are compared componentwise. For a set $S\subseteq\mathbb R^m$ and a scalar $t$ , $tS=\{ta: a\in S\}$ , and the sum of sets is Minkowski addition, $S+T=\{s+t: s\in S,\ t\in T\}$ .

Let $K_1,\dots,K_n\subseteq\mathbb R^m$ be nonempty convex activity sets and $K\subseteq\mathbb R^m$ a nonempty convex resource set. Problem (I) is

\sup\ c\cdot x\quad\text{subject to}\quad x_1K_1+x_2K_2+\cdots+x_nK_n\subseteq K,\quad x_j\ge0,

and $X\subseteq\mathbb R^n$ denotes its set of feasible $x$ . Problem (Ib) is the special case $K=K(b)=\{y\in\mathbb R^m: y\le b\}$ for a right-hand side $b\in\mathbb R^m$ .

The support functional of a set $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y\cdot a$ , a value in $[-\infty,+\infty]$ . With $e_i$ the $i$ -th unit vector, the auxiliary matrix $\bar A$ is the $m\times n$ matrix with entries

\bar a_{ij}=\delta^*(e_i\mid K_j)=\sup_{a_j\in K_j}a_{ij},

defined when all of these are finite, and LP $(\bar A)$ is the linear program $\max c\cdot x$ subject to $\bar Ax\le b$ , $x\ge0$ . Finally $M$ is the set of $m\times n$ matrices $(a_1,\dots,a_n)$ whose $j$ -th column lies in $K_j$ .

In the application, the activity sets are Euclidean balls $K_j=\{a\in\mathbb R^m:\|a-a_j\|_2\le\rho_j\}$ around nominal columns $a_j$ of a matrix $A_0$ , with radii $\rho_j\ge0$ .

Formalization targets

Goal: the THEOREM (p. 1156)

Assume every $K_j$ is nonempty and convex and $\delta^*(e_i\mid K_j)<\infty$ for all $i,j$ . Then

\{x : x\ \text{feasible for (Ib)}\}=\{x : \bar Ax\le b,\ x\ge 0\},

and for every objective $c$ , the optimal solutions of (Ib) and of LP $(\bar A)$ coincide.

Milestones

Feasibility for (I) is equivalent to $x\ge0$ and $\sum_j x_ja_j\in K$ for every choice $a_j\in K_j$ (p. 1154).
LEMMA (p. 1155): $X$ is convex.
If $\delta^*(e_i\mid K_j)=\infty$ for some $i$ , every feasible $x$ of (Ib) has $x_j=0$ (p. 1155).
Compact activity sets have $\delta^*(e_i\mid K_j)<\infty$ (p. 1156).
$x$ is feasible for (Ib) iff $Ax\le b$ for every $A\in M$ and $x\ge0$ (p. 1156).
Every $A\in M$ satisfies $A\le\bar A$ entrywise (proof of THEOREM).
Feasible for LP $(\bar A)$ implies feasible for (Ib) (proof of THEOREM).
Feasible for (Ib) implies $\sum_j x_j\sup_{a_j\in K_j}a_{ij}\le b_i$ for every $i$ , i.e. feasible for LP $(\bar A)$ (proof of THEOREM).
For Euclidean balls, $\delta^*(e_i\mid K_j)=a_{ij}+\rho_j$ , so $\bar a_j=a_j+\rho_je$ with $e$ the all-ones vector (p. 1157).
Inexact LP over balls: (Ib) has the same feasible and optimal solutions as $\max c\cdot x$ subject to $\sum_j x_j(a_j+\rho_je)\le b$ , $x\ge0$ (p. 1157).

Significance

The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in $M$ , of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column $j$ is inflated by the full radius $\rho_j$ , which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.

The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.

Difficulty

The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every $A\in M$ " to $\bar A$ uses that the supremum of a sum of independent terms is the sum of suprema, which needs every $K_j$ nonempty and the scalars $x_j$ nonnegative; with an empty activity set the Minkowski sum is empty and every $x\ge0$ becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.

Formalization scope

Vectors are Fin m → ℝ and Fin n → ℝ, with indices $0,\dots,m-1$ in place of $1,\dots,m$ ; the order on vectors is componentwise.
Feasibility of (I) is the Minkowski-sum inclusion (∑ j, x j • K j) ⊆ R (pointwise set operations) together with $x\ge0$ . It is not defined as "for every choice $a_j\in K_j$ ", which would make milestones 1 and 5 trivial, and $\bar A$ is constructed from the $K_j$ , not an arbitrary matrix dominating $M$ , which would make the goal trivial.
$\delta^*$ is valued in EReal. The entries of $\bar A$ are its real conversions, so every statement mentioning $\bar A$ assumes $K_j\neq\emptyset$ and $\delta^*(e_i\mid K_j)<\infty$ , the paper's standing assumptions (pp. 1154–1156). Convexity of the $K_j$ is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of $K$ ).
An optimal solution is a feasible point attaining the maximum of $c\cdot x$ ; the paper writes $\sup$ and does not discuss attainment. Because the goal identifies the feasible sets, the two problems also have equal suprema.
Hyperspheres use the Euclidean norm (EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii $\rho_j\ge0$ .
The support functional restates the published FenchelRobust.Counterpart.supportFun with the same body.
Not formalized: Magnanti's extension to $\ge$ and $=$ rows (p. 1156), and the remarks on (GLP) and stochastic programming. Contributions of proofs of any milestone, and of an EReal statement equating the optimal values, are welcome.

Selected references

A. L. Soyster, Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming, Operations Research 21(5), 1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Mathematics of Operations Research 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal and A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Mathematical Programming 88, 411–424, 2000. https://doi.org/10.1007/PL00011380
D. Bertsimas and M. Sim, The Price of Robustness, Operations Research 52(1), 35–53, 2004. https://doi.org/10.1287/opre.1030.0065

12 thms2 active usersReviewed

Operations Research Optimization Probability+1·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 4: For a Random Subspace, ‖Pq‖⁻∞ ≤ (log n/n)‖r‖² with Probability Tending to OneResearch Paper

Motivation

Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6

Setting

Fix a dimension $n$ , an integer $d$ with $0\le d\le n$ , and a vector $r\in\mathbb R^n$ . Draw a random $d$ -dimensional subspace $U$ from the distribution invariant under orthogonal transformations. Let $p$ be the Euclidean orthogonal projection of $r$ onto $U$ , and put $q=r-p$ , its projection onto $U^\perp$ . The matrix $P=\operatorname{diag}(p)$ turns the vector $q$ into the coordinatewise product $Pq=(p_jq_j)_{j=1}^n$ .

For a coordinate vector $z$ , let $z^-=(\min\{z_j,0\})_{j=1}^n$ and $\|z\|^-_\infty=\|z^-\|_\infty$ . Thus $\|Pq\|^-_\infty$ records the magnitude of the largest negative coordinate of $Pq$ . An unsubscripted vector norm is always the Euclidean $\ell_2$ norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2

The formal model samples an $(n-d)\times n$ matrix $G$ with independent standard normal entries and sets $U=\ker G$ . The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension $d$ . The construction covers the endpoint cases $d=0$ and $d=n$ as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6

Formalization targets

Theorem 5

For arbitrary choices $r_n\in\mathbb R^n$ and $d_n\le n$ at each dimension, the central target is

\Pr\left\{\|P_nq_n\|^-_\infty\le \frac{\log n}{n}\|r_n\|_2^2\right\} \longrightarrow 1\qquad(n\longrightarrow\infty).

The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of $r_n$ and $d_n$ may change with $n$ ; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13

Source milestones

The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by $\sqrt{3\log n/n}$ with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6

Significance

The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7

The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.

Difficulty

A direct norm bound on $p$ and $q$ loses the coordinate information needed for the factor $\log n/n$ . The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so $\|r\|$ is the $\ell_2$ norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated $d$ -dimensional law almost surely.

Lemma 6 concerns $d,m\ge1$ and $n\ge2$ , where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains $d=0$ , $d=n$ , and $r=0$ . Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition $\varepsilon>0$ . All limits are probabilities tending to one, never probability one at every finite $n$ .

Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.

Selected references

Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. DOI
Sidney I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71, cited in the report for the Gaussian maximum estimate. DOI

7 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Integer Programming Formulation of Traveling Salesman Problems: The Miller–Tucker–Zemlin Constraints Exactly Describe the Itineraries with at Most p Cities per TourResearch Paper

Why this formulation matters

The traveling salesman problem asks for a shortest closed route through a set of cities. Writing it as an integer program requires linear constraints whose integer solutions are exactly the routes. The assignment constraints (each city entered once and left once) are not enough: their integer solutions include collections of disjoint cycles, called subtours, that never pass through the starting city. Some extra family of constraints must rule these out.

In 1960 C. E. Miller, A. W. Tucker and R. A. Zemlin gave such a family using one auxiliary real variable per city (J. ACM 7(4), 326–329). Their MTZ constraints have polynomially many rows, $n^2-n$ for $n$ cities, whereas the subtour elimination constraints of Dantzig, Fulkerson and Johnson (1954) (Oper. Res. 2(4)) have one row per subset of cities. They also handle a generalization: a salesman who returns to base several times, visiting at most $p$ cities per trip. This is the basic form of a capacitated vehicle routing problem. MTZ-type constraints remain standard in vehicle routing models and in textbook formulations of the TSP. Their linear relaxations are known to be weaker than those of the subtour elimination formulation (Padberg and Sung, 1991).

The paper attributes the model to Tucker and reports five machine experiments with Gomory's all-integer algorithm. The computational part is outside this mission.

Setting

There are $n$ cities $1,\dots,n$ and a base city $0$ . A tour is a succession of visits to cities without stopping at city $0$ . In problem (1) the salesman leaves $0$ , visits each of the $n$ cities exactly once and returns to $0$ , possibly several times, with at most $p$ cities per tour. Formally, an itinerary is a list $I=(T_1,\dots,T_t)$ of tours. Each tour is a nonempty list of cities other than $0$ of length at most $p$ , and each city $1,\dots,n$ occurs exactly once in the concatenation of the tours. The number $t$ of tours is the number of returns to $0$ . Tour $(c_1,\dots,c_k)$ travels the arcs $(0,c_1),(c_1,c_2),\dots,(c_k,0)$ . $a_{ij}(I)$ denotes the number of times $I$ travels the arc $(i,j)$ . For real distances $d_{ij}$ , the length of $I$ is the sum of $d_{ij}$ over the arcs it travels.

Problem (2) has non-negative integer variables $x_{ij}$ ( $0\le i\ne j\le n$ ) and real variables $u_1,\dots,u_n$ :

\min \sum\sum_{0\le i\ne j\le n} d_{ij}x_{ij}\quad\text{s.t.}\quad \sum_{\substack{i=0\\ i\ne j}}^{n} x_{ij}=1\ (j\ge1),\quad \sum_{\substack{j=0\\ j\ne i}}^{n} x_{ij}=1\ (i\ge1),\quad u_i-u_j+p\,x_{ij}\le p-1\ (1\le i\ne j\le n).

When the number of tours $t$ is fixed, the relation $\sum_{i=1}^n x_{i0}=t$ is added. With $t=1$ and $p\ge n$ , (1) is the standard traveling salesman problem.

Formalization targets

Goal: the equivalence of (1) and (2)

For every $n\ge0$ and every $p\ge1$ :

\{\,x : \exists u,\ (x,u)\ \text{feasible for (2)}\,\} \;=\; \{\,a(I) : I \text{ a legitimate itinerary of (1)}\,\},

with $\sum_{i=1}^n x_{i0}$ equal to the number of tours $t(I)$ , and with the $u_i$ in the converse taken to be non-negative integers. In addition, $\sum\sum_{i\ne j} d_{ij}\,a_{ij}(I)$ equals the length of $I$ for all real $d$ . The paper says that (2) "will be shown to be equivalent to (1)". Its "burden of proof" is that the two feasible sets correspond and the two objectives agree, and the goal states exactly that.

Milestones, in the order of the paper's proof

The constraints of (2) force $x_{ij}\in\{0,1\}$ (p. 327).
Along a path $r_0,\dots,r_m$ of non-base cities with all $x_{r_kr_{k+1}}=1$ , $u_{r_0}-u_{r_m}\le-m$ (p. 328).
A feasible $x$ has no cycle that avoids city $0$ , so all tours include city 0 (pp. 327–328).
For $p\ge1$ , no tour of a feasible $x$ visits more than $p$ cities (p. 328).
The converse: $u_i=$ the position of city $i$ in its tour makes $(a(I),u)$ feasible, with $1\le u_i\le p$ (p. 328).
Under $x=a(I)$ the objective of (2) is the distance travelled in (1) (p. 327).
An itinerary with $t$ tours of at most $p$ cities requires $tp\ge n$ (p. 326).

Significance

The result. The theorem justifies using (2) in place of (1). Because the feasible sets match and the objectives agree, an optimal solution of (2) is an optimal itinerary of (1), and the same holds with the number of tours fixed. It also shows that a compact, polynomial-size family of linear inequalities in auxiliary potentials excludes every subtour. The same idea, with the $u_i$ read as loads or arrival times, underlies the standard capacity and time-window constraints of vehicle routing.

Formalizing it. The result is classical and its proof is short, but the paper argues informally. It follows successor chains, treats "a tour" without defining an itinerary, and leaves several steps implicit, including the hypothesis $p\ge1$ and the distinctness of $r_{p+1}$ and $r_1$ . No machine-checked statement of the MTZ equivalence is recorded on the platform. The remaining work is the whole formal proof: the combinatorics that turns a 0/1 matrix with unit row and column sums and no subtours into a list of tours, the converse labelling, and the bookkeeping identity between the two objectives.

Difficulty

The inequalities themselves are elementary. Each milestone about (2) is a short computation with the potentials $u_i$ . The work is in the passage from a feasible matrix $x$ to an itinerary. The successor walk from city $0$ must be shown to terminate at $0$ and to cover every arc of $x$ . The resulting tours must be listed so that their arc counts reproduce $x$ exactly, including the number of arcs leaving $0$ . That number is not constrained directly in (2). It equals $\sum_{i}x_{i0}$ only through a counting argument on the row and column sums. A proof that only shows some itinerary exists does not establish the correspondence the paper claims.

Formalization scope

Cities are Fin (n + 1) with 0 the base city, which is the paper's indexing. The commitments, each also stated in the items' Formalization Notes, are:

An itinerary is a List of tours, each tour a List of cities. The paper's "legitimate itinerary" is read as: every tour nonempty, free of 0, of length at most $p$ ; the concatenation duplicate-free; every city $1,\dots,n$ present.
"A feasible solution to (2) has $x_{ij}$ which do define a legitimate itinerary" is read as $x=a(I)$ , the arc counts of $I$ , together with $\sum_{i=1}^n x_{i0}=t(I)$ ("The number of returns to city 0 is given by $\sum x_{i0}$ "). Arc counts are counts, so $x_{ij}\in\{0,1\}$ is a theorem, not an encoding choice.
"Together with appropriate $u_i$ " is made explicit as the existence of natural-number $u_i$ , following the paper's remark that the $u_i$ may be taken non-negative integers. The labelling $u_i=j$ is a definition.
Problem (2) has no variables $x_{ii}$ . The matrix $x$ is indexed by all pairs and the clause $x_{ii}=0$ encodes their absence. $u_0$ exists in the encoding but appears in no constraint.
$x_{ij}\in\mathbb N$ ("non-negative integers"), $u_i\in\mathbb R$ ("arbitrary real numbers"), and $p-1$ and $p\,x_{ij}$ are computed in $\mathbb R$ .
Added hypothesis $p\ge1$ in the goal and in milestone 4. The paper does not state it, and the claim is false without it: for $n=1$ , $p=0$ , $x_{01}=x_{10}=1$ is feasible for (2) but no itinerary exists.
The distances $d_{ij}$ are arbitrary reals, with no sign, symmetry or triangle condition, as on the page.
Milestone 2 states the exact summed bound $-m$ . The page prints the weaker $j+1-k$ .
Milestone 3 excludes every cycle of $x$ avoiding $0$ . The page argues for the cycle met while following successors from $0$ , by an argument that applies to any such cycle.

Not formalized: the constraint and variable counts and the elimination of $x_{i0},x_{0j}$ "to produce an equivalent problem with $n^2+n$ inequalities and $n^2$ variables" (p. 328), which the paper does not make precise, and the machine experiments (pp. 328–329).

Trivializing readings are ruled out. The goal identifies $x$ with the arc counts of an itinerary, not merely the existence of some itinerary. The hypotheses are satisfiable: for $n=3$ , $p=2$ , the itinerary $[[1,2],[3]]$ with $u=(1,2,1)$ is feasible for (2), while the subtour $x_{01}=x_{10}=x_{23}=x_{32}=1$ is not, for any $u$ . Contributions welcome: proofs of the milestones, a reusable library of "functional digraph with unit in- and out-degree" decompositions, and the optimization corollary (equal optimal values of (1) and (2)).

Selected references

C. E. Miller, A. W. Tucker, R. A. Zemlin, Integer Programming Formulation of Traveling Salesman Problems, Journal of the ACM 7(4), 326–329, 1960. https://doi.org/10.1145/321043.321046
G. Dantzig, R. Fulkerson, S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 393–410, 1954. https://doi.org/10.1287/opre.2.4.393
M. Padberg, T.-Y. Sung, An analytical comparison of different formulations of the travelling salesman problem, Mathematical Programming 52, 315–357, 1991. https://doi.org/10.1007/BF01582894
R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bulletin of the AMS 64(5), 275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

On the Job-Shop Scheduling Problem: The Integer Program (2)–(7) with 0–1 Variables y_jk Attains Exactly the Minimum Make-SpanResearch Paper

Motivation

The job-shop scheduling problem asks how to time a set of tasks on shared machines so that every product is finished as early as possible. Around 1959 several authors proposed to solve it with Gomory's then new integer programming (Gomory 1958). The obstacle is the noninterference condition: two tasks on the same machine must not overlap, so one of them must finish before the other starts. That is an "either-or" condition. It describes a nonconvex set, and classical linear programming cannot express it.

A. S. Manne's note On the Job-Shop Scheduling Problem (Operations Research 8 (1960) 219–223) writes the either-or condition as two linear inequalities in integers. It adds one 0–1 variable per pair of tasks that compete for a machine, and it uses a large constant derived from a bound $T$ on the start days. This is the origin of the big-M disjunctive formulation, which remains the standard textbook integer program for job shops and, more broadly, the standard way to linearize a disjunction of two linear inequalities.

Timeline. Johnson (1954) introduced the make-span criterion for two- and three-stage production schedules. Bowman (1959) and Wagner (1959) proposed integer programs for machine scheduling. Manne (1960), stimulated by Bowman's paper, gave the formulation stated here. He counted its unknowns as 275 for 5 machines with 10 tasks each, against 600 for Wagner's formulation on the same example (p. 222).

Setting

There are $n\ge1$ tasks and $M$ machines. Task $j$ requires the single machine $\mu(j)$ for $a_j$ consecutive days, where $a_j$ is an integer. An integer horizon $T$ bounds the start days: the integer unknown $x_j\in\{0,1,\dots,T\}$ is the day on which task $j$ begins. A pair $(j,k)$ with $j<k$ and $\mu(j)=\mu(k)$ is a conflicting pair. For each such pair the tasks must not overlap:

x_j-x_k\ge a_k\quad\text{or else}\quad x_k-x_j\ge a_j. \tag{1}

The instance may also impose precedence $x_j+a_j\le x_k$ for given pairs (5a), exact delays $x_j+a_j+\Theta_{jk}=x_k$ for given pairs (5c), and delivery dates $x_j+a_j\le d_j$ for given tasks (6). A schedule is an $x\in\{0,\dots,T\}^n$ satisfying (1), (5a), (5c) and (6). Its make-span is

\operatorname{ms}(x)=\max_{j}\,(x_j+a_j),

the calendar time needed for all jobs when the shop starts on day $0$ .

Manne's integer program has integer unknowns $x_j$ with $0\le x_j\le T$ , one integer $y_{jk}$ for each conflicting pair, and the minimand $t$ , subject to (5a), (5c), (6),

0\le y_{jk}\le 1,\tag{2}

(T+a_k)\,y_{jk}+(x_j-x_k)\ge a_k,\tag{3}

(T+a_j)(1-y_{jk})+(x_k-x_j)\ge a_j,\tag{4}

and $x_j+a_j\le t$ for every $j$ (7). The value $y_{jk}=1$ means that $j$ precedes $k$ ; $y_{jk}=0$ means that $k$ precedes $j$ .

Formalization targets

Goal: the integer program solves the make-span problem

For every instance and every integer $t^\ast$ ,

t^\ast=\min\{t:\ \exists\,x,y\ \text{integer satisfying } 0\le x_j\le T \text{ and } (2)\text{–}(7)\}\iff t^\ast=\min_{x\ \text{schedule}}\operatorname{ms}(x).

Both minima are required to exist. In particular the program has an optimum exactly when a schedule exists. The paper claims this when it says that "the problem now consists of the minimization of $t$ " subject to (2)–(7) (p. 221).

Milestones

Pair equivalence (p. 220). If $|x_j-x_k|\le T$ , some integer $y_{jk}$ satisfies (2)–(4) if and only if (1) holds.
Equal start days are excluded (p. 220). If $x_j=x_k$ and $a_j,a_k>0$ , no $y_{jk}$ satisfies (2)–(4).
Feasibility correspondence (pp. 220–221). For fixed $x$ and $t$ , some $y$ makes $(x,y,t)$ feasible for (2)–(7) if and only if $x$ is a schedule with $x_j+a_j\le t$ for all $j$ .
The $y_{jk}$ must be discrete (p. 222). With $y_{jk}$ real in $[0,1]$ and $0<a_j,a_k\le T$ , conditions (3)–(4) admit $x_j=x_k$ , where (1) fails.
Counting unknowns (pp. 221–222). With $M$ machines of $p$ tasks each, $n=Mp$ and there are $M\,p(p-1)/2$ conflicting pairs; for $M=5$ , $p=10$ this gives $50+225=275$ unknowns.

Significance

The result. The goal certifies that a single integer program, with one binary variable per conflicting pair, computes the optimal make-span of a job shop with precedence, exact delays and delivery dates. The same pattern is used whenever a disjunction $f\ge0$ or $g\ge0$ of bounded linear forms has to be put into a mixed-integer program: a binary variable selects the active branch, and a constant at least as large as the range of the inactive form switches the other branch off. Milestone 1 is that pattern in its simplest form, and milestone 4 shows why the binary variable cannot be relaxed.

Formalizing it. The paper's argument is informal. It rests on a summary table of admissible values of $y_{jk}$ that holds only when the gap $|x_j-x_k|$ is large enough. A machine-checked version fixes the exact hypotheses: integrality of $y_{jk}$ , the bound $|x_j-x_k|\le T$ , and nonemptiness of the task set. To the best of the curators' knowledge, no machine-checked proof of the correctness of the big-M job-shop formulation exists; the definitions here can serve later scheduling missions that need a disjunctive integer program.

Difficulty

The mathematics is elementary, and the difficulty lies in stating it exactly. The obvious reading, "(3)–(4) are equivalent to (1)", is false without the bound $|x_j-x_k|\le T$ . For instance, with $y_{jk}=0$ condition (4) reads $x_j-x_k\le T$ , which cuts off valid orders if start days may lie beyond the horizon. It is also false for real $y_{jk}$ . Equally, "minimize $t$ subject to (7)" equals the maximum of $x_j+a_j$ only after the optimum over $t$ and over $x$ are interchanged and the empty task set is excluded. A naive formalization that states the schedule side as "the least $t$ with (7)" proves nothing about the make-span.

Formalization scope

Tasks are Fin n (the paper's task $j$ is index $j-1$ ), machines Fin M. Start days, durations, horizon, delays, delivery dates, $y_{jk}$ and $t$ are integers (ℤ), so that $x_j-x_k$ and $1-y_{jk}$ are not truncated. Durations are not assumed positive except in milestones 2 and 4, where positivity is necessary. One definitions file, ManneJobShop.Formulation.Model, holds the instance, the conflicting pairs, schedules, the make-span (Finset.sup', so $n\ge1$ is required via [NeZero n]) and the integer program.

Explicit readings of loose phrases:

"a (large) integer $T$ that will constitute a redundant upper bound upon the unknowns $x_j$ " (p. 219): both the schedule problem and the integer program restrict start days to $0\le x_j\le T$ . Redundancy is not assumed.
"The effect of conditions (3) and (4) may therefore be summarized as follows" (p. 220): stated as the equivalence of milestone 1 and the exclusion of milestone 2, not row by row (for $0<x_j-x_k<a_k$ , condition (3) forces $y_{jk}=1$ , not $\{0,1\}$ ).
"the minimization of $t$ " (p. 221): IsLeast of the feasible values of $t$ , matched against IsLeast of the set of make-spans of schedules.
"necessarily of a discrete nature" (p. 222): existence of a real $y_{jk}\in[0,1]$ satisfying (3)–(4) at $x_j=x_k$ when $0<a_j,a_k\le T$ ("large" $T$ read as $T\ge a_j,a_k$ ).
" $m$ possible conflicting pairs of machine assignments" (p. 222): pairs $j<k$ on the same machine, one $y_{jk}$ each.
"If task $j$ is the last task which the shop is to perform upon the item" (p. 221): a delivery date may be attached to any task, which contains the paper's case.

Trivializing formalizations are ruled out: the make-span is a maximum, not a restatement of (7); $y_{jk}$ is an integer; the horizon appears on both sides; the goal is stated for every instance with $n\ge1$ , including infeasible ones. The (5b) example is (5a) for two pairs. Wagner's comparison, the remarks on Gomory's algorithm, Dantzig's secondary constraints and Monte Carlo methods, and the economic discussion of the make-span are not formalized. Proofs of every milestone and of the goal are welcome.

Selected references

A. S. Manne, On the Job-Shop Scheduling Problem, Operations Research 8(2) (1960) 219–223. https://doi.org/10.1287/opre.8.2.219
E. H. Bowman, The Schedule-Sequencing Problem, Operations Research 7(5) (1959) 621–624. https://doi.org/10.1287/opre.7.5.621
H. M. Wagner, An Integer Linear-Programming Model for Machine Scheduling, Naval Research Logistics Quarterly 6(2) (1959) 131–140. https://doi.org/10.1002/nav.3800060205
R. E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the AMS 64(5) (1958) 275–278. https://doi.org/10.1090/S0002-9904-1958-10224-4
S. M. Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, Naval Research Logistics Quarterly 1(1) (1954) 61–68. https://doi.org/10.1002/nav.3800010110

7 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 1: Binary Search over Rounded LP Vertices Finds a Schedule within Twice the Optimal MakespanResearch Paper

Motivation

Scheduling unrelated parallel machines to minimize the makespan, written $R\,\|\,C_{\max}$ , is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within $2\sqrt m$ times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines $m$ .

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee $2$ , independent of $m$ . Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.

Setting

There are $n$ jobs and $m\ge 1$ machines. If job $j$ is scheduled on machine $i$ , it takes $p_{ij}$ time units, a positive integer. A schedule $\sigma$ assigns every job $j$ to one machine $\sigma(j)$ . The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$ , the makespan of $\sigma$ is the largest load, and $\mathrm{OPT}$ is the minimum makespan over all schedules.

For deadlines $d_1,\dots,d_m$ and a threshold $t$ , let $J_i(t)=\{j: p_{ij}\le t\}$ and $M_j(t)=\{i : p_{ij}\le t\}$ . The linear program (LP) has variables $x_{ij}\ge 0$ for $j\in J_i(t)$ and constraints

\sum_{i\in M_j(t)}x_{ij}=1\quad(j=1,\dots,n),\qquad \sum_{j\in J_i(t)}p_{ij}x_{ij}\le d_i\quad(i=1,\dots,m).

The integer program (IP) replaces $d_i$ by $d_i+t$ and requires $x_{ij}\in\{0,1\}$ . A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point $\tilde x$ is the bipartite graph on machines and jobs with an edge $(i,j)$ whenever $\tilde x_{ij}>0$ .

A $\rho$ -relaxed decision procedure answers, for a deadline $d$ , either 'no' or a schedule, such that (1) every schedule it returns has makespan at most $\rho d$ , and (2) if it answers 'no', no schedule has makespan at most $d$ . The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan $t$ is an upper bound $u$ , with lower bound $l=\lceil t/m\rceil$ , queries the procedure at $d=\lfloor(u+l)/2\rfloor$ , moves $u$ to $d$ on a schedule and $l$ to $d+1$ on 'no', and outputs the best schedule found once $l=u$ .

The LP rounding procedure answers, on deadline $d$ , by solving (LP) with $d_1=\dots=d_m=t=d$ : 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex $\tilde x$ chosen by the LP solver, supported on $\tilde x$ .

Formalization targets

Goal: Theorem 2

For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure $D$ exists, and for every such $D$ the output $\sigma_D$ of the binary search satisfies

\operatorname{makespan}(\sigma_D)\le 2\cdot\mathrm{OPT}.

Milestones

The support graph of every vertex of (LP) is a pseudoforest: every set $S$ of machines and $T$ of jobs spans at most $|S|+|T|$ edges (§2, p. 4).
In a machine–job pseudoforest, every set of jobs of degree at least $2$ can be matched injectively into the machines (§2, pp. 4–5).
A schedule supported on a feasible $\tilde x$ with at most one fractional job per machine has loads at most $d_i+t$ (§2, p. 5).
Theorem 1 (Rounding Theorem): every vertex $\tilde x$ of (LP) has a schedule $\sigma$ supported on $\tilde x$ with

\sum_{j:\sigma(j)=i}p_{ij}\le d_i+t\qquad(i=1,\dots,m).

Lemma 1: for every $\rho$ -relaxed decision procedure, the binary search outputs a schedule of makespan at most $\rho\cdot\mathrm{OPT}$ .
A schedule with makespan at most $d$ gives a feasible point of (LP) with $d_i=t=d$ (§3, p. 5).
The LP rounding procedure is $2$ -relaxed (§3, pp. 5–6).

Significance

Theorem 2 gives a constant-factor approximation for $R\,\|\,C_{\max}$ that does not depend on $m$ . The same rounding theorem drives the paper's second algorithm, a $(1+\epsilon)$ -approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below $3/2$ unless $\mathrm{P}=\mathrm{NP}$ . The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.

The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over $T$ , optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines $d_i$ , arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.

Difficulty

The obvious rounding, putting each job on a machine where $\tilde x_{ij}$ is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound $d_i+t$ requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because $\tilde x$ is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.

On the algorithmic side, the binary search must be shown to return a schedule within $\rho\cdot\mathrm{OPT}$ although the decision procedure is only approximately correct; the invariants (the lower bound stays below $\mathrm{OPT}$ , the stored schedule stays within $\rho$ times the upper bound) have to be tracked through a recursion.

Formalization scope

Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix $(p_{ij})$ ; $\mathrm{OPT}$ is the makespan of a schedule σopt with IsOptimalSchedule.
(LP) is modelled on full $m\times n$ real matrices with the entries $p_{ij}>t$ fixed to $0$ ; this polytope is affinely isomorphic to the paper's, so vertices (Mathlib's Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real $t\ge 0$ , more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral $t$ .
Algorithmic wording not formalized. Theorem 2 states "a 2-approximation algorithm ... that runs in time bounded by a polynomial in the input size"; Lemma 1 speaks of polynomial procedures; Theorem 1 adds "this rounding can be done in polynomial time". Running time, the ellipsoid method and vertex finding are not formalized. What is formalized is the guarantee the proofs establish: the binary search, written as a Lean function, returns a schedule within $\rho\cdot\mathrm{OPT}$ (Lemma 1, for every $\rho$ -relaxed procedure) and within $2\cdot\mathrm{OPT}$ for every LP rounding procedure and every choice of vertex (Theorem 2).
Explicit constants: the factor $2$ of Theorem 2 and of the $2$ -relaxed procedure, which comes from $d_i+t$ with $d_i=t=d$ ; the overshoot $t$ of Theorem 1; the initial bounds $u=$ greedy makespan and $l=\lceil u/m\rceil$ (the paper's $t/m$ , rounded up because $\mathrm{OPT}$ is an integer); the query point $\lfloor(u+l)/2\rfloor$ .
The LP solver's choice is quantified over by a vertex selector, returning a vertex when (LP) is feasible and nothing otherwise; one always exists, since the polytope is compact.
Trivializing formalization ruled out. "There is a schedule with makespan at most $2\cdot\mathrm{OPT}$ " is trivially witnessed by an optimal schedule; the goal instead bounds the output of the binary search, whose every 'almost' answer must be a rounding of the solver's vertex, supported on it and feasible for (IP).
Needed infrastructure: extreme points of polytopes given by linear constraints and their tight-constraint rank characterization; bipartite pseudoforests and Hall-type matchings; well-founded recursion for the search. Proofs of any milestone, and reusable lemmas on extreme points of assignment polytopes, are welcome.

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 (the source of this mission's statements and numbering); also Proc. 28th IEEE Symposium on Foundations of Computer Science (1987) 217–224
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
E. Davis, J. M. Jaffe, Algorithms for scheduling tasks on unrelated processors, Journal of the ACM 28 (1981) 721–736, https://doi.org/10.1145/322276.322284
D. B. Shmoys, É. Tardos, An approximation algorithm for the generalized assignment problem, Mathematical Programming 62 (1993) 461–474, https://doi.org/10.1007/BF01585178
J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3, https://doi.org/10.1007/978-3-540-30717-4

11 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Algorithms for the Assignment and Transportation Problems: Munkres' Algorithm Terminates on Every Real n × n Matrix, and Its Final Starred Zeros Form a Minimum-Sum AssignmentResearch Paper

Motivation

The assignment problem asks how to assign $n$ men to $n$ jobs, one man per job, so that the total cost (or, equivalently, the total rating) is optimal. It is the simplest combinatorial optimization problem with a nontrivial polynomial-time algorithm, and it appears as a subroutine across operations research: in transportation and network-flow methods, in tracking and data association, in scheduling, and as the relaxation behind branch-and-bound methods for the travelling salesman problem.

The algorithm studied here is the one now usually called the Hungarian method or Kuhn–Munkres algorithm.

1931: Kőnig and Egerváry prove the theorem on lines and independent zeros of a matrix that the method rests on.
1955: H. W. Kuhn gives the Hungarian method, with finiteness argued for integer matrices through a decreasing integer sum (Kuhn 1955). M. Flood restates it as Steps A–D.
1957: J. Munkres gives a fully specified version, in which Step B of Flood's outline (find a minimal set of lines containing all zeros and a maximal set of independent zeros) is carried out by an explicit marking procedure with starred and primed zeros. He proves it correct, shows that the integrality assumption is unnecessary, and bounds the work by a polynomial in $n$ (Munkres 1957).

The mission formalizes Munkres' correctness proof for §1 of that paper.

Setting

Let $A=(x_{ij})$ be a real $n\times n$ matrix, $x_{ij}$ being the cost of assigning man $i$ (row $i$ ) to job $j$ (column $j$ ). A set of entries is independent if no two of them lie in the same line (row or column). An assignment is a permutation $\sigma$ , with $\sigma(r)$ the man doing job $r$ . Its cost is $\sum_r x_{\sigma(r)\,r}$ , and $\sigma$ is an optimal assignment if this cost is at most that of every permutation $\tau$ . Choosing $n$ independent entries of minimum sum is the same as choosing an optimal assignment.

The algorithm. A state of the algorithm holds the current matrix, a set of starred zeros $0^*$ , a set of primed zeros $0'$ , a set of covered rows and a set of covered columns. An entry is non-covered, once-covered or twice-covered according as it lies in zero, one or two covered lines.

Preliminaries. Subtract from each row its smallest element, then from each column its smallest entry. Consider the zeros in turn and star each one that has no starred zero in its row or column. Cover the columns containing a $0^*$ .
Step 1. Prime a non-covered zero. If its row contains no $0^*$ , go to Step 2. Otherwise cover its row and uncover the column of that $0^*$ . When no non-covered zero remains, go to Step 3.
Step 2. Build the alternating sequence $Z_0,Z_1,\dots,Z_{2k}$ . It starts at the $0'$ just found. Each $Z_{2i+1}$ is the $0^*$ in the column of $Z_{2i}$ , each $Z_{2i+2}$ is the $0'$ in the row of $Z_{2i+1}$ , and the sequence stops at a $0'$ with no $0^*$ in its column. Unstar its starred zeros and star its primed zeros. Erase all primes, uncover all rows and cover the columns containing a $0^*$ . Stop if all columns are covered; otherwise return to Step 1.
Step 3. Let $h$ be the smallest non-covered element. Add $h$ to each covered row, subtract $h$ from each uncovered column, and return to Step 1 with all marks kept.

The quantity $n_k$ , the maximal number of independent zeros of the matrix $A_k$ , measures progress.

Formalization targets

Goal: correctness of the algorithm

For every real $n\times n$ matrix $A$ :

\exists\,\text{start};\quad \text{every run is finite};\quad \text{no reachable non-final state is stuck};\quad \text{at a final state } \{0^*\}=\{(\sigma(r),r)\}\ \text{with}\ \sum_r x_{\sigma(r)r}=\min_\tau \sum_r x_{\tau(r)r}.

The four clauses are needed together: optimality at final states alone holds for an algorithm that never stops.

Milestones

Remark (2): subtracting row constants $u_i$ and column constants $v_j$ does not change the optimal assignments.
The zeros starred in the Preliminaries are independent.
At Step 2 the sequence $Z_0,\dots,Z_{2k}$ exists, is unique and has distinct elements.
Step 2 leaves an independent set of starred zeros, larger by one.
Lines containing all the zeros number at least the maximal number of independent zeros.
At Step 3 the starred zeros are a maximal independent set and the covered lines a minimal cover.
At Step 3, $h>0$ ; the transformation subtracts $h$ from non-covered entries, adds $h$ to twice-covered ones, keeps every $0^*$ and $0'$ a zero, and $n_{k+1}\ge n_k$ .
If $n_{k+1}=n_k$ , Step 2 does not occur before the next Step 3, which begins with more covered rows.
While $n_k$ is constant, Step 3 is applied at most $n$ times.
Every row and column of the matrix always contains a zero.
Step 3 decreases the sum of the entries by $n(n-n_k)h$ .

Significance

Correctness of the Hungarian method is the basis of a standard algorithm for the assignment problem and, through it, of methods for transportation problems, minimum-cost bipartite matching and weighted bipartite matching. Its $O(n^3)$ refinements remain in practical use. The invariants of the proof are the primal–dual structure of the problem: the row and column constants subtracted along the way form a dual solution, and the starred zeros at the end are a primal solution satisfying complementary slackness.

The result has been proved since 1957 and is in every textbook on combinatorial optimization. A machine-checked version of Munkres' specific procedure, as a transition system with all its free choices, with finiteness for real (not only integer) matrices, is not available on this platform; Mathlib has no assignment algorithm. The mission produces a verified specification of the algorithm, reusable invariants about covers and independent zeros, and a termination argument that does not rely on integrality.

Difficulty

Optimality at termination is short once the invariants are known. The work lies in two places.

First, the invariants hold only along runs. "Each $0^*$ is covered by precisely one line", "no column contains more than one $0^*$ " and "no row contains more than one $0'$ " fail for arbitrary marked matrices, so they must be carried as an inductive invariant through every move, including the Step 3 transformation, which keeps the primes.

Second, termination. The obvious measure, the sum of the entries, decreases by $n(n-n_k)h$ at each Step 3, but for real entries $h$ can be arbitrarily small, so the decreasing sum gives no bound on the number of steps. The page replaces this argument by the stronger result of p. 35 (milestone 8), which holds for real entries. Turning it into a proof that every run of the nondeterministic move relation is finite, including the moves inside Step 1 and Step 2, is the core of the formalization.

Formalization scope

Matrices and positions. Entries are arbitrary reals, as on p. 35. Positions are Fin n × Fin n (row, column).
Output orientation. The output permutation follows the published definition HeldWolfeCrowder_Assignment_Setting: σ r is the row assigned to column r, the starred positions are $(\sigma(r),r)$ , and optimality is IsOptimalAssignment A σ with respect to the original input matrix.
Nondeterminism. The algorithm is an inductive move relation Step. The order in which the Preliminaries consider the zeros, and the non-covered zero primed in Step 1, are free choices. Every claim holds for every run.
Relational steps. Step 2's sequence and Step 3's $h$ are described relationally. Their existence, and $h>0$ , are theorems, not built into the moves.
Reachable states. Invariants are stated for states reachable from a start state, never for arbitrary states.
Finiteness. Finiteness of every run is accessibility (Acc) of each start state for the reversed move relation.
Termination test after the Preliminaries. "If all columns are covered, stop" is also applied when leaving the Preliminaries. The page goes to Step 1 unconditionally there. If the Preliminaries already star $n$ zeros, Step 3 would then have no non-covered element.
Independent zeros. The maximal number of independent zeros is a finite maximum of cardinalities, so it has no junk value.
Edge case $n=0$ . No positivity of $n$ is assumed. For $n=0$ the start state is final.
Ruled out. A goal stating only optimality at final states, or invariants stated for arbitrary states, would be a trivializing formalization; the goal states termination of every run and absence of stuck states as well.

Not formalized: the operation count $(11n^3+12n^2+31n)/6$ of pp. 35–36, whose cost model is informal; the argument that returning to the standard input after Step 3 is unnecessary (pp. 34–35); König's theorem (Remark (1), cited); and §2 on the transportation problem, which is stated without proof.

Welcome contributions: proofs of the milestones, a general library of lines and independent zeros in matrices (reusable for König–Egerváry), and an executable refinement of the move relation.

Selected references

J. Munkres, Algorithms for the assignment and transportation problems, J. Soc. Indust. Appl. Math. 5 (1957), 32–38. https://doi.org/10.1137/0105003
H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. https://doi.org/10.1002/nav.3800020109
M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223 (source of the published assignment-cost definitions reused here)

15 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Linear Programming and Sequential Decisions: An Optimal Solution of the Equilibrium LP Yields a Stationary Decision Rule of Least Expected Monthly CostResearch Paper

Motivation

Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.

Timeline of the LP approach to average-cost problems:

1960 — Manne: the inventory model as a linear program in the joint probabilities of (stock level, production quantity); mixed strategies allowed; the decision rule is read off as a conditional probability.
1960 — H. M. Wagner, in a companion note in the same issue, shows that an optimal solution consisting of pure strategies exists.
1962 — C. Derman (Management Science 9(1), 1962) gives the general finite-state, finite-action version, assuming every stationary randomized rule yields an irreducible chain.
1960 — F. d'Epenoux (Revue Française de Recherche Opérationnelle 4, No. 14; English translation 1963) treats the discounted criterion by linear programming, as Manne's closing note records.

Setting

A positive integer $T$ bounds inventory accumulation; the stock levels are $0,1,\dots,T$ . At the start of a month the initial stock $i$ is observed and a production quantity $j$ is chosen; the available stock is $k=i+j$ . The month's demand $n\in\{0,1,2,\dots\}$ is independent of everything else and has law $p_n$ . Backlogs are excluded, so the terminal stock is $t=\max(0,k-n)$ , which becomes the next initial stock. A finite set $A$ of admissible pairs $(i,j)$ , all with $i+j\le T$ and containing $(i,0)$ for every $i\le T$ , lists the decisions available at each stock level. Costs are three arbitrary real functions: $C_1(i)$ of the initial stock, $C_2(j)$ of the production quantity, and $C_3(n-k)$ of the shortage level.

A stationary randomized decision rule $q(j\mid i)$ is a conditional probability of producing $j$ at stock $i$ , supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of $q$ is a stationary distribution $y=(y_0,\dots,y_T)$ of that chain: the law $y'$ of the terminal stock equals the law $y$ of the initial stock, (2). The expected monthly cost (1) of $q$ in the equilibrium $y$ is

\mathcal EC_1(i)+\mathcal EC_2(j)+\mathcal EC_3(n-k),

the expectation taken under the joint law $y_i\,q(j\mid i)\,p_n$ of (initial stock, production, demand).

The linear program has one unknown $x_{ij}$ per admissible pair, the joint probability of (initial stock $i$ , production $j$ ). Its constraints are $x_{ij}\ge0$ , (4) $\sum_{i,j}x_{ij}=1$ , and the equilibrium equations

\text{(8.t)}\qquad \sum_j x_{tj}=\sum_{\substack{i,j,n:\\ i+j-n=t}}p_nx_{ij}\qquad(t=1,\dots,T),

and its objective (9) is $\sum_{i,j}c_{ij}x_{ij}$ with the cost coefficients (10)

c_{ij}=C_1(i)+C_2(j)+\sum_np_nC_3(n-i-j).

The companion equation (8.0) for $t=0$ has right-hand side $\sum_{i+j-n\le0}p_nx_{ij}$ and is omitted from the constraints. A feasible $x$ is decoded into $y_i=\sum_jx_{ij}$ and $q(j\mid i)=x_{ij}/y_i$ .

Formalization targets

The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.

Goal: an LP optimum gives an optimal stationary rule

Assume $\sum_np_n|C_3(n-i-j)|<\infty$ for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution $x^*$ , with decoding $(q^*,y^*)$ , $q^*$ is a stationary randomized rule, $y^*$ is a statistical equilibrium of $q^*$ , and

\mathrm{Cost}(q^*,y^*)=\sum_{i,j}c_{ij}x^*_{ij}\le \mathrm{Cost}(q,y)

for every stationary randomized rule $q$ and every statistical equilibrium $y$ of $q$ .

Milestones

(7): under a rule in a distribution $y$ , the law of the terminal stock is the right-hand side of (7)/(8) evaluated at $x_{ij}=y_iq(j\mid i)$ .
(8.0)–(8.T): a rule in statistical equilibrium yields a point satisfying $x\ge0$ , (4) and all of (8.0)–(8.T).
(8.0) is redundant: (4) and (8.1)–(8.T) imply (8.0).
§3, N.B.: every feasible $x$ equals $y_iq(j\mid i)$ for its decoding $(q,y)$ , with $y$ an equilibrium of $q$ .
(10): the expected monthly cost (1) under the joint law $x_{ij}p_n$ equals $\sum c_{ij}x_{ij}$ .
Table 1: the cost coefficients of the §6 example ( $T=3$ , $p=(2/3,0,1/3)$ , $C_1(i)=i$ , $C_2(j)=3j$ , $C_3(m)=\max[0,6m]$ , $j\in\{0,1\}$ ) are $4,5,3,4,2,5,3$ .
Table 2, footnote 3: $x_{01}=1/3$ , $x_{11}=2/9$ , $x_{20}=4/9$ is optimal with cost $31/9$ ; the do-nothing solution costs $4$ .
Footnote 5: the implicit prices $-7/3,-13/3,-11/3$ of (8.1)–(8.3), with $31/9$ on (4), are an optimal dual solution.

Significance

The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.

The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient $x_{ij}/\sum_jx_{ij}$ is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.

Difficulty

Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over $(i,j,n)$ with conditions $i+j-n\le0$ and $i+j-n=t$ , and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and $\sum_np_n=1$ . The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level $0$ must be recovered from (4) and the bound $i+j\le T$ . And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.

Formalization scope

All statements live in the namespace ManneLP.Equilibrium. Conventions:

Stock levels and production quantities are natural numbers; a model carries $T>0$ , the admissible set $A$ (a Finset (ℕ × ℕ) with $i+j\le T$ and every $(i,0)\in A$ ), a demand law $p:\mathbb N\to\mathbb R$ with $p_n\ge0$ and HasSum p 1, and costs $C_1,C_2:\mathbb N\to\mathbb R$ , $C_3:\mathbb Z\to\mathbb R$ . The shortage level $n-i-j$ is an integer; no convexity, sign or monotonicity of the costs is assumed.
The admissible set is a parameter: §6 imposes a capacity limit $j\le1$ . Reading of the page: $i+j\le T$ is how §2's requirement $\max(0,k-n)\le T$ holds whatever the demand; $(i,0)\in A$ (producing nothing is possible) is implicit in §2.
The terminal stock is computed by truncated subtraction in $\mathbb N$ , which equals $\max(0,k-n)$ . Sums over demands are tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.
A statistical equilibrium is a stationary distribution of the chain of the rule, defined from the transition probabilities, not from (8). The expected monthly cost is defined from the joint law of (stock, production, demand), not as $\sum c_{ij}x_{ij}$ . The LP constraint set omits (8.0), exactly as the page does.
The decoded rule uses the default action $j=0$ at stock levels with $\sum_jx_{ij}=0$ ; any admissible default would do.
Table 2's $x_{30}=\varepsilon$ is the paper's device against degeneracy; the example's solution has $x_{30}=0$ . Footnote 5 prints no price for (4); $31/9$ is the price forced by equal objectives, and the dual optimum is not claimed unique.

Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as $\sum c_{ij}x_{ij}$ (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.

Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.

Selected references

A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963 (translation of the 1960 French paper). https://doi.org/10.1287/mnsc.10.1.98

13 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems VII: Bias Optimality — Four Equivalent Characterizations of a Bias Optimal Pure Stationary PolicyTextbook

Why bias optimality matters

A finite Markov decision problem can have several policies with the same long-run average reward even though they behave differently before reaching a recurrent class. Average reward discards a finite initial advantage: dividing total reward by the horizon sends any fixed transient contribution to zero. In applications where the process runs for a long but unspecified time, this leaves a genuine choice among average-optimal policies. Bias optimality uses discounted values as the discount factor approaches one to resolve that choice. Kallenberg develops the criterion in Chapter 5 of Linear Programming and Finite Markovian Control Problems, following Blackwell's earlier notion of a nearly optimal policy.

The chapter asks for a way to recognize a bias optimal policy without comparing it directly with every possible sequence of history-dependent, randomized decisions. Its central characterization, Theorem 5.2.2, gives three tests involving only pure stationary policies. That change in the comparison class matters: there are finitely many pure stationary rules, while a general policy may depend on an unbounded history. The theorem also explains why average optimality alone leaves policies untied only at the gain level, while their bias vectors can differ. The two-state example in Figure 5.2.1 exhibits an average-optimal stationary rule that is not bias optimal (Kallenberg, pp. 163–164).

The finite decision model

The state space is $E=\{1,\ldots,N\}$ with $N>0$ . Each state $i$ has its own finite, nonempty set $A(i)$ of admissible actions. Choosing $a\in A(i)$ earns the real reward $r_{ia}$ immediately and moves to state $j$ with probability $p_{iaj}$ . The rows are stochastic: $p_{iaj}\ge0$ and $\sum_jp_{iaj}=1$ . This is the chapter's standing assumption, stated at the opening of §5.2 (Kallenberg, p. 162).

A policy $R\in C$ assigns a probability distribution on the actions available at the current state after every finite history. Thus $C$ includes randomized and history-dependent decisions. A pure stationary policy $f^\infty\in C_D$ instead fixes one action $f(i)\in A(i)$ for each state and uses it in every period. Time starts at $t=1$ . From initial state $i$ , let $v_i^t(R)$ be expected reward in period $t$ , and let $v_i^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}v_i^t(R)$ be expected discounted reward for $0\le\alpha<1$ . The optimal discounted value $v_i^\alpha$ is the supremum of $v_i^\alpha(R)$ over all $R\in C$ , taken separately for each state.

The average reward is $\phi_i(R)=\liminf_{T\to\infty}T^{-1}\sum_{t=1}^T v_i^t(R)$ ; its optimal value $\phi_i$ is again the statewise supremum over $C$ . The corresponding limsup is $\hat\phi_i(R)$ . A policy is average optimal when $\phi_i(R)=\phi_i$ at every state. It is bias optimal when $v_i^\alpha(R)-v_i^\alpha\to0$ as $\alpha\uparrow1$ at every state (Kallenberg, pp. 21–23 and 161).

For a pure stationary $f$ , write $P(f)_{ij}=p_{i,f(i),j}$ and $r(f)_i=r_{i,f(i)}$ . The stationary matrix $P^*(f)$ is the Cesàro limit of the powers of $P(f)$ . The deviation matrix and bias vector are

D(f)=\bigl(I-P(f)+P^*(f)\bigr)^{-1}-P^*(f), \qquad u(f^\infty)=D(f)r(f).

The gain of $f^\infty$ is $\phi(f^\infty)=P^*(f)r(f)$ . These are the book's Definitions 2.4.2 and notation (2.5.5), and their finite stochastic-matrix properties are recorded in Theorem 2.4.1 (Kallenberg, pp. 29 and 33–34).

Formalization targets

The goal is Theorem 5.2.2, for each pure stationary $f_*^\infty$ . It asserts that the following are equivalent: (i) $f_*^\infty$ is bias optimal against the value over all $C$ ; (ii) for every $f^\infty\in C_D$ , the vector limit $\lim_{\alpha\uparrow1}\bigl(v^\alpha(f_*^\infty)-v^\alpha(f^\infty)\bigr)$ exists and is nonnegative; (iii) $f_*^\infty$ is average optimal and, at every state $i$ , its bias is maximal among pure stationary policies optimal at that state; and (iv) for every $f^\infty\in C_D$ , the vector limit

\lim_{T\to\infty}\frac1T\sum_{t=1}^T\sum_{s=1}^t \bigl(v^s(f_*^\infty)-v^s(f^\infty)\bigr)\ge0

exists. These limits are read in the extended reals: a strictly positive gain gap makes a difference tend to $+\infty$ , which satisfies the displayed inequality. The period rewards $v^s$ in the last formula are not discounted values. The printed clause (iii) has a typographical error in the set following max; its proof on p. 164 supplies the intended restriction $\phi_i(f^\infty)=\phi_i$ . The formal statement uses that reading and records it explicitly.

Two earlier chapter results are milestones. Lemma 5.2.1 bounds the Abel limsup $(1-\alpha)v_i^\alpha(R)$ by the upper average reward $\hat\phi_i(R)$ for any policy. Theorem 5.2.1 says that bias optimality implies average optimality, with a two-state example showing that average optimality does not imply bias optimality. The later §5.3 linear-programming construction is a separate route to finding a bias optimal policy and is outside this mission's statement layer.

What the characterization gives

The equivalence allows bias optimality to be checked through discounted differences, bias vectors, or accumulated period rewards. Its bias-vector clause identifies the relevant comparison set: a policy can be optimal in average reward at one state without being optimal at every state, and that statewise distinction cannot be discarded. It also makes the bias criterion finer than average optimality, as the two-state counterexample shows (Kallenberg, pp. 163–165).

The source proves these results; the mission asks for machine-checked proofs of the stated equivalence and its two supporting results. The finite history and reward definitions can support later formalizations of Kallenberg's average-reward and constrained models. The matrix definitions can also be reused for results about finite Markov chains, including the Cesàro limit and deviation matrix. No machine-checked proof of this specific four-way characterization is claimed here.

Where the difficulty lies

Comparing average rewards alone loses the transient reward information that bias is designed to retain. The discounted comparison has an apparent divergence of order $(1-\alpha)^{-1}$ whenever two policies have different gains; the finite residual becomes meaningful only after those gain terms are separated. The accumulated-reward test also takes a second Cesàro average, so a direct identification with ordinary average reward would miss its bias contribution. The theorem has to preserve both the gain ordering and the finite bias remainder across these limiting regimes (Kallenberg, pp. 164–165).

For a general policy, the discounted value is defined by infinitely many history-dependent choices, whereas $P^*$ and $D$ apply to one fixed stationary matrix. This is the obstacle in passing from clause (i), which compares with all $C$ , to the tests against $C_D$ . Treating the optimal discounted value as a supremum over stationary policies by definition would erase that obstacle and change the theorem.

Formalization scope

Lean uses Fin N with $N>0$ for states and a finite action type with nonempty state-dependent admissible subsets. Rewards are real, transition rows are stochastic, and policies are distributions on actions after complete finite histories. The finite sum of products defining each history's probability supplies $v_i^t(R)$ ; no measure-theoretic path space is needed. Discounted rewards use a real infinite sum for $\alpha$ near one from below. Average rewards are real liminf and limsup values of bounded sequences. Optimal values are statewise suprema over all admissible policies, not over just $C_D$ .

The matrix $P^*$ is a Cesàro limit and $D$ uses the book's inverse formula. Their convergence and nonsingularity for finite stochastic matrices are mathematical obligations, not added assumptions of the goal. The $T=0$ value of a totalized average and the value of a discounted sum outside its summable range do not enter the limits. Contributions to the finite-chain limit facts, boundedness of reward criteria, the Abel/Cesàro comparison, and the four equivalences are all within scope. A formalization that restricts the optimum in bias optimality to pure stationary policies would not be this theorem.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository.
David Blackwell, “Discrete Dynamic Programming,” Annals of Mathematical Statistics 33 (1962), 719–726. DOI.

8 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems IV: Positive Dynamic Programming — an Extreme Optimal Dual Solution Yields a Pure Stationary Optimal PolicyTextbook

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.

6 thms2 active usersReviewed

Completed

Discrete Geometry Group Theory·Captain: mikedeng1

Some Polyhedra Related to Combinatorial Problems II: The Faces of the Master Polyhedron P(G, g0) Are the Basic Feasible Solutions of a Subadditive Linear SystemResearch Paper

Motivation

Finite group equations arise when an integer program is expressed relative to an integer basis: the residue of a candidate solution in a finite Abelian group records whether it satisfies the original integrality requirement. Gomory's group polyhedron collects the nonnegative integer solutions with one prescribed residue. Its faces give valid linear inequalities for the group relaxation, so a description of those faces is useful to anyone studying integer programming cuts or the geometry of integer hulls. Gomory's 1969 paper develops the group equation and its polyhedra in this setting and then gives a finite system for the faces of the largest, or master, polyhedron. Gomory 1969, pp. 457–458, 474, 480–483.

The main question is how to recognize a facet inequality without ranging over every nonnegative integer solution of the group equation. The paper's Theorem 7 characterizes facets through a system with one row for each integer solution, an infinite collection in general. Theorem 18 replaces that family by rows determined by pairs of group elements and a rank condition at the candidate coefficient vector. Gomory 1969, pp. 469–470, 481–483.

Setting

Let $\mathcal G$ be a finite Abelian group with zero $0$ , and let $\mathcal G^+=\mathcal G\setminus\{0\}$ . For a subset $\mathcal N\subseteq\mathcal G^+$ and a right-hand side $g_0\in\mathcal G$ , a group-equation solution is a nonnegative integer vector $t\in\mathbb N^{\mathcal N}$ satisfying

\sum_{g\in\mathcal N}t(g)g=g_0.

The set of solutions is $T(\mathcal G,\mathcal N,g_0)$ , and the group polyhedron $P(\mathcal G,\mathcal N,g_0)$ is their convex hull in the real coordinate space $\mathbb R^{\mathcal N}$ . The master polyhedron $P(\mathcal G,g_0)$ uses $\mathcal N=\mathcal G^+$ . This mission concerns $g_0\ne0$ ; Gomory specifies a separate convention at $g_0=0$ , excluding the zero solution from that master polyhedron. Gomory 1969, pp. 457–458, 474–475.

Gomory calls $\pi\cdot x\ge\pi_0$ a face when $\pi\ne0$ , all points of $P$ satisfy the inequality, and its tight points generate the entire hyperplane $\pi\cdot x=\pi_0$ by affine combinations. Thus "face" means a facet of full hyperplane dimension here. The equivalent integer-point criterion uses the tight members of $T$ , which is the representation adopted in Lean. A basic feasible solution of a linear system satisfies every equation and inequality and has tight rows whose coefficient vectors span the full variable space. Gomory 1969, pp. 468–469.

Formalization targets

The path to the goal starts with the sign of the face coefficients, the infinite-system characterization, and the shortest-path interpretation. An integer vector $t$ represents a path whose total group displacement is $\sum_g t(g)g$ and whose length is $\pi\cdot t$ . The shortest-path statements lead to subadditivity and complementary equalities for face coefficients. For $P(\mathcal G,g_0)$ , Theorem 17 collects the row conditions needed for the final system. Gomory 1969, pp. 469–473, 480–481.

The target is Theorem 18. Fix $g_0\ne0$ and $\pi_0>0$ . With $\pi(0)=0$ , system (13) is

\begin{aligned} \pi(g_0)&=\pi_0,\\ \pi(g)+\pi(g_0-g)&=\pi_0 &&(g\in\mathcal G^+,\ g\ne g_0),\\ \pi(g)+\pi(h)&\ge\pi(g+h) &&(g,h\in\mathcal G^+),\\ \pi(g)&\ge0 &&(g\in\mathcal G^+). \end{aligned}

The goal asserts the full equivalence

\pi\cdot x\ge\pi_0\text{ is a face of }P(\mathcal G,g_0) \quad\Longleftrightarrow\quad \pi\text{ is a basic feasible solution of (13).}

The equation rows, ordered pair rows, and nonnegativity rows all count toward basicness; $\pi_0$ is held fixed. Gomory 1969, pp. 481–483, Theorem 18.

Significance

Theorem 18 turns a geometric property defined against infinitely many integer vectors into a finite test in $|\mathcal G|-1$ coefficient variables. A solver can check its displayed equations and inequalities and then check whether the tight row vectors have full rank. That gives a concrete route to enumerating the facet coefficient vectors of $P(\mathcal G,g_0)$ for a fixed finite group, the use Gomory reports immediately after the proof. Gomory 1969, p. 483.

The result was proved in the paper; the work here is to formalize that known theorem and the numbered results it uses. The group-solution model, the integer-point facet criterion, and the generic tight-row definition of basic feasibility can also support other group-polyhedron arguments. The local prior-art search found related formalizations of facets and polyhedra, but none with the same integer-point-generated hyperplane and finite-group conventions, so these definitions are stated for this paper's objects.

Difficulty

Validity of the rows of (13) for a face does not by itself establish Theorem 18. Basicness requires the tight rows to span all $|\mathcal G|-1$ coefficient directions, and the converse must turn that rank information into enough tight integer solutions to generate a hyperplane. A supporting inequality that is tight at only a smaller face would pass a mere feasibility check while failing Gomory's face definition. The shortest-path results connect the group equations to the coefficient restrictions, but do not erase the rank requirement. Gomory 1969, pp. 468–470, 472–473, 481–483.

Formalization scope

Lean uses a finite Abelian group and a Finset $\mathcal N$ of nonzero elements. Its real vectors have coordinates indexed by $\mathcal N$ itself, with no unconstrained zero coordinate. The group equation is a finite sum of natural-number multiples in $\mathcal G$ ; $P$ is the real convex hull of the cast integer solutions. A face requires a nonzero normal, validity on every integer solution, and equality between the affine span of tight integer points and the entire hyperplane. This excludes the trivial reading that merely asks for one tight point. It also makes an empty solution set incapable of supplying a face. Theorem 7 assumes $\mathcal N$ nonempty ( $n'\ge1$ ), as the paper does implicitly: with no coordinates every vector would be trivially basic.

Paths are represented by their nonnegative integer arc-multiplicity vectors. The same vector can describe several arc orders, but the length and group displacement used here depend only on multiplicity. Shortestness is stated by comparison with every competing vector of the same displacement; no infimum with an empty-set default is used. The complement and subadditivity rows of (13) use $\pi(0)=0$ , and the subadditivity rows include ordered pairs with equal entries. Basic feasible solutions use the span of tight coefficient rows, including equation rows, in the full real space of $|\mathcal G|-1$ variables.

The mission includes the paper's Theorems 6, 7, 10, 17, Lemmas 1–2, and both numbered corollaries on p. 473 as milestones. Contributions that establish the affine-span and rank equivalences, or reusable finite-group shortest-path and polyhedral lemmas, directly advance the target. Theorems for $g_0=0$ and for other sections of the paper are outside this mission's stated domain.

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.

11 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+2·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems IX: Discounted Semi-Markov Decision Processes — the Value Vector Is the Smallest Superharmonic VectorTextbook

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.

6 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Some Polyhedra Related to Combinatorial Problems I: A Minimizing Vertex of the Corner Polyhedron Gives an Optimal Integer Solution When the Right-Hand Side Lies Deep in the Basis ConeResearch Paper

Motivation

An integer program in standard form, $\max c\cdot x$ subject to $Ax=b$ , $x\ge 0$ , $x$ integer, is easy to state and hard to solve. Its linear programming relaxation is solved by the simplex method, which ends at an optimal basis $B$ . The difference between the two problems is the integrality of $x$ , and R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2, 451–558, doi:10.1016/0024-3795(69)90017-2) measures that difference with a finite Abelian group. Dropping only the nonnegativity of the basic variables leaves a problem whose feasible set has a simple structure: its convex hull is the corner polyhedron, and its integer points are the solutions of an equation in the group $\mathbb Z^m/B\mathbb Z^m$ .

The first section of the paper uses this to explain when the integer program reduces to the group problem. Its asymptotic theorem says that if $b$ lies far enough inside the cone where $B$ is LP-optimal, then an optimal solution of the group problem gives an optimal integer solution. Gomory first proved this in 1965 (On the relation between integer and noninteger solutions to linear programs, PNAS 53, 260–265, doi:10.1073/pnas.53.2.260) by a counting argument on group solutions. The 1969 paper proves it again through the geometry of the corner polyhedron. The vertices of that polyhedron are irreducible, and an irreducible point is small. This is the version formalized here.

Setting

Let $A=(B,N)$ be an integer $m\times(m+n)$ matrix, with $B$ a nonsingular $m\times m$ matrix (the first $m$ columns) and $N$ the $m\times n$ matrix of the remaining columns $N_1,\dots,N_n$ . As on p. 452 of the paper, $A$ contains an $m\times m$ unit matrix. Let $b\in\mathbb Z^m$ and $c=(c_B,c_N)\in\mathbb R^{m+n}$ . The integer program (2) is

\max\ c\cdot x\quad\text{subject to}\quad Ax=b,\ x\ge 0,\ x\ \text{integer}.

The relative prices are $c_N^*=-c_N+c_BB^{-1}N$ , with components $c^*_{m+i}$ . $B$ is an optimal LP basis when $B^{-1}b\ge0$ and every $c^*_{m+i}\ge0$ .

The group is $\mathcal G=M(I)/M(B)$ , where $M(I)=\mathbb Z^m$ and $M(B)$ is the lattice of integer combinations of the columns of $B$ . Let $f$ be the quotient map. $\mathcal G$ is finite of order $D=|\det B|$ . Let $\mathcal N$ be the set of nonzero elements among $fN_1,\dots,fN_n$ , and put $g_0=fb$ . The group equation is

\sum_{g\in\mathcal N}t(g)\cdot g=g_0,\qquad t(g)\in\mathbb Z_{\ge0},

and $P(\mathcal G,\mathcal N,g_0)$ is the convex hull of its solutions in $\mathbb R^{\mathcal N}$ . A nonnegative integer $t$ is irreducible if any two integer vectors $s,r$ with $0\le s,r\le t$ and $\sum s(g)\cdot g=\sum r(g)\cdot g$ are equal.

The group costs are $c^*(g)=\min_{i:\,fN_i=g}c^*_{m+i}$ . Problem (8) minimizes $\sum_g c^*(g)t(g)$ over the solutions of the group equation. A corresponding vertex of a point $t^*$ (Remark 1) is a nonnegative integer $x_N^*$ with three properties: $t^*(g)=\sum_{i:\,fN_i=g}x^*_{m+i}$ ; at most one positive $x^*_{m+i}$ per group element; and $x^*_{m+i}=0$ when $fN_i=\bar0$ . It uses only least cost columns when $x^*_{m+i}>0$ only if $c^*_{m+i}=c^*(fN_i)$ .

The cone $K_B=\{y\in\mathbb R^m:B^{-1}y\ge0\}$ is where $B$ is LP-optimal. $K_B(d)$ is the set of its points at Euclidean distance at least $d$ from its frontier, and $l_{\max}$ is the largest Euclidean length of a column $N_i$ .

Formalization targets

Goal: THEOREM 4 (p. 462)

If $b\in K_B\bigl(l_{\max}(D-1)\bigr)$ , $t^*$ is a vertex of $P(\mathcal G,\mathcal N,fb)$ minimizing (8), and $x_N^*$ is a corresponding vertex using only least cost columns, then

x^*=\bigl(B^{-1}(b-Nx_N^*),\ x_N^*\bigr)\ \text{is an optimal integer solution of (2)}.

Milestones

THEOREM 1 (p. 459): an irreducible $t$ satisfies $\prod_{g\in\mathcal N}(1+t(g))\le|\mathcal G|$ .
p. 459: $|M(I)/M(B)|=|\det B|$ .
THEOREM 2 (p. 460): every vertex of $P(\mathcal G,\mathcal N,g_0)$ is an irreducible integer point.
Proof of THEOREM 4 (p. 462): an irreducible $t$ has $\sum_g t(g)\le|\mathcal G|-1$ .
THEOREM 3 (p. 461): a corresponding vertex of a minimizing vertex is optimal for (2) whenever $B^{-1}(b-Nx_N^*)\ge0$ .
Proof of THEOREM 4: $\|Nx_N^*\|\le l_{\max}(D-1)$ .
Proof of THEOREM 4: $y\in K_B(d)$ and $\|v\|\le d$ imply $y-v\in K_B$ .
Display (10), p. 464: the optimal $x^*$ of THEOREM 4 satisfies $\prod_{i=1}^n(1+x^*_{m+i})\le D$ .

Significance

THEOREM 4 explains why integer programs with large right-hand sides are often easy. For $b$ outside a band of width $l_{\max}(D-1)$ along the boundary of the cone $K_B$ , the integer optimum is the LP solution $B^{-1}b$ plus a correction that depends only on the class of $b$ modulo the lattice of $B$ . That correction is periodic in $b$ and can be tabulated once for the $D$ group elements. The vertex form adds a structural statement: the correction can be read off a vertex of the corner polyhedron, so the faces and vertices of corner polyhedra (the subject of the rest of the paper) bear directly on integer programming. Display (10) shows such optimal solutions are small: their nonbasic parts satisfy $\prod(1+x_{m+i})\le D$ .

All results here are proved in the paper. None of them is formalized yet. The 1965 version of the asymptotic theorem, posed as THEOREM 1 of the mission on Gomory (1965), is in the same family of statements. Its hypothesis is that the group solution is optimal; here the hypothesis is that it is a vertex of $P(\mathcal G,\mathcal N,g_0)$ . Its counting lemma (a short optimal group solution) and its bound $\|Ny\|\le(D-1)l$ have counterparts in milestones 4 and 6.

Difficulty

An optimal solution of the group problem need not be short. Group solutions can be made longer without changing their cost (add a zero-cost cycle), and a long nonbasic part $x_N$ can push $b-Nx_N$ out of the cone $K_B$ , making $x_B$ negative. The goal must therefore use the vertex hypothesis. Vertices are irreducible (THEOREM 2), and irreducibility bounds their size through a pigeonhole count in the finite group (THEOREM 1). The formal work is spread across three settings: the convex geometry of the hull of an infinite integer set, the arithmetic of the quotient $\mathbb Z^m/B\mathbb Z^m$ and its order, and the linear algebra connecting $B^{-1}$ , the cone $K_B$ and its frontier.

Formalization scope

Vectors on $\mathcal N$ are functions on the subtype of a Finset of the group. Integer solutions are $\mathbb N$ -valued, and $P(\mathcal G,\mathcal N,g_0)$ is convexHull ℝ of their real images. THEOREMS 1 and 2 are stated for an arbitrary finite Abelian group and any finite $\mathcal N$ not containing $0$ , as in the paper. The integer program uses the basis as the first $m$ columns, Fin m ⊕ Fin n. $B^{-1}$ is the real matrix inverse, and every statement assumes $\det B\ne0$ . Optimality of $x$ means feasibility plus $c\cdot y\le c\cdot x$ for every feasible integer $y$ ; no supremum is taken. The loose phrases of the paper are read as follows.

"Vertex" means an extreme point.
"Every vertex is irreducible" means every vertex is the image of an integer solution, and that solution is irreducible.
"Optimal linear programming basis" means $B^{-1}b\ge0$ and $c^*\ge0$ .
"Corresponding vertex $x^*$ of $P_x(B,N,b)$ " means conditions (i)–(iii) of Remark 1, which the paper calls easily verified, taken as the definition.
"Minimizing (8)" means minimizing over the integer solutions of the group equation.
"Euclidean distance from the frontier" is explicit: $\sqrt{\sum_k v_k^2}$ , frontier in the usual topology, so $K_B(0)=K_B$ .

The printed slip on p. 462 ( $\sum(1+t^*(g))$ for THEOREM 1's product) is corrected in the Lean. Dropping the vertex hypothesis from the goal is not a valid formalization (the statement becomes false in general), and neither is defining irreducibility with real $r,s$ (THEOREM 1 then fails). The existence of a minimizing vertex, which the paper takes for granted, is not posed.

A complete development needs the finiteness and order of $\mathbb Z^m/B\mathbb Z^m$ (Mathlib's AddSubgroup.index_eq_natAbs_det), extreme points of convex hulls (extremePoints_convexHull_subset), and an argument that a closed cone with $y$ deep inside it contains the ball around $y$ . The group-polyhedron definitions and THEOREMS 1–2 apply to any finite Abelian group and are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. https://doi.org/10.1016/0024-3795(69)90017-2
R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Nat. Acad. Sci. USA 53 (1965), 260–265. https://doi.org/10.1073/pnas.53.2.260
R. E. Gomory, Faces of an integer polyhedron, Proc. Nat. Acad. Sci. USA 57 (1967), 16–18. https://doi.org/10.1073/pnas.57.1.16
B. L. van der Waerden, Modern Algebra, English translation of the 2nd German edition, Ungar, New York, 1949–1950 (computation of $f$ , cited p. 456).

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems VIII: Single-Controller Stochastic Games — a Dual Pair of Linear Programs Gives the Value and Stationary Optimal PoliciesTextbook

Motivation

A two-person zero-sum stochastic game (also called a Markov game) is a Markov decision problem with two decision makers who pull in opposite directions: at every time point both players choose an action simultaneously, one player pays the other, and the system moves to a random next state whose law depends on the current state and both actions. Stochastic games were introduced by Shapley (Shapley 1953) and are the standard model for adversarial sequential decisions in operations research, economics and computer science (pursuit–evasion, inspection, robust control against an adversarial environment).

Shapley proved that a discounted stochastic game has a value and that both players have stationary optimal policies. The value, however, is in general not computable by linear programming: it need not lie in the field generated by the data. Kallenberg's Example 6.2.1 (after Parthasarathy and Raghavan) has rational data and an irrational value in one state. When only one player controls the transition probabilities, the situation changes: the value and stationary optimal policies are the optimal solutions of one pair of dual linear programs (Parthasarathy & Raghavan, as cited in Kallenberg 1983, pp. 192 and 196; Kallenberg 1983, Chapter 6).

Timeline.

1953: Shapley proves existence of the value and of stationary optimal policies for the discounted game.
1977–1978: Parthasarathy and Raghavan study games in which one player controls the transitions and identify an order-field property for the value and optimal decision rules (cited in Kallenberg 1983, pp. 192, 196).
1983: Kallenberg presents the dual pair (6.2.1)/(6.2.2), with the controlling player's policy read off the dual and the opponent's from the primal, and a constructive existence proof (Remark 6.2.2).

Setting

The state space is $E = \{1,\dots,N\}$ with $N>0$ . In state $i$ player I chooses an action $a$ from a finite nonempty set $A(i)$ and player II an action $b$ from a finite nonempty set $B(i)$ . Player I then receives $r_{iab}$ from player II, and the next state is $j$ with probability $p_{iabj} \ge 0$ , where $\sum_j p_{iabj} \le 1$ .

A history at time $t$ is $(i_1,a_1,b_1,\dots,i_{t-1},a_{t-1},b_{t-1},i_t)$ . A policy $R_1$ of player I chooses, at each time and history, a probability distribution on $A(i_t)$ ; policies $R_2$ of player II are defined likewise. A policy is stationary, written $\pi^\infty$ or $\rho^\infty$ , if the distribution depends only on the current state. With $v_i^t(R_1,R_2)$ the expected reward in period $t$ from initial state $i$ , the total reward is $v_i(R_1,R_2) = \sum_{t\ge1} v_i^t(R_1,R_2)$ .

A pair $(R_1^*,R_2^*)$ is optimal if, componentwise,

v(R_1,R_2^*) \le v(R_1^*,R_2^*) \le v(R_1^*,R_2) \qquad\text{for all policies } R_1,R_2, \tag{6.1.1}

and then $\mathrm{val(TMG)} := v(R_1^*,R_2^*)$ is the value of the game.

Assumption 6.2.1 (contraction). There are $\mu \gg 0$ and $\alpha\in[0,1)$ with $\sum_j p_{iabj}\mu_j \le \alpha\mu_i$ for all $i$ , $a\in A(i)$ , $b\in B(i)$ . The discounted game is the case $\mu = e$ .

Assumption 6.2.2 (single controller). $p_{iabj}$ does not depend on $b$ ; it is written $p_{iaj}$ .

For a stationary $\rho$ write $r_{ia}(\rho) = \sum_b r_{iab}\rho_{ib}$ and $p_{iaj}(\rho)=\sum_b p_{iabj}\rho_{ib}$ . A vector $y$ is TMG-superharmonic if some stationary $\rho^\infty$ of player II satisfies $y_i \ge r_{ia}(\rho) + \sum_j p_{iaj}(\rho) y_j$ for all $a\in A(i)$ , $i\in E$ . For weights $\beta_j>0$ the two linear programs are

\min\Big\{\textstyle\sum_j\beta_jy_j \ \Big|\ \sum_j(\delta_{ij}-p_{iaj})y_j-\sum_b r_{iab}\rho_{ib}\ge0;\ \sum_b\rho_{ib}=1;\ \rho_{ib}\ge0\Big\} \tag{6.2.1}

\max\Big\{\textstyle\sum_iz_i \ \Big|\ \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=\beta_j;\ -\sum_a r_{iab}x_{ia}+z_i\le0;\ x_{ia}\ge0\Big\} \tag{6.2.2}

Formalization targets

Goal: Theorem 6.2.3

Under Assumptions 6.2.1 and 6.2.2, let $(y^*,\rho^*)$ and $(x^*,z^*)$ be optimal solutions of (6.2.1) and (6.2.2), and $\pi^*_{ia} := x^*_{ia}/\sum_a x^*_{ia}$ . Then

v(R_1,(\rho^*)^\infty) \le v((\pi^*)^\infty,(\rho^*)^\infty) = y^* \le v((\pi^*)^\infty,R_2)\qquad\text{for all policies } R_1,R_2 .

The goal fixes no constants; it states that the LP pair produces the value and optimal stationary policies.

Milestones

Theorem 6.2.1 (Shapley): under Assumption 6.2.1 both players have stationary optimal policies.
Theorem 6.2.2: under Assumption 6.2.1, $\mathrm{val(TMG)}$ is the smallest TMG-superharmonic vector.
Theorem 6.2.4 (i): for a stationary $\pi^\infty$ of player I, $x_{ia}(\pi) = [\beta^T(I-P(\pi))^{-1}]_i\pi_{ia}$ and $z_i(\pi) = \min_{b} r_{ib}(\pi)\sum_a x_{ia}(\pi)$ give a feasible point of (6.2.2) with $\sum_i z_i(\pi) = \min_\rho \sum_j\beta_j v_j(\pi^\infty,\rho^\infty)$ .
Theorem 6.2.4 (ii): every feasible $(x,z)$ of (6.2.2) has $x = x(\pi)$ and $z\le z(\pi)$ for $\pi_{ia} = x_{ia}/\sum_a x_{ia}$ .

Theorems 6.2.1 and 6.2.2 hold for the general contracting game. Assumption 6.2.2 enters only from (6.2.1) on.

Significance

The result. Theorem 6.2.3 turns a single-controller game into a finite computation, Algorithm XXVII: solve one LP pair and read off the value and optimal stationary policies of both players. A consequence (Remark 6.2.1) is that the value and the optimal decision rules lie in the field generated by the rewards and transition probabilities. Example 6.2.1 shows this fails without Assumption 6.2.2. Theorem 6.2.4 matches the feasible points of the dual program with the stationary policies of the controlling player. This is the game version of the correspondence between state-action frequencies and policies in Markov decision problems.

Formalizing it. All results are proved in the book, and Theorem 6.2.1 is classical. None of them is formalized: the platform has turn-based stochastic games with positional strategies (TBSGStrategyIteration), which do not cover simultaneous moves or history-dependent randomized policies. The mission adds a reusable model of simultaneous-move stochastic games with history-dependent policies, together with machine-checked optimality of the LP solution against every such policy.

Difficulty

There are two difficulties. First, optimality in (6.1.1) is against every history-dependent randomized policy of the opponent, while the LP produces only stationary policies. Fixing one player's stationary policy reduces the game to a Markov decision problem for the other player (Remark 6.1.1), and the facts needed from that problem (stationary policies suffice, and the value is the smallest superharmonic vector) are theorems about contracting MDPs, not consequences of the LP. Second, Theorem 6.2.2 rests on Shapley's existence theorem, which is not a linear-programming fact: its usual proof is a fixed-point argument for the Shapley operator built from one-stage matrix games. Remark 6.2.2 indicates a route that avoids it, through the bounded polytope of state-action frequencies of a contracting MDP. Either way, LP duality alone does not give optimality against non-stationary opponents.

Formalization scope

Model. $E$ is Fin N with $N>0$ . Actions live in finite types α, β, and $A(i)$ , $B(i)$ are nonempty Finsets. Rows are substochastic.
Policies. A history in $H_{n+1}$ is a record of $n+1$ states and $n$ actions of each player. A policy is a family of distributions indexed by time and history, supported on the current action set. Stationary policies are the image of state-dependent decision rules.
Probabilities and reward. History probabilities are explicit finite products, with no measure theory. The total reward is the tsum of the period rewards, which converges absolutely under Assumption 6.2.1, and every theorem assumes it.
Linear programs. Their variables are functions on all actions that vanish off $A(i)$ (resp. $B(i)$ ). Optimality means feasible and attaining the min/max over the feasible set. The common $p_{iaj}$ is $p_{iab_0j}$ for a fixed $b_0\in B(i)$ , and Assumption 6.2.2 makes the choice irrelevant. $\beta_j>0$ is a hypothesis, as on p. 194.
The minimum in Theorem 6.2.4 (i) is over stationary policies of player II and is stated with attainment.

Restricting either player's policy class to stationary policies would make the optimality claims of Theorems 6.2.1 and 6.2.3 a statement about a finite family and is ruled out: the comparison class is all history-dependent randomized policies.

Lemma 6.1.1 is Mathlib's isSaddlePointOn_value (Mathlib/Order/SaddlePoint.lean) and is not restated. The LP duality theorems of Chapter 1 are proved on the platform (LinearOptimization.lp_strong_duality, lp_complementary_slackness) and may be used. Useful contributions include: the reduction of Remark 6.1.1 (a fixed stationary opponent gives an MDP), the contracting-MDP facts it needs, and a proof of Theorem 6.2.1. The model definitions are reusable for any finite stochastic game.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 6. https://ir.cwi.nl/pub/13008
L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
T. Parthasarathy and T. E. S. Raghavan, Finite algorithms for stochastic games, International Conference on Dynamic Programming, Vancouver, 1977; cited in Kallenberg 1983, p. 232. https://ir.cwi.nl/pub/13008
T. Parthasarathy and T. E. S. Raghavan, An order field property for stochastic games when one player controls the transition probabilities, Game Theory Conference, Cornell, 1978; cited in Kallenberg 1983, p. 233. https://ir.cwi.nl/pub/13008

7 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems II: An Extreme Optimal Solution of the Dual Linear Program Yields a Pure Stationary Policy Optimal among Transient PoliciesTextbook

Why optimize only transient policies?

A Markov decision model describes a system that repeatedly occupies a state, receives a reward when an action is chosen, and then moves according to action-dependent probabilities. Termination may occur after any action. In a model with signed rewards, a policy that continues indefinitely can have a different total-reward behavior from one that eventually leaves the active states. Section 3.3 of Kallenberg's 1983 monograph therefore asks for the best policy within the transient class. The restriction occurs naturally in stopping problems: a decision maker may continue for a while, but the expected number of visits to each active state must remain finite.

The chapter relates that policy problem to a finite linear program. The central question is stronger than finding a policy with a large average over initial states. It asks for one policy that is optimal from every initial state among all transient policies, including policies that randomize and use the entire observed history. Kallenberg's Theorem 3.3.5 says that an extreme optimal point of the program identifies such a policy, and that the policy can be pure and stationary. Theorem 3.3.5, p. 57.

The finite model and its policies

Let $E=\{1,\ldots,N\}$ be a nonempty finite state set. Each state $i$ has a finite nonempty set $A(i)$ of available actions. If action $a\in A(i)$ is selected, the system earns the real reward $r_{ia}$ and then moves to $j$ with probability $p_{iaj}\ge0$ . The row sum $\sum_jp_{iaj}$ is at most one; any missing mass represents termination. Action sets can differ across states. These are the conventions of Section 2.2, pp. 19–20.

A policy $R$ selects an action distribution at each decision epoch. It may depend on the entire state-action history. A Markov policy depends only on time and the current state; a stationary policy uses the same state-dependent distribution at every time; a pure stationary policy selects one action $f(i)\in A(i)$ in each state. These four classes are denoted $C$ , $C_M$ , $C_S$ , and $C_D$ . The first decision occurs at time $t=1$ in the book.

Write $\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ for the chance of being in state $j$ and choosing action $a$ at time $t$ , given initial state $i$ . A policy is transient if the expected number of visits to each state is finite from every initial state:

\sum_{t=1}^{\infty}\mathbb P_R(X_t=j\mid X_1=i)<\infty\qquad(i,j\in E).

For such a policy, its expected total reward $v_i(R)$ is finite. Section 3.3 assumes that at least one transient policy exists. Its transient value is $w_i=\sup\{v_i(R):R\text{ transient}\}$ , which can still be infinite as the policy varies. Section 2.2, pp. 21–23; §3.3, pp. 49–50.

Formalization targets

Fix positive weights $\beta_j>0$ . The linear program (3.3.7) maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative state-action arrays satisfying the flow equations

\sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}=\beta_j\qquad(j\in E).

Its feasible set is $P$ . A transient stationary rule $\pi$ has an occupation vector $x(\pi)$ , where $x_{ia}$ is the $\beta$ -weighted expected number of visits to state-action pair $(i,a)$ . Theorem 3.3.3 identifies transient stationary rules bijectively with $P$ and identifies extreme points with pure rules. Theorem 3.3.4 compares the occupation sets of all four policy classes: $\overline{K(D)}\subset K(S)=K(M)=K=P$ , where the bar means closed convex hull. Theorems 3.3.3–3.3.4, pp. 54–55.

The goal is Theorem 3.3.5, p. 57. If $x^*$ is an extreme optimal solution of that program and $f_*(i)$ is the action with $x^*_{i f_*(i)}>0$ , then the pure stationary policy $f_*^\infty$ is transient and

v_i(R)\le v_i(f_*^\infty) \qquad\text{for every transient policy }R\text{ and every }i\in E.

A stronger companion statement is Theorem 3.3.6, p. 58: under the correspondence of Theorem 3.3.3, a stationary policy is optimal transient exactly when its occupation vector is optimal for (3.3.7), in the two directions printed on the page. The milestone list follows the chapter's numbered results on the finite-value Bellman equation, the smallest superharmonic vector, the stationary-policy/LP correspondence, the four occupation sets, and the preservation of optimality. The goal itself does not assume that $w$ is finite; the existence of an extreme LP optimum is its stated premise.

What the result gives

An LP optimum is a vector of occupation amounts, not an implementable policy by itself. Theorem 3.3.5 converts an extreme optimum into an action choice at each state. It also upgrades a scalar objective weighted by $\beta$ to simultaneous optimality of the resulting policy from every initial state. This is the bridge between the finite optimization problem and the original control problem. The scope is specifically transient optimality: Example 3.3.4, p. 58 gives a policy outside that comparison class with larger total reward.

The result is proved in the book. The work here is to give its model, occupation map, linear program, and numbered supporting statements precise Lean interfaces that can later receive machine-checked proofs. The reusable parts include finite substochastic MDP data, history-dependent policy semantics, transient visit sums, and state-action occupation vectors. The theorem proofs are open in this proposal.

Where the difficulty lies

Optimizing a weighted sum of rewards is not, by itself, the same as optimizing every state's reward. The linear program also describes flows of expected visits, while the theorem talks about actual policies and all initial states. A solver must account for both links without assuming that all policies are stationary. The geometry of an extreme feasible point matters because the theorem selects an action from each state using a positive coordinate. Existence of a transient policy does not by itself bound the supremum of transient rewards; Example 3.3.1, p. 50 makes that distinction explicit.

Formalization scope

Lean uses Fin N with $N>0$ for states and a finite action type with a state-dependent finite nonempty available-action set. Only available state-action pairs index occupation vectors and LP variables. Transition rows are substochastic, not necessarily stochastic. Rewards are real and may have either sign. A general policy is a normalized action kernel on full finite histories; its Markov, stationary, and pure stationary subclasses remain distinct. The history list is stored newest first, and Lean's time index zero corresponds to the book's time one. All state-action probabilities are finite sums over histories; transience is summability of state-visit probabilities, and occupation counts are infinite sums used under that condition.

The LP flow constraints are equalities and $\beta$ is strictly positive. The goal does not normalize $\beta$ to a probability distribution, matching (3.3.7); Theorem 3.3.4 uses the initial-distribution convention of p. 55 and hence normalizes it. Theorem 3.3.3 uses the matrix inverse $(I-P(\pi))^{-1}$ only for transient stationary rules. For Theorems 3.3.1–3.3.2, nonemptiness of the transient class and boundedness above of each transient reward set make the real supremum meaningful. Theorem 3.3.5 uses neither boundedness as an extra hypothesis nor a restriction of the comparison class to stationary policies. A formalization that compares $f_*^\infty$ only with stationary (or Markov) policies, or that identifies the classes $C$ , $C_M$ , $C_S$ , $C_D$ , would make Theorems 3.3.4 and 3.3.5 much weaker or trivial, and is ruled out: the comparison class is every history-dependent randomized transient policy. Mathlib's finite sums, matrices, summability, convex hull, and extreme-point definitions provide the general library interface. Contributions establishing the policy/occupation identities and the chapter's numbered milestones are within scope.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, §§2.2 and 3.3, pp. 19–23 and 49–60. Publisher repository.

9 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Outline of an Algorithm for Integer Solutions to Linear Programs: The Fractional Cut (3) Cuts Off the Simplex Solution but Keeps Every Nonnegative Integer Solution and the Integer Maximum of wResearch Paper

Motivation

Integer linear programming asks for the best point whose coordinates are integers, even though linear programming methods naturally search over real points. In his 1958 note, Gomory describes a systematic way to add a constraint that excludes a fractional simplex solution while retaining every nonnegative integer solution. This mission isolates that single cut and its effect on the objective value. The note announces an iterative finite algorithm, but explicitly defers a proof of finiteness to another treatment. The target here is the cut's correctness for one tableau.

The cut belongs to the history of cutting plane methods for integer programs. Related formalized objects include a Chvátal closure and intersection cuts based on lattice free sets, but their data and cut constructions differ from the row and fractional part formula in Gomory's note. The note itself contrasts its systematic row operation with earlier problem specific constraints used by Dantzig, Fulkerson, and Johnson and by Markowitz and Manne. Those comparisons explain why a reusable row formula is useful; they do not assert an identity between the different cuts.

Setting

A tableau is a finite array of real numbers $a'_{i,j}$ . Row $0$ represents the objective variable $w$ ; rows $1,\ldots,m$ represent $x'_1,\ldots,x'_m$ . Column $0$ holds constants; columns $1,\ldots,n$ multiply the negatives of the variables $t'_1,\ldots,t'_n$ . A solution of (2) is a pair $(x',t')$ satisfying

x'_i=a'_{i,0}+\sum_{j=1}^{n}a'_{i,j}(-t'_j),\qquad 0\le i\le m.

The original integer program requires $w=x'_0$ , every $x'_i$ , and every $t'_j$ to be nonnegative integers. The simplex solution of this tableau has $t'=0$ and $x'_i=a'_{i,0}$ . It is a real tableau solution, whether or not any of its coordinates are integers.

Choose a row $i_0$ whose constant $a'_{i_0,0}$ is not an integer. For each coefficient let $n'_{i_0,j}=\lfloor a'_{i_0,j}\rfloor$ be the greatest integer at most that coefficient, and let $f'_{i_0,j}=a'_{i_0,j}-n'_{i_0,j}$ be its fractional part. Equation (3) defines a new variable

s_1=-f'_{i_0,0}-\sum_{j=1}^{n}f'_{i_0,j}(-t'_j).

The augmented system (2)* adds this equation to the tableau. Feasibility now also requires $s_1\ge0$ ; an integer solution additionally requires $s_1\in\mathbb Z$ . For example, the one row relation $x'=\tfrac12-\tfrac12t'$ admits the integer solution $(x',t')=(0,1)$ , and its cut value is $s_1=0$ . At the simplex point $t'=0$ , the same cut value is $-\tfrac12$ .

Formalization targets

Fractional cut and integer optimum

The main target combines exclusion of the simplex solution, exact correspondence of nonnegative integer solutions, and equality of their attained objective values. Writing $\mathcal I_2$ and $\mathcal I_{2^*}$ for the two sets of nonnegative integer solutions, the correspondence is

(x',t')\in\mathcal I_2\quad\Longleftrightarrow\quad (x',t',s_1(x',t'))\in\mathcal I_{2^*}.

Every member of $\mathcal I_{2^*}$ has the displayed cut value for $s_1$ , and the projection that drops $s_1$ leaves $w$ unchanged. Consequently a real $W$ is the greatest attained $w$ value for (2) exactly when it is the greatest attained value for (2*). The statement does not assume either set has a maximum.

Supporting claims

The milestones follow the paragraphs on page 277: projection of feasible solutions, the impossibility of integer solutions when the selected row has a fractional constant but only integral other coefficients, exclusion of the simplex point, the identity proving $s_1$ integral, and its nonnegativity on integer solutions. These are the claims the note uses to pass from the cut formula to the correspondence and the objective statement.

Significance

The result certifies that equation (3) removes the current fractional simplex point while retaining every integer candidate and its objective value. It is the local correctness condition needed before one can safely reoptimize an integer program after adding this constraint. The note's argument is a mathematical result about one tableau, independent of whether the subsequent sequence of pivots terminates.

This mission supplies a machine checkable interface for the tableau, the fractional cut, and the projection between their integer feasible sets. The theorem statements are drafted and compile with open proofs; this mission does not claim that the paper's result already has a machine checked proof here. A completed proof would make the one cut result available for later developments about iterations, optimization, or stronger cut families.

Difficulty

The cut value is visibly at least $-f'_{i_0,0}$ when the nonbasic variables are nonnegative, but that inequality alone does not give $s_1\ge0$ : the right side is negative for the chosen row. The key additional statement is that the real expression for $s_1$ is an integer on an integer tableau solution. Formalization must preserve both facts while using the same sign convention for the tableau and the cut. Merely defining the augmented solution as a pair together with its computed cut value would make the correspondence automatic and would omit the new variable's integrality and nonnegativity requirements.

Formalization scope

Lean uses real valued tableau coefficients and real valued variables with a separate predicate for being an integer. This lets the fractional simplex point and integer feasible points inhabit the same space. The row and column sets are finite, including the cases $m=0$ and $n=0$ ; row $0$ is $w$ , column $0$ is the constant column, and Lean's Fin n index $j$ denotes the paper's $t'_{j+1}$ . The selected row can be row $0$ in Lean. Gomory chooses a constraint row, but the local cut argument needs only the selected row's variable to be integral, and $w$ is integral in the stated problem. Every variable, including $w$ and the added $s_1$ , is required to be nonnegative and integral in an integer solution.

The fractional part uses the greatest integer at most a real number, including negative coefficients. The objective comparison uses greatest elements of the sets of attained $w$ values, so empty and unbounded sets receive no artificial supremum. Nonnegative constants and objective row coefficients are features of the simplex setting, but the five local claims and goal remain valid without those extra hypotheses. The paper's loose phrases “cuts off,” “one-one correspondence,” and “can be replaced” are represented by infeasibility of the augmented simplex point, a unique extension and projection preserving $w$ , and equivalence of greatest attained $w$ values, respectively.

The mission does not formalize the derivation of (2) from (1) by simplex pivots, dual simplex reoptimization, finiteness of repeated cutting, the $m+n+2$ equation bound and deletion of re-entering $s$ variables, the suggested choice of largest fractional part, or the reported E101 runs. These concern an iterative process the note does not define fully, or empirical observations. Reusable contributions include a verified fractional part identity, the integer extension theorem, and solution set correspondence for a real tableau.

Selected references

Ralph E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the American Mathematical Society 64(5), 1958, 275–278. DOI: 10.1090/S0002-9904-1958-10224-4.
George B. Dantzig, R. Fulkerson, and S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 1954, 393–410. DOI: 10.1287/opre.2.4.393.

7 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems I: Five Equivalent Characterizations of a Transient Markov Decision Problem, among Them Contraction and a Finite Linear ProgramTextbook

Motivation

Finite Markov decision models are often described by policies that choose an action from the current state. The admissible class in a total reward problem is wider: a randomized decision may use the complete history of observed states and chosen actions. For an undiscounted infinite horizon, the expected number of visits to a state may be infinite, and the total reward may be an extended real number. It matters whether a test carried out on finitely many pure stationary policies really controls this wider class. Kallenberg's Section 3.2 answers that question for finite models whose transition rows may lose probability mass when the process terminates.

The chapter is part of a 1983 account of linear programming methods for finite Markovian control. Its Theorem 3.2.4 collects earlier characterizations of transience and relates them to a finite linear program. The historical attribution in Kallenberg's Remark 3.2.2 is precise: Veinott (1969) established the equivalence of the first three conditions for nonrandomized policies, Hordijk (1976, course notes) extended the first four to general policies, and Denardo and Rothblum (1979) established the link between pure stationary transience and the LP condition. The mission targets Kallenberg's combined five-way statement, rather than treating those partial precedents as separate conclusions. Kallenberg, pp. 42–43.

Setting

Let $E$ be a finite nonempty state space of size $N$ . For every state $i$ , let $A(i)$ be a nonempty finite set of actions. Choosing $a\in A(i)$ gives the transition number $p_{iaj}\ge0$ to state $j$ , with $\sum_jp_{iaj}\le1$ . The missing mass is the probability that the system terminates before another decision epoch. This is a substochastic model; replacing the inequality by equality would change the question. Kallenberg, §2.2.

A policy $R$ specifies, at each epoch $t\ge1$ , a probability distribution on $A(i_t)$ after the full history $(i_1,a_1,\ldots,a_{t-1},i_t)$ . It may be randomized and may depend on all preceding states and actions. A memoryless policy depends only on the epoch and current state. A pure stationary policy $f^\infty$ chooses a single admissible action $f(i)$ in state $i$ at every epoch. Write $P_R(X_t=j\mid X_1=i)$ for the probability of state $j$ at epoch $t$ from initial state $i$ . The policy is transient when $\sum_{t\ge1}P_R(X_t=j\mid X_1=i)<\infty$ for every pair $i,j$ . Kallenberg, pp. 20–23.

The finite-horizon survival recursion starts from $y_i^0=1$ and sets $y_i^t=\max_{a\in A(i)}\sum_jp_{iaj}y_j^{t-1}$ for $t\ge1$ . A model is contracting if there is a strictly positive vector $\mu$ and a scalar $0\le c<1$ for which $\sum_jp_{iaj}\mu_j\le c\mu_i$ for every admissible $(i,a)$ . These objects are determined by the transition system; rewards do not enter the five-way characterization. Kallenberg, p. 23 and pp. 41–43.

Formalization targets

Five equivalent conditions

For any fixed $\beta_j>0$ , Theorem 3.2.4 states the equivalence of: transience of every pure stationary policy; transience of every policy; $\max_i y_i^N<1$ ; contraction; and existence of a finite solution of

\max\left\{\sum_{i\in E}\sum_{a\in A(i)}x_{ia}:\ \sum_{i\in E}\sum_{a\in A(i)}(\delta_{ij}-p_{iaj})x_{ia}\le\beta_j\ (j\in E),\quad x_{ia}\ge0\right\}.

“Finite solution” means an attained finite optimum. The $\beta_j$ are arbitrary positive right-hand sides, not a choice that the theorem is allowed to make after seeing the model. The state count $N$ is the exponent in $y^N$ , and the inequality is strict. Kallenberg, Theorem 3.2.4, pp. 42–43.

Supporting targets

The milestones follow the results the chapter uses on the way to Theorem 3.2.4, in attack order:

Theorem 2.5.1 (Derman–Strauch) and its Corollary 2.5.1: for a fixed initial distribution, a memoryless policy reproduces the state-action probabilities $P_R(X_t=j,Y_t=a\mid X_1=i)$ of any policy or of any countable mixture of policies.
Lemma 3.2.1: under Assumption 3.2.1, $\lim_{\alpha\uparrow1}v_i^\alpha(R)=v_i(R)$ in $[-\infty,+\infty]$ .
Theorem 3.2.1: under Assumption 3.2.1 there is a pure stationary policy $f^\infty$ with $v(f^\infty)=v$ , where $v_i=\sup_Rv_i(R)$ .
Theorem 3.2.2: if $v$ is p-summable, then $v_i=\max_{a\in A(i)}\{r_{ia}+\sum_jp_{iaj}v_j\}$ .
Theorem 3.2.3: if some policy is transient, some pure stationary policy is transient.
Lemma 3.2.2: $y_i^t=\sup_R\sum_jP_R(X_{t+1}=j\mid X_1=i)$ , attained by the policy $(f_t,f_{t-1},\dots,f_1,f_1,\dots)$ built from maximizers of the recursion.

Assumption 3.2.1 says that every policy's expected total reward $v_i(R)=\lim_T\sum_{t\le T}v^t_i(R)$ exists in $[-\infty,+\infty]$ ; it is a hypothesis of items 2–4 only. Kallenberg, pp. 32–33, 37–42.

Significance

The theorem gives four finite or structured ways to recognize a property quantified over all policies. The survival condition uses only $N$ recursion steps, and the contraction condition supplies a weighted geometric bound on continuation. The LP links the same property to a finite-dimensional optimization problem. Each characterization can serve a different later argument without assuming the policy class has been reduced to stationary rules. Kallenberg, Theorem 3.2.4.

The five-way theorem and its supporting results are proved in the book; this mission asks for machine-checked proofs of their stated finite-model versions. The Derman–Strauch policy result is quoted by Kallenberg without proof, so its formal proof is a separate substantial contribution. None of these results has a machine-checked proof yet. The general history and occupancy definitions can be reused by later total-reward and constrained-control missions.

Difficulty

Checking only the finitely many pure stationary transition matrices does not directly bound the occupation counts of a history-dependent policy. Such a policy can change its action distribution after each observed path, and it need not be a mixture of stationary policies chosen once at the start. Likewise, $y_i^N<1$ is a finite-horizon bound, whereas transience is a statement about an infinite series of visit probabilities. The main difficulty is connecting these different quantifiers without changing the policy class. The LP condition adds a second boundary: its constraints use $\le\beta_j$ , and finite value includes attainment. Kallenberg, pp. 41–45.

Formalization scope

States are Fin N with $N>0$ , and actions form one finite ambient type with a nonempty admissible subset $A(i)$ at each state. Transitions are real nonnegative numbers with row sums at most one. Epoch $t=1$ is Lean index zero. A history records states and earlier actions; policy decision rules are normalized and supported on the current state's admissible actions. Occupancies are finite sums of transition products, so the definition of transience is summability of a nonnegative real sequence, not a bound on an individual term.

The reward layer is separate from the transition system. It uses extended real limits under Assumption 3.2.1, while the five-way goal needs no reward hypothesis. Sums $\sum_jp_{iaj}x_j$ of extended reals are only asserted for p-summable $x$ , where no $+\infty$ and $-\infty$ meet with positive coefficients; the convention $0\cdot(\pm\infty)=0$ is the book's. The LP objective and constraints range only over admissible state-action pairs. Its finite-solution predicate includes a feasible optimizer. Contraction allows an arbitrary componentwise positive weight $\mu$ and requires $0\le c<1$ ; it does not normalize $\mu$ to the all-ones vector. The $N$ -step test uses the cardinality of the original state space.

All-policy transience means every history-dependent randomized policy. Restricting that quantifier to Markov or stationary policies would remove the central content of the theorem. Useful contributions include finite-history probability identities, the Derman–Strauch occupancy theorem, the maximal-survival recursion, the stationary total-optimality result, and the finite LP characterization. The occupancy and policy definitions are reusable beyond this mission.

Selected references

L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
C. Derman and R. E. Strauch, A note on memoryless rules for controlling sequential control processes, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699618
A. F. Veinott Jr., Discrete dynamic programming with sensitive discount optimality criteria, Annals of Mathematical Statistics 40 (1969), 1635–1660. https://doi.org/10.1214/aoms/1177697379
E. V. Denardo and U. G. Rothblum, Optimal stopping, exponential utility, and linear programming, Mathematical Programming 16 (1979), 228–244. https://doi.org/10.1007/BF01582110
A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25 (1979), 352–362. https://doi.org/10.1287/mnsc.25.4.352

12 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Linear Programming and Finite Markovian Control Problems III: Contracting Dynamic Programming — Pure, Stationary, Markov and General Policies Span One State-Action Frequency PolytopeTextbook

Motivation

Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).

The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).

Setting

Let $E$ be a nonempty finite set of states. Each $i\in E$ has a nonempty finite action set $A(i)$ . Taking $a\in A(i)$ earns a real reward $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$ . A row may sum to less than one; the missing probability is termination. A policy $R$ specifies a probability distribution over $A(i)$ after every finite history ending in $i$ . A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action $f(i)$ in each state. These are the classes $C$ , $C_M$ , $C_S$ , and $C_D$ of §2.2 (Kallenberg 1983, pp. 19–21).

The standing contraction assumption supplies weights $\mu_i>0$ and $0\le\alpha<1$ with

\sum_{j\in E}p_{iaj}\mu_j\le\alpha\mu_i \qquad(i\in E,\ a\in A(i)).

It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).

For an initial probability distribution $\beta$ , with $\beta_i\ge0$ and $\sum_i\beta_i=1$ , write $x_{ja}(R)$ for the expected total number of visits to state $j$ at which action $a$ is chosen, averaged over the initial state. Let $K$ , $K(M)$ , $K(S)$ , and $K(D)$ collect these frequency vectors for the four policy classes. The frequency polytope $P$ consists of nonnegative vectors $x$ satisfying conservation of expected flow at each state:

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

These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).

Formalization targets

The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every $\beta_i>0$ , and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).

The mission goal allows zero entries in the initial distribution and compares all four policy classes:

\overline{K(D)}=K(S)=K(M)=K=P.

The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, $K(D)$ is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).

Significance

The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over $P$ without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).

The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.

Difficulty

For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of $K$ with $P$ therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When $\beta_j=0$ , different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).

Formalization scope

States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index $n=0$ represents the book's period $t=1$ . The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.

The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.

Selected references

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

6 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

Linear Programming and Markov Decision Chains 3: The Representative of a Pure Stationary Policy Is an Extreme Point of the Dual LPResearch Paper

Linear programs for average-reward Markov decision chains

A Markov decision chain is a controlled Markov chain: in each state the controller picks an action, collects a reward and moves to a random next state with probabilities that depend on the state and the action. Under the average reward criterion, the long-run reward per step, an optimal policy can be computed by linear programming. For chains in which every stationary policy has a single recurrent class (the unichain case) this goes back to Manne (1960), de Ghellinck (1960) and d'Epenoux (1960): the variables of the dual linear program are long-run state–action frequencies, and the vertices of its feasible set are exactly the pure stationary policies.

In the general multichain case a policy may split the state space into several recurrent classes with transient states between them, and the frequency picture breaks down. Denardo and Fox (1968) and Denardo (1970) gave linear programs that require solving several programs in sequence. Hordijk and Kallenberg (Management Science 25(4), 1979) showed that one pair of dual linear programs suffices: from an optimal dual solution one reads off an average optimal policy (their Theorems 7 and 8). To make the correspondence between policies and dual solutions explicit, they attach to every stationary policy a representative, a particular feasible solution of the dual program, and prove (Theorem 10) that the representative of a pure stationary policy is a vertex of the feasible set. This mission formalizes Theorem 10.

Timeline:

1960: Manne; de Ghellinck; d'Epenoux. The linear program for unichain average-reward problems, with pure policies at the vertices.
1962: Blackwell. The limit matrix $P^*$ and deviation matrix $D$ of a finite stochastic matrix, and their identities (Ann. Math. Statist. 33).
1968–1970: Denardo and Fox; Denardo. Multichain problems by a sequence of linear programs.
1979: Hordijk and Kallenberg. A single dual pair for the multichain case; representatives of stationary policies; Theorem 10.

Setting

The state space $E$ is finite. Each state $i$ has a finite nonempty set $A(i)$ of actions; action $a$ in state $i$ earns $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$ , $\sum_j p_{iaj}=1$ . Fix weights $\beta_j>0$ with $\sum_j\beta_j=1$ .

The dual linear program has one pair of variables $x_{ia},y_{ia}$ for each state $i$ and each admissible action $a\in A(i)$ . Its feasible set consists of the $(x,y)$ with

\textstyle\sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\qquad \sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\qquad(j\in E),\qquad x,y\ge 0 .

A pure stationary policy $f^\infty$ uses the action $f(i)\in A(i)$ whenever the chain is in state $i$ . Its transition matrix is $P(f)=(p_{if(i)j})$ . For a stochastic matrix $P$ , the limit matrix $P^*=\lim_n\frac1n\sum_{k=1}^nP^{k-1}$ exists, and the deviation matrix is $D=(I-P+P^*)^{-1}-P^*$ . A state is recurrent if every state reachable from it can reach it back, and transient otherwise; the set $T$ collects the transient states, and the states reachable from a recurrent state form an ergodic set. Write $E_1,\dots,E_m$ for the ergodic sets of $P(f)$ .

The representative of $f^\infty$ is

x_{ia}(f)=[\beta^TP^*(f)]_i\,\delta_{af(i)},\qquad y_{ia}(f)=[\beta^TD(f)+\gamma^TP^*(f)]_i\,\delta_{af(i)},

with $\gamma_l=0$ for $l\in T$ and, for $l\in E_j$ , $\gamma_l=\max_{i\in E_j}\big(-\sum_k\beta_kd_{ki}\big)\big/\sum_{k\in E_j}p^*_{ki}$ . The paper defines the same formulas for randomized stationary policies $\pi$ , with $\pi_{ia}$ in place of $\delta_{af(i)}$ .

Formalization targets

Goal: Theorem 10 (p. 361)

(x(f),y(f))\ \text{is an extreme point of the feasible set of the dual linear program}

for every finite Markov decision chain, every positive probability vector $\beta$ and every pure stationary policy $f^\infty$ . The statement contains feasibility of the representative.

Milestones

§3.3, pp. 359–360: the representative $(x(\pi),y(\pi))$ of any stationary policy is feasible.
Proof of Theorem 10, p. 362: for a stochastic $P$ , every solution of $x^T(I-P)=0$ , $x^T+y^T(I-P)=\beta^T$ (system (7)) satisfies $x^T=\beta^TP^*$ and $y^T=\beta^TD+y^TP^*$ .
Proof of Theorem 10, p. 362: such a solution has $y_i=(\beta^TD)_i$ for $i\in T$ .
Proof of Theorem 10, p. 362: on each ergodic set $E_k$ of $P(f)$ there is a state $i(k)$ with $y_{i(k)f(i(k))}(f)=0$ .
Proof of Theorem 10, p. 362 (Chung, p. 33): a row vector $z$ with $z_i=\sum_{l\in E_k}z_lp_{li}$ on an ergodic set $E_k$ that vanishes at one state of $E_k$ vanishes on all of $E_k$ .

Significance

Theorem 10 is the vertex half of the policy–solution correspondence of Hordijk and Kallenberg: every pure stationary policy appears as a basic feasible solution of one linear program, in the multichain case and without any communication assumption. It connects the simplex method on that program with the set of pure policies, and it is a building block for the later literature on linear programming for multichain Markov decision problems. The paper also records that the converse fails: an extreme point may induce a randomized policy.

The result is proved in the paper. As far as is known it has not been machine-checked. A formal proof also checks the exact form of $\gamma$ : the paper prints the denominator of $\gamma_l$ as $\sum_k p^*_{ki}$ , a sum over all states, and with that reading the representative is not feasible as soon as transient states feed an ergodic set (two states, $0\to1\to1$ : $y_1=-\beta_0/2$ ). The denominator $\sum_{k\in E_j}p^*_{ki}$ is the one the paper's own feasibility computation on p. 360 uses, and it is the one stated here.

Difficulty

Feasibility is a calculation with the identities $PP^*=P^*P=P^*P^*=P^*$ and $(I-P)D=I-P^*$ . Extremality is the substance. Restricted to the pairs $(i,f(i))$ , the constraints become the square system (7) in the state variables, and system (7) determines $x$ and the transient part of $y$ , but on each ergodic set it determines $y$ only up to adding a multiple of the stationary distribution of that class: the matrix $I-P$ is singular, with one degree of freedom per ergodic set. The naive argument, that the equality constraints alone pin the point down, therefore fails as soon as there is an ergodic set; the extra information has to come from the nonnegativity constraints, and that is why the exact value of $\gamma$ matters. In the general multichain setting this requires the class structure of a finite Markov chain (closed classes, transient states, the support of $P^*$ , uniqueness of invariant vectors on a closed communicating class), little of which is in Mathlib in usable form.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP: finite states, finite actions, admissible sets $A(i)$ (nonempty), transition probabilities nonnegative with unit row sums. $P^*$ and $D$ are the published limitMatrix and deviationMatrix of Blackwell's Lemma 1, whose identities are the open platform theorems BlackwellDiscreteDP.NearOne.lemma_1a and lemma_1d.
The dual variables are functions on the subtype of admissible state–action pairs, so non-admissible actions have no coordinates. The feasible set is a subset of $(\mathrm{Pair}\to\mathbb R)\times(\mathrm{Pair}\to\mathbb R)$ and "extreme point" is Mathlib's Set.extremePoints ℝ. Membership in it includes feasibility.
Row vectors act by vecMul. Recurrence and accessibility are the published IsRecurrent and Accessible; the ergodic set of a recurrent $l$ is the set of states accessible from $l$ . The maximum in $\gamma$ is a Finset.sup' over that finite nonempty set.
$\gamma$ uses the corrected denominator $\sum_{k\in E_j}p^*_{ki}$ . A formalization with $\gamma=0$ , or one in which the non-admissible coordinates of the program are free, is a different and false or trivial statement and is ruled out.
Stationary randomized rules are nonnegative weights on $A(i)$ summing to one; the pure rule of $f$ is the indicator of $f(i)$ .
Useful contributions: the class decomposition of a finite stochastic matrix (closed classes, $p^*_{ki}=0$ for transient $i$ , positivity of $p^*_{ii}$ on recurrent states), uniqueness of invariant vectors on a closed communicating class, and proofs of Blackwell's Lemma 1(a), 1(d). All of these are reusable beyond this mission.

Selected references

A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
E. V. Denardo, On Linear Programming in a Markov Decision Problem, Management Science 16(5):281–288, 1970. https://doi.org/10.1287/mnsc.16.5.281
E. V. Denardo and B. L. Fox, Multichain Markov Renewal Programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968. https://doi.org/10.1137/0116038
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259

9 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On Approximate Solutions of Systems of Linear Inequalities: If Ax ≦ b Is Consistent, Every x Has a Solution x₀ with Fₙ(x − x₀) ≦ c·Fₘ((Ax − b)⁺)Research Paper

Motivation

Iterative methods for a system of linear inequalities $Ax\le b$ stop at a vector $\bar x$ that only almost satisfies the system: the violation $(A\bar x-b)^+$ is small but not zero. A user then needs to know that $\bar x$ is close to an actual solution. Hoffman's 1952 paper (J. Res. Nat. Bur. Standards 49) gives the first quantitative form of this fact: the distance from $\bar x$ to the solution set is at most a fixed multiple of the violation. The paper itself names one application: in Brown's method for solving games, the computed strategy vector approaches the set of optimal strategy vectors.

The result is now known as Hoffman's error bound and the constant as the Hoffman constant. It is a standard tool in convergence analysis, sensitivity analysis of linear programs, and the theory of error bounds.

Timeline.

1952: S. Agmon (The relaxation method for linear inequalities, NAML Report 52-27, NBS; later Canad. J. Math. 6, 1954, doi:10.4153/CJM-1954-037-2) proves the two geometric lemmas on which Hoffman's proof rests, and a bound in the Euclidean/max norm setting.
1952: A. J. Hoffman proves the bound for arbitrary positive homogeneous size functions $F_n$ , $F_m$ , and gives explicit constants in the max and sum norms by way of matrix games.
Later work (Robinson 1973; Güler, Hoffman and Rothblum 1995; Peña, Vera and Zuluaga 2021) extends the bound to perturbed systems, characterises the sharp constant, and studies its computation.

Setting

Let $A=(a_{ij})$ be a real $m\times n$ matrix with rows $A_1,\dots,A_m$ and let $b\in\mathbb R^m$ . The system (1) is $A_i\cdot x\le b_i$ for $i=1,\dots,m$ , briefly $Ax\le b$ ; its solution set is $\Omega=\{x : Ax\le b\}$ , and the system is consistent if $\Omega\ne\emptyset$ . The $i$ th half space is $\{x : A_i\cdot x\le b_i\}$ .

For a real number $a$ , $a^+=a$ if $a\ge0$ and $a^+=0$ otherwise; for a vector, $y^+$ is taken coordinatewise. So $(Ax-b)^+$ records by how much $x$ violates each inequality.

Hoffman measures sizes with a positive homogeneous function $F_k$ on $\mathbb R^k$ : a continuous real function with (i) $F_k(x)\ge0$ and $F_k(x)=0$ only for $x=0$ , and (ii) $F_k(\alpha x)=\alpha F_k(x)$ for $\alpha\ge0$ . Norms are examples, but $F_k$ need not be symmetric, subadditive or convex.

For a set $S$ of rows, $M$ is the $m\times n$ matrix obtained from $A$ by replacing the rows outside $S$ by $0$ , and $\bar y$ keeps the coordinates of $y\in\mathbb R^m$ in $S$ and zeroes the others. "Nearest" always refers to Euclidean distance. The set $E$ consists of the points $x$ outside the cone $\{z : Mz\le0\}$ whose nearest point in that cone is the origin; $K'$ is the cone spanned by the rows of $M$ with the origin removed.

Section 3 uses three norms: $|x|$ (largest absolute coordinate), $\|x\|$ (sum of absolute coordinates) and the Euclidean norm. With $g_{ij}=A_i\cdot A_j$ , $a_S$ is the largest absolute coordinate of a row in $S$ , and $v_S=\min_\lambda\max_{i\in S}\sum_{j\in S}g_{ij}\lambda_j$ over probability vectors $\lambda$ on $S$ , the value of the matrix game $(g_{ij})_{i,j\in S}$ .

Formalization targets

Goal: Hoffman's theorem (Section 2, p. 263)

If $Ax\le b$ is consistent and $F_n$ , $F_m$ are positive homogeneous, there is $c>0$ such that for every $x$ some solution $x_0$ satisfies

F_n(x-x_0)\le c\,F_m\bigl((Ax-b)^+\bigr).

The constant is existential and fixed before $x$ ; no value is asserted. This is the weakest statement that carries the content and survives any later improvement of the constant.

Milestones: the proof's lemmas (pp. 263–264)

Lemma 2: if $y$ is the point of $\Omega$ nearest to $x\notin\Omega$ , then $x$ lies outside the intersection $\Omega_S$ of the half spaces active at $y$ , and $y$ is also the point of $\Omega_S$ nearest to $x$ .
Lemma 3: for every set $S$ of rows there is $d_S>0$ with $F_m((Mx)^+)\ge d_S F_n(x)$ for all $x\in E$ .
Lemma 1: there is $e>0$ with $F_m(\bar y)\le e\,F_m(y)$ for all $y$ and all $S$ .
Lemma 4: $K'=E$ .

Milestones: explicit constants (pp. 264–265)

\text{(9)}\quad |x-x_0|\le\frac{a}{v}\,|(Ax-b)^+|\quad\text{if all }A_i\cdot A_j>0,\ v=\min_{i,j}A_i\cdot A_j,\ a=\max_{i,j}|a_{ij}|;

\text{(10)}\quad |x-x_0|\le\frac{a}{w}\,\|(Ax-b)^+\|\quad\text{if } w=\min_i\Bigl(g_{ii}+\sum_{j:\,g_{ij}<0}g_{ij}\Bigr)>0;

\text{(8)}\quad |x-x_0|\le c\,|(Ax-b)^+|,\qquad c=\max_{v_S>0}\frac{a_S}{v_S}.

Each is stated as in the theorem: for every $x$ there is a solution $x_0$ with the bound.

Significance

The result. The theorem converts a residual estimate into a distance estimate. Any scheme that drives $(Ax-b)^+$ to zero brings its iterates to the solution set at a linear rate in the residual. Linear convergence proofs for projection and first-order methods on polyhedral problems and stability results for LP solution sets build on it. Formulas (8)–(10) show that in the max and sum norms the constant can be read off the rows of $A$ through a matrix game.

Formalizing it. The theorem has been proved since 1952, and later papers give several alternative proofs. The mission formalizes Hoffman's own proof route, Lemmas 1–4, in Lean and Mathlib, and the explicit constants (8)–(10). Mathlib has Farkas-type results and projections onto closed convex sets in inner product spaces, but no error bound for linear inequality systems, and the Prove2Me library has no statement of Hoffman's theorem.

Difficulty

For a single $x$ , a bound is trivial: take $x_0$ the nearest solution and choose $c$ accordingly. The whole content is that one $c$ works for all $x$ , including $x$ far from $\Omega$ and $x$ approaching $\Omega$ along every direction. A compactness argument on $\{x : F_n(x)=1\}$ alone fails, because the ratio $F_n(x-x_0)/F_m((Ax-b)^+)$ is not a continuous function of $x$ on a compact set: the nearest solution and the set of active constraints jump as $x$ moves. Lemma 3 needs a positive lower bound on a set $E$ that is not obviously closed away from the origin; its closedness comes from Lemma 4, i.e. from Farkas' lemma. Since $F_n$ , $F_m$ are not norms, no argument using the triangle inequality or symmetry is available. For (8), a set $S$ can arise in Lemma 2 with $v_S=0$ (e.g. $x_1\le0$ , $-x_1\le0$ in $\mathbb R^2$ with $x=(1,0)$ ), contrary to an unnumbered remark on p. 265; the bound (8) is still true, but that remark cannot be used.

Formalization scope

Vectors are Fin k → ℝ, $A$ is Matrix (Fin m) (Fin n) ℝ, the system is A *ᵥ x ≤ b (componentwise), and $y^+$ is posPartVec y = fun i => max (y i) 0.
$F_n$ , $F_m$ are arbitrary functions satisfying IsPosHomogeneous (continuity, nonnegativity, vanishing exactly at $0$ , positive homogeneity); they are never specialised to norms in the goal or Lemmas 1, 3.
"Nearest" is Euclidean and written with the dot product: $y$ is nearest to $x$ in $\Omega$ if $(x-y)\cdot(x-y)\le(x-z)\cdot(x-z)$ for all $z\in\Omega$ . (Mathlib's dist on Fin n → ℝ is the sup distance and is not used.) Lemmas 2 and 3 take "a nearest point" as hypothesis; since the Euclidean nearest point of a closed convex set is unique, this is the page's "the nearest point".
A "subset $S$ of the half spaces" is a Finset (Fin m) of row indices; $M$ keeps all $m$ rows, with zero rows outside $S$ .
In (8)–(10), $|x|$ is ⨆ i, |x i| and $\|x\|$ is ∑ i, |x i|; minima and maxima over finite index sets are ⨅/⨆ in ℝ, equal to the attained min/max on nonempty sets. $v_S$ is defined directly by (7) as a min over the simplex of a max, for nonempty $S$ , so no minimax theorem is needed. In (8), $c$ is the maximum over nonempty $S$ with $v_S>0$ and is $0$ when there is none (only when $A=0$ ). In $w$ , the page's summation range " $j=1,\dots,n$ " is read as ranging over the $m$ rows, since $g$ is indexed by rows.
Consistency is a hypothesis of the goal and of (8)–(10).

The quantifier order $\exists c>0,\ \forall x,\ \exists x_0$ is part of the statement: a version with $c$ chosen after $x$ is trivially true and is not this theorem; likewise $e$ precedes $y$ and $S$ in Lemma 1 and $d_S$ precedes $x$ in Lemma 3.

Infrastructure a complete development needs: existence and the variational characterisation of the Euclidean projection onto a polyhedron in Fin n → ℝ; Farkas' lemma in cone form (published as LinearOptimization.farkas_cone_corollary); compactness of level sets of positive homogeneous functions. The projection and polyhedral-cone lemmas are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal, and sharper or equivalent forms of the constants are welcome.

Selected references

A. J. Hoffman, On Approximate Solutions of Systems of Linear Inequalities, J. Res. Nat. Bur. Standards 49(4) (1952), 263–265. https://doi.org/10.6028/jres.049.027
S. Agmon, The Relaxation Method for Linear Inequalities, Canad. J. Math. 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
S. M. Robinson, Bounds for error in the solution set of a perturbed linear program, Linear Algebra Appl. 6 (1973), 69–81. https://doi.org/10.1016/0024-3795(73)90007-4
O. Güler, A. J. Hoffman, U. G. Rothblum, Approximations to solutions to systems of linear inequalities, SIAM J. Matrix Anal. Appl. 16(2) (1995), 688–696. https://doi.org/10.1137/S0895479892237744
J. Peña, J. C. Vera, L. F. Zuluaga, New characterizations of Hoffman constants for systems of linear constraints, Math. Program. 187 (2021), 79–109. https://doi.org/10.1007/s10107-020-01473-6

10 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

The Ellipsoid Method and Its Consequences in Combinatorial Optimization: With a Weak Separation Oracle, the Rounded Ellipsoid Method Is ε-Optimal After N = 4n²⌈log(2R²‖c‖/(rε))⌉ StepsResearch Paper

Motivation

The ellipsoid method decides questions about a convex set $K \subseteq \mathbb{R}^n$ by maintaining an ellipsoid that contains the relevant part of $K$ and shrinking it step by step. Introduced for convex minimization by Yudin and Nemirovskii and by Shor in the 1970s, it became famous in 1979 when Khachiyan used it to show that linear programming is solvable in polynomial time. Grötschel, Lovász and Schrijver (Combinatorica 1 (1981)) observed that the method never needs an explicit description of $K$ : it only needs, for a query point $y$ , either a confirmation that $y$ is (nearly) in $K$ or a hyperplane (nearly) separating $y$ from $K$ . From this they derived that optimization and separation are polynomially equivalent for convex bodies, which in turn gives polynomial algorithms for problems with exponentially many constraints: matroid intersection, submodular function minimization, and the stable set problem in perfect graphs.

The engine of all of these applications is a single quantitative statement, Theorem (2.4) of the paper: with a weak separation oracle and with all numbers rounded to a fixed number of binary digits, a prescribed number $N$ of ellipsoid steps produces an $\varepsilon$ -optimal point.

Timeline. 1976–1977: Yudin–Nemirovskii and Shor, the method for convex programming. 1979: Khachiyan, polynomial-time linear programming. 1981: Gács–Lovász publish a complete proof of Khachiyan's result with the explicit rounded update; Grötschel–Lovász–Schrijver state and prove the weak-oracle version, Theorem (2.4), and its combinatorial consequences; Bland–Goldfarb–Todd survey the method (Oper. Res. 29 (1981)). 1988: the monograph of Grötschel, Lovász and Schrijver (Springer) gives the full theory of weak oracles.

Setting

All norms are Euclidean: $\|v\| = \sqrt{v^{\mathsf T}v}$ , and for a symmetric matrix $\|A\|$ is the largest absolute eigenvalue. $S(a_0,\rho)$ is the closed Euclidean ball of radius $\rho$ about $a_0$ , and $S(K,\delta)$ the set of points within distance $\delta$ of $K$ .

A convex body $(K, a_0, r, R)$ consists of a compact convex $K\subseteq\mathbb{R}^n$ , $n\ge 2$ , and $0<r\le R$ with

S(a_0,r)\subseteq K\subseteq S(a_0,R).

A weak separation oracle with precision $\delta>0$ answers a query $y$ either with " $y\in S(K,\delta)$ ", or with a vector $d$ , $\|d\|\ge 1$ , such that $d^{\mathsf T}x\le d^{\mathsf T}y+\delta$ for all $x\in K$ .

Given an objective $c$ and an accuracy $\varepsilon>0$ (with $\varepsilon<r$ and $\|c\|\ge 1$ ), set

N = 4n^2\left\lceil \log\frac{2R^2\|c\|}{r\varepsilon}\right\rceil,\qquad \delta = \frac{R^2\,4^{-N}}{300n},\qquad p = 5N .

Start from $x_0=a_0$ , $A_0=R^2I$ . At step $k$ query the oracle at $x_k$ . If it answers "feasible", $k$ is a feasible index and $a=c$ ; otherwise $a=-d$ . Put $b_k = A_ka/\sqrt{a^{\mathsf T}A_ka}$ and

x_k^* = x_k+\frac{1}{n+1}b_k,\qquad A_k^* = \frac{2n^2+3}{2n^2}\Bigl(A_k-\frac{2}{n+1}b_kb_k^{\mathsf T}\Bigr),

and obtain $x_{k+1}$ , $A_{k+1}$ by rounding $x_k^*$ , $A_k^*$ to $p$ binary digits, keeping $A_{k+1}$ symmetric. The ellipsoids are $E_k=\{x : (x-x_k)^{\mathsf T}A_k^{-1}(x-x_k)\le 1\}$ , and $K_k$ is the set of points of $K$ whose objective value is at least that of every feasible centre found before step $k$ .

In Lean, IsRoundedRun K c a₀ R δ p N x A feas a d records exactly these conditions, Kk is $K_k$ , and $E_k$ is the published LinearOptimization.ellipsoid (x k) (A k).

Formalization targets

Goal: Theorem (2.4)

If $j<N$ is a feasible index whose centre is best among the feasible centres, $c^{\mathsf T}x_j=\max\{c^{\mathsf T}x_k : k<N \text{ feasible}\}$ , then

c^{\mathsf T}x_j \ \ge\ \max_{x\in K} c^{\mathsf T}x - \varepsilon .

The statement is for every run, i.e. for every sequence of valid oracle answers and every admissible rounding.

Milestones, in attack order

(13): the explicit inverse $(A_k^*)^{-1}=\frac{2n^2}{2n^2+3}\bigl(A_k^{-1}+\frac{2}{n-1}\frac{aa^{\mathsf T}}{a^{\mathsf T}A_ka}\bigr)$ , and $A_k^*\succ 0$ .
Lemma (2.1): $A_0,\dots,A_N$ are positive definite, $\|x_k\|\le\|a_0\|+R2^k$ , $\|A_k\|\le R^22^k$ , $\|A_k^{-1}\|\le R^{-2}4^k$ .
Lemma (2.2): $\mu(E_{k+1}) < e^{-1/(5n)}\mu(E_k)$ .
Lemma (2.3): $K_k\subseteq E_k$ for $k=0,\dots,N$ .
(32): $\mu(K_N)\le\mu(E_N)\le e^{-N/(4n)}\mu(E_0)=e^{-N/(4n)}R^nV_n$ .
(34): the piece above the level $t$ of the cone with base the $r$ -disc through $x_0$ orthogonal to $c$ and apex $y\in K$ has volume $\frac{V_{n-1}r^{n-1}(\zeta-c^{\mathsf T}x_0)}{n\|c\|}\bigl(\frac{\zeta-t}{\zeta-c^{\mathsf T}x_0}\bigr)^n$ , which bounds $\mu(\{z\in K: c^{\mathsf T}z\ge t\})$ from below.

Significance

Theorem (2.4) turns any weak separation procedure for a convex body into a weak optimization procedure, with a number of oracle calls and a numerical precision polynomial in $n$ , $\log R$ , $\log(1/r)$ , $\log\|c\|$ and $\log(1/\varepsilon)$ . This is the "only if" half of the paper's Theorem (3.1), and through it the source of the polynomial algorithms of Chapters 4–6 of the paper and of the 1988 monograph. Its rounding analysis is what makes the method an algorithm on finite-precision numbers rather than an argument about exact real arithmetic.

The result is proved, and has been for over forty years. What this mission adds is a machine-checked proof of the rounded, weak-oracle version, including the error analysis that the paper compresses into "rounding errors can be estimated similarly". Related items already on the platform formalize exact-arithmetic ellipsoid methods: Bertsimas–Tsitsiklis's central-cut method for polyhedra (LinearOptimization.ellipsoid_method_correct, proved) and Bubeck's version for convex minimization with a first-order oracle (arXiv:1405.4980). Neither has a weak oracle, the inflated factor $(2n^2+3)/(2n^2)$ , or rounding.

Difficulty

For the exact update with factor $n^2/(n^2-1)$ and an exact separating hyperplane through the centre, containment and volume decrease are a classical computation. Here three perturbations interact. The cut is shifted by $\delta$ , so the retained half-ellipsoid is slightly larger than a half. The rounded matrix differs from $A_k^*$ by up to $n2^{-p}$ in norm, which could destroy positive definiteness if the smallest eigenvalue were not controlled from below, and Lemma (2.1)'s bound $R^24^{-k}$ is what controls it. The containment $K_{k+1}\subseteq E_{k+1}$ must absorb both errors, and it is the inflation factor $(2n^2+3)/(2n^2)$ , chosen larger than the optimal one, that leaves room. The paper bounds the remainder term in (29) only by "similar methods"; making that bound explicit is the bulk of the work. The final step also needs the volume rate $e^{-N/(4n)}$ in (32), which is sharper than iterating Lemma (2.2) and requires the exact per-step volume ratio of the inflated update.

Formalization scope

$\mathbb{R}^n$ is Fin n → ℝ with Lebesgue measure. Since Lean's norm on Fin n → ℝ is the sup norm, the Euclidean norm is written out (euclNorm), and the bounds $\|A_k\|\le R^22^k$ , $\|A_k^{-1}\|\le R^{-2}4^k$ are stated as quadratic-form (eigenvalue) bounds. $N$ uses the natural logarithm and the integer ceiling.

The runs generalize the page in three ways, each of which makes the theorems stronger: the oracle's answers are any answers valid for its specification; rounding is any symmetric value within $2^{-p}$ entrywise; and data are real rather than rational.

The page's standing assumptions $\varepsilon<r$ , $\|c\|\ge1$ , $n\ge2$ (p. 173) are hypotheses. Two hypotheses are added, because the page's $N$ , $\delta$ and $p$ are absolute numbers and the claims fail at extreme scales:

$R\ge 1$ (Lemmas (2.1)–(2.3), (32), Theorem (2.4)): for $R=r=2^{-1000}$ , $\varepsilon=r/2$ , $n=2$ , rounding can make $A_1=0$ .
$\varepsilon\le1$ (Lemma (2.3), (32), Theorem (2.4)): for $R=r=10^{13}$ , $\varepsilon=0.99r$ , $n=2$ , $\delta>2r$ , and a valid oracle can cut away all of $K$ .

Neither is needed in (13) or (34).

A run predicate without the oracle clause would make Lemma (2.3) false, and one with exact equality instead of rounding would state a weaker theorem; the goal quantifies over every run, never over some run. Positive definiteness of the $A_k$ is a consequence (Lemma (2.1)), not a hypothesis: since Lean's inverse of a singular matrix is $0$ , assuming it would hide the lemma's content.

Out of scope: the paper's polynomial-time claims (Theorem (3.1) and its consequences), the bit length of the numbers, and the rationality of inputs, since no oracle-machine model with bit complexity exists in Mathlib or on the platform.

Reusable infrastructure: volumes of ellipsoids and of cone pieces, Sherman–Morrison-type inverses, and perturbation bounds for positive definite matrices. Contributions of these as separate lemmas are welcome.

Selected references

M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1(2) (1981) 169–197. https://doi.org/10.1007/bf02579273
P. Gács, L. Lovász, Khachiyan's algorithm for linear programming, Mathematical Programming Study 14 (1981) 61–68. https://doi.org/10.1007/BFb0120921
L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20 (1979) 191–194 (English translation of the original article).
R. G. Bland, D. Goldfarb, M. J. Todd, The ellipsoid method: a survey, Operations Research 29(6) (1981) 1039–1091. https://doi.org/10.1287/opre.29.6.1039
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Ch. 8. Book record.
S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8 (2015). https://arxiv.org/abs/1405.4980

10 thms2 active usersReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

An Additive Algorithm for Solving Linear Programs with Zero-One Variables: In Finitely Many Iterations the Additive Algorithm Yields an Optimal Solution or Proves InfeasibilityResearch Paper

Motivation

Binary decisions arise when a variable records whether a project is selected, a facility is opened, or an action is taken. Linear constraints then describe the resources or conditions those choices must satisfy. Egon Balas's 1965 paper gives a direct algorithm for a finite linear program with zero-one variables: it begins with all variables at zero, adds variables with value one, and uses explicit tests to discard assignments that cannot improve the best feasible assignment found so far. The paper states that the procedure eventually produces an optimal feasible solution or a conclusion that none exists. Its numbered convergence theorem is the target of this mission. Balas (1965)

The result is historically distinct from algorithms that solve a continuous relaxation and then enforce integrality. Balas describes his method as a direct combinatorial search over binary assignments, with additions and subtractions used to update costs and slacks. The theorem concerns the correctness and finite termination of the particular steps printed in the paper, including their backward scan and cancellation rules. The local catalog contains work on branch and bound for a biconvex program, but no existing platform item about a zero-one programming algorithm with these steps; the biconvex result concerns a different model and algorithm. Balas (1965)

Setting

Let $N$ be a finite set of binary coordinates and $M$ a finite set of constraints. The data are a real matrix $A=(a_{ij})_{i\in M,j\in N}$ , a real vector $b=(b_i)_{i\in M}$ , and nonnegative objective coefficients $c_j\ge0$ . A binary assignment is represented by the set $J\subseteq N$ of coordinates assigned one; all other coordinates are zero. Its slack and cost are

y_i(J)=b_i-\sum_{j\in J}a_{ij},\qquad z(J)=\sum_{j\in J}c_j.

The assignment is feasible when $y_i(J)\ge0$ for every $i\in M$ . It is optimal when it is feasible and has no greater cost than any other feasible assignment. These are Balas's problem $P$ and solutions (1)–(8). The coefficients of $A$ and $b$ may have either sign; $N$ and $M$ may be empty. Balas (1965), pp. 519, 523

The algorithm generates assignments $J_0,J_1,\ldots,J_s$ , starting at $J_0=\varnothing$ . Among the generated feasible assignments, their least cost is the ceiling $z^{*(s)}$ ; if there are none, $z^{*(s)}=+\infty$ . Each generated assignment has an improving set $N_p$ formed when it first appears. Later steps cancel candidate indices and keep records $C_k^s$ of which values attached to an earlier assignment have been cancelled by the time $J_s$ is generated. The algorithm either processes the latest assignment, scans earlier strict subsets in descending order, or stops. Its value-based choice rule permits several choices when both value and cost tie. Balas (1965), pp. 523–528

Formalization targets

The paper's two lemmas and Theorem 1 establish the cancellation claims used by its convergence theorem. Lemma 1 says a feasible completion $J_t\supset J_s$ below the current ceiling adds no index in $C^s$ ; Lemma 2 makes the corresponding assertion for an earlier assignment under its stated complete-cancellation hypothesis. Theorem 1 says that an abandoned assignment has no better feasible completion. The two numbered parts of the convergence proof assert that a single iteration cannot continue indefinitely and that no assignment is generated twice. A remark after (16) records that a feasible generated assignment has an empty improving set. Balas (1965), pp. 529–533

The mission's goal is Convergence Theorem 2:

\text{every run from }J_0=\varnothing\text{ stops after finitely many steps, with either an optimal feasible assignment or a valid infeasibility verdict.}

The finite-step assertion includes progress: every reachable state before a stopping situation has a successor. At a stop, $z^{*(s)}=+\infty$ means no feasible binary assignment exists; if the ceiling is finite, a generated assignment attaining it exists and every generated assignment at that cost is optimal for $P$ . These clauses make the paper's two possible outcomes explicit. Balas (1965), Convergence Theorem 2 and step 5a

Significance

The theorem certifies the algorithm as a complete decision and optimization procedure for the stated finite binary program. The infeasibility outcome concerns every possible binary assignment, not only the assignments the algorithm happened to visit. The optimality outcome similarly compares the reported assignment against all feasible assignments. Without these global claims, reaching a stopping situation would only show that the current search path has no remaining candidates. Balas (1965), pp. 526, 533

The result was proved in the 1965 paper. The work here is to state its algorithm and correctness claims in Lean and provide a target for a machine-checked proof; the submitted theorem files are open statements. The finite binary-program model, cost and slack functions, ceiling with infinity, and state-transition vocabulary can also support formal analyses of other exact enumeration procedures. The particular cancellation and backward-scan rules belong to Balas's algorithm. Balas (1965)

Difficulty

It is immediate that there are finitely many binary assignments. That alone does not show finite termination: the paper's step 5 may revisit earlier generated assignments, and the rules must prevent repeated work within one iteration as well as repeated generated assignments across iterations. It also does not justify pruning. When an improving set becomes empty, the remaining challenge is to show that no feasible assignment omitted by the search improves the ceiling. These are the separate claims recorded in parts (a) and (b), Lemmas 1–2, and Theorem 1. Balas (1965), pp. 529–533

Formalization scope

Lean uses Fin n and Fin m for the paper's one-based index sets. A binary assignment is a Finset (Fin n). A general finite zero-one linear program is its own definition; problem $P$ adds the paper's standing assumption $c_j\ge0$ . There is no positive-size assumption on either index set. The algorithm stores generated assignments, each improving set as formed, cancellation snapshots, current cancellations, and its program point. Slack and cost are recomputed from the assignment by (6) and (21). Reachability is the reflexive transitive closure of the printed steps, and all milestone claims about states are restricted to reachable ones. The strict symbol $\subset$ means proper inclusion as the paper's footnote specifies. Balas (1965), pp. 523–525

The ceiling is represented in WithTop ℝ, with $\top$ for $+\infty$ . The cost tests (14), (17), (24), and (29) are written additively so they retain the paper's meaning when no feasible assignment has yet been generated. The improving set $N_p$ remains fixed after generation; the step-5 scan uses $N_k^s=N_k-(C_k^s\cup D_k^s)$ with the stored snapshot $C_k^s$ , as in (18). Step 1a cancels the cost-bound indices for every earlier assignment, and steps 6a and 7b resume the scan below the index just checked. The final tie break permits any index still tied after minimizing its cost. “In a finite number of iterations” is encoded as no infinite run plus a next step at each reachable non-stopped state. “No feasible solution” quantifies over all binary assignments. “Abandoned” is the predicate specified before Theorem 1: $u^k$ is abandoned when the algorithm is instructed to stop, or to check some $N_p^s$ with $p<k\le s$ , including the indices step 5 passes over because their remaining improving set is empty. Lemma 2 reads $C_p^{s+1}$ either as the cancellations accumulated so far during iteration $s+1$ or as the cancellation records at the transition that obtains $u^{s+1}$ . Balas (1965), pp. 525–533

The paper prints $z^{*(k)}$ in Theorem 1, but its algorithm and proof use the ceiling at the abandonment iteration, $z^{*(s)}$ ; the Lean theorem states that corrected version and retains the original wording in the milestone record. A transition system that is stuck before a declared stopping situation, a ceiling encoded as a finite real sentinel, or a verdict quantified only over generated assignments would make the goal weaker than the paper's claim. Contributions toward the milestone proofs, state invariants, and reusable finite-search lemmas are in scope. The preliminary reduction of a general binary program to $P$ , the efficiency remarks, numerical examples, and the modified algorithm of Remark II are outside this mission. Balas (1965), pp. 519, 528–533

Selected references

Egon Balas, An Additive Algorithm for Solving Linear Programs with Zero-One Variables, Operations Research 13(4), 517–546, 1965. DOI: 10.1287/opre.13.4.517

10 thms2 active usersReviewed

Linear Optimization

Missions

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms III: Every Directed Uniform Multicommodity Flow Problem Has Ω(𝒮/log n) ≤ f ≤ 𝒮Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 12 (p. 804)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms II: Every Product Multicommodity Flow Problem with k Commodities Has Ω(𝒮/log k) ≤ f ≤ 𝒮Research Paper

Why multicommodity max-flow and min-cut

Setting

Formalization targets

Goal: Theorem 7 (pp. 801–802)

Milestones, in the order the proof uses them

Stronger companions

Significance

Difficulty

Formalization scope

Selected references

Linear Programming and Markov Decision Chains 2: Representatives of Average Optimal Stationary Policies Are Optimal Dual Solutions, and Every Optimal Dual Solution Gives an Average Optimal PolicyResearch Paper

Motivation

Setting

Formalization targets

Optimality correspondence

Supporting results

Significance

Difficulty

Formalization scope

Selected references

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 2: The Greedy Forward Dual Solution Is Optimal and Its Value Is the Lot-Sizing CostResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming: The Set-Inclusive LP Has the Same Feasible Set as the LP of Support FunctionalsResearch Paper

Motivation

Setting

Formalization targets

Goal: the THEOREM (p. 1156)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 4: For a Random Subspace, ‖Pq‖⁻∞ ≤ (log n/n)‖r‖² with Probability Tending to OneResearch Paper

Motivation

Setting

Formalization targets

Theorem 5

Source milestones

Significance

Difficulty

Formalization scope

Selected references

Integer Programming Formulation of Traveling Salesman Problems: The Miller–Tucker–Zemlin Constraints Exactly Describe the Itineraries with at Most p Cities per TourResearch Paper

Why this formulation matters

Setting

Formalization targets

Goal: the equivalence of (1) and (2)

Milestones, in the order of the paper's proof

Significance

Difficulty

Formalization scope

Selected references

On the Job-Shop Scheduling Problem: The Integer Program (2)–(7) with 0–1 Variables y_jk Attains Exactly the Minimum Make-SpanResearch Paper

Motivation

Setting

Formalization targets

Goal: the integer program solves the make-span problem

Milestones

Significance

Difficulty

Formalization scope