Operations Research

Motivation

Two optimization problems on weighted networks sit at the base of operations research and algorithm design. The first asks for the cheapest way to connect every node of a network, such as a cable, pipeline or communication network. The answer is a minimum weight spanning tree. The second asks for the shortest route from a depot to every other node of a road or data network, the single-source shortest path problem. Chapter 12 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) treats both. It proves the structural lemmas behind the greedy spanning tree algorithms of Kruskal (1956) and Prim (1957), and the correctness of the shortest path algorithm of Dijkstra (1959).

The minimum spanning tree problem goes back to Borůvka (1926), who designed an electrical network for Moravia. Kruskal and Prim gave the two greedy algorithms taught today, and Dijkstra's 1959 note treated both problems. Dijkstra's shortest path method, with heap-based refinements such as Fredman and Tarjan (1987), remains the standard solver for non-negative lengths and a building block of routing, scheduling and network flow codes.

Setting

A graph $G = (V, E)$ has a finite vertex set $V$ and a set $E$ of 2-element subsets of $V$. A weight $w(e) \in \mathbb N_0$ is attached to each edge, and a set $S$ of edges has weight $w(S) = \sum_{e \in S} w(e)$. A spanning forest of $G$ is an acyclic graph $H = (V, S)$ with $S \subseteq E$. A spanning tree is a spanning forest that is connected. The weight of a spanning tree is the weight of its edge set. In Lean these are SimpleGraph V with [Fintype V], IsSpanningForest G H ($H \le G$ and acyclic), IsSpanningTree G T ($T \le G$ and a tree), and weight w T for a weight w : Sym2 V → ℕ.

A digraph $G = (V, E)$ has $E \subseteq V \times V$ with $x \ne y$ for every directed edge $(x, y)$. Each directed edge has a length $w(x, y) \in \mathbb N_0$. The length is extended by $w(x, y) = \infty$ for non-edges. A directed path from $a$ to $b$ is a sequence $(a = u_0, \dots, u_t = b)$ of distinct vertices in which consecutive pairs are directed edges. Its length is $\sum_{i<t} w(u_i, u_{i+1})$. The distance $\operatorname{dist}(a, b) \in \mathbb N_0 \cup \{\infty\}$ is the minimum length of a directed path from $a$ to $b$, and is $\infty$ when no such path exists. A shortest path is a directed path attaining it. In Lean this is WeightedDigraph V with ext, IsDirPath, pathLength, dist and IsShortestPath.

Dijkstra's algorithm (Algorithm 12.14) with root $r$ and $n = |V|$ keeps a sequence $\sigma$ of permanent vertices, a value $\delta(x) \in \mathbb N_0 \cup \{\infty\}$ and a sequence $P(x)$ for each vertex. Step 1 sets $\delta(r) = 0$, $P(r) = (r)$, $\sigma = (r)$, and $\delta(x) = w(r, x)$, $P(x) = (r, x)$ for $x \ne r$. Step $i$ with $1 < i < n$ scans from the last permanent vertex $v_i$. For every temporary $x$ it sets $\delta(x) \leftarrow \min\{\delta(x), \delta(v_i) + w(v_i, x)\}$, and on a strict decrease it replaces $P(x)$ by $P(v_i)$ followed by $x$. Each step ends by appending to $\sigma$ a temporary vertex of minimum $\delta$, chosen arbitrarily among ties. The algorithm halts at Step $n$. DijkstraRun G r i s holds when some sequence of admissible choices leads to state s at the start of Step $i$.

Formalization targets

Goal: correctness of Dijkstra's algorithm (Theorem 12.18)

For every halted state of every run, and every vertex $x$,

$$\delta(x) = \operatorname{dist}(r, x), \qquad \operatorname{dist}(r, x) < \infty \implies P(x) \text{ is a shortest path from } r \text{ to } x.$$

Milestones

1. Proposition 12.3. A spanning forest $H = (V, S)$ of a graph on $n \ge 1$ vertices has $|S| \le n - 1$ and exactly $n - |S|$ components. It is a spanning tree if and only if $|S| = n - 1$.
2. Proposition 12.4 (Exchange Principle). Let $T$ be a spanning tree and $xy \in E \setminus T$. Then $T$ contains a unique path $x = x_0, \dots, x_t = y$, and replacing any edge $x_i x_{i+1}$ of it by $xy$ gives a spanning tree.
3. Lemma 12.6. In a connected weighted graph, let $F$ be a spanning forest and $C$ a component of $F$. A minimum weight edge leaving $C$ lies in some spanning tree that has minimum weight among the spanning trees containing $F$.
4. Proposition 12.16. Every prefix and every suffix of a shortest path is a shortest path.
5. Proposition 12.17. When the algorithm halts, $\delta(v_1) \le \delta(v_2) \le \cdots \le \delta(v_n)$.

Milestones 4 and 5 are the two statements the book's proof of the goal rests on. Milestones 1–3 are the spanning tree half of the chapter. Lemma 12.6 is the result from which the book derives the correctness of Kruskal's and Prim's algorithms.

Significance

Theorem 12.18 certifies that one pass of $n$ steps computes all distances from $r$ and a shortest path tree, with no condition on the digraph beyond non-negative lengths. Lemma 12.6 is the cut property. Every greedy minimum spanning tree method (Kruskal, Prim, Borůvka) is an instance of it, and the exchange principle is the matroid basis-exchange axiom specialised to the graphic matroid.

All of these results are classical and proved. None is formalized in this form on the platform. Mathlib has spanning trees of connected graphs, uniqueness of paths in acyclic graphs, and the edge count $n - 1$ of a tree. It has no edge–component count for forests, no exchange principle, no weighted spanning trees, and no Dijkstra. On Prove2Me, FamousTheorems.tree_card_edges_6b and ClassicalGaps.isAcyclic_edges_eq_card_sub_one_imp_connected cover only the tree case of Proposition 12.3. KServer.mst_cut_property is a cut property for complete graphs encoded by parent maps, a different statement. The label-correcting algorithm of Dynamic Programming and Optimal Control II (BertsekasDP.label_correcting_*) is a different algorithm: it keeps an open list and scans in arbitrary order, not by minimum label.

Difficulty

The goal is a statement about the final state of a run, but the facts it depends on only become visible across steps: a permanent vertex's $\delta$ and $P$ never change again, and $\delta(x)$ is always the length of the current $P(x)$. None of this is recorded in the final state itself. An argument over the steps of the run has to show that each $P(x)$ remains a path with distinct vertices, including when edges of length $0$ allow ties. It also has to handle the value $\infty$, where $\infty + a = \infty$ and a comparison between two infinite values never counts as a decrease. Tie-breaking is arbitrary, so no argument may depend on which minimum is chosen. For Lemma 12.6 the difficulty is the exchange step: removing an edge of a tree path and adding a crossing edge must again give a tree that still contains the forest $F$, and this is a statement about cycles and components, not about counts.

Formalization scope

• Graphs are SimpleGraph V over a Fintype V. Weights are Sym2 V → ℕ (the book's $w : E \to \mathbb N_0$; values off $E$ are never used). Acyclic, tree and connected components are Mathlib's. In Proposition 12.3, $|S| = n - k$ is written $|S| + k = n$ and $n \ge 1$ is assumed, which the bound $n - 1$ presupposes.
• Lemma 12.6 assumes $G$ connected, the section's standing assumption (p. 239). The page's "to avoid trivialities, we assume $n \ge 3$" is not imposed, because the statement holds for every $n$. The crossing edge may have either endpoint in $C$.
• Lengths in the digraph are ℕ, and $\delta$ and distances are ℕ∞, where $\infty$ is ⊤, never a large finite number. A version with real or ℝ≥0 lengths would be a generalization and is not what is asked.
• Dijkstra's algorithm is defined step by step exactly as on pp. 246–247, including $\delta(x) = w(r, x) = \infty$ and $P(x) = (r, x)$ for non-neighbours at Step 1. The goal quantifies over every halted state, so it holds for every tie-breaking. A halted state always exists; a sorry-free check of this is in the workspace. For a vertex not reachable from $r$ the book is silent. The distance there is read as $\infty$, and the shortest-path conclusion is asserted only at finite distance.
• A trivializing formalization is ruled out: $\delta$ is computed by the update rule of Algorithm 12.14, not defined as the distance, and the theorem is not stated for an arbitrary procedure satisfying its own conclusion.
• The book uses no $O(\cdot)$ bounds or approximate constants in these statements, so there are no constants to instantiate.
• Reusable infrastructure: a list-based theory of directed paths and distances in ℕ∞, the invariants of Dijkstra's algorithm, and forest edge counting. Contributions of general lemmas (walks shortcut to paths without increasing length, component counts under edge insertion) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 12. https://www.appliedcombinatorics.org/
• E. W. Dijkstra, "A note on two problems in connexion with graphs", Numerische Mathematik 1 (1959) 269–271. https://doi.org/10.1007/BF01386390
• J. B. Kruskal, "On the shortest spanning subtree of a graph and the traveling salesman problem", Proc. AMS 7 (1956) 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• R. C. Prim, "Shortest connection networks and some generalizations", Bell System Technical Journal 36 (1957) 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
• M. L. Fredman and R. E. Tarjan, "Fibonacci heaps and their uses in improved network optimization algorithms", J. ACM 34 (1987) 596–615. https://doi.org/10.1145/28869.28874
• O. Borůvka, "O jistém problému minimálním", Práce Moravské přírodovědecké společnosti 3 (1926) 37–58. https://dml.cz/handle/10338.dmlcz/500114

Motivation

Network revenue management decides which products to make available to arriving customers when products share scarce resources: an airline sells itineraries (products) that consume seats on flight legs (resources), and each itinerary has a fare. When customers choose among the offered products, rather than asking for one fixed product, the standard planning tool is a deterministic linear program that replaces random choices by their expected values. Gallego, Iyengar, Phillips and Dubey (2004, Columbia CORC technical report TR-2004-01) and Liu and van Ryzin (2008) formulated this choice-based linear program; its solution drives bid-price and offer-set policies used in practice.

The difficulty is size. The choice-based program has one variable for each subset of products, $2^n$ in all, and is solved by column generation, whose pricing subproblem is itself an assortment problem. Feldman and Topaloglu (Oper. Res. 65(5), 2017) show that when customers choose under the Markov chain choice model of Blanchet, Gallego and Goyal (2016), the choice-based program is equivalent to a linear program with only $2n$ variables and $m+n$ constraints. This mission formalizes that equivalence, Theorem 7 of the paper.

Setting

There are $n$ products, $N=\{1,\dots,n\}$. Under the Markov chain choice model a customer first visits product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she moves from product $j$ to product $i$ with probability $\rho_{j,i}$, or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. The paper assumes throughout that

$$\lambda_j>0\quad\text{and}\quad\sum_{i\in N}\rho_{j,i}<1\qquad\text{for all } j\in N.$$

For an offer set $S\subseteq N$, $P_{j,S}$ is the expected number of visits to product $j$ while it is offered, which is its purchase probability, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the solution of the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .$$

Dropping the constraints tied to $S$ gives the polyhedron

$$\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+ : x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\}.$$

The network has $m$ resources, $M=\{1,\dots,m\}$, with capacities $c_q$; the selling horizon has $T$ periods; product $j$ earns $r_j$ and consumes $a_{q,j}$ units of resource $q$. With $u_S$ the probability of offering $S$ in a period, the (Choice Based) linear program is

$$\max_{u\in\mathbb R^{2^n}_+}\Big\{\sum_{S\subseteq N}\sum_{j\in N}T r_jP_{j,S}u_S:\ \sum_{S\subseteq N}\sum_{j\in N}Ta_{q,j}P_{j,S}u_S\le c_q\ \forall q\in M,\ \sum_{S\subseteq N}u_S=1\Big\},$$

and the (Reduced) linear program is

$$\max_{(x,z)\in\mathbb R^{2n}_+}\Big\{\sum_{j\in N}T r_jx_j:\ \sum_{j\in N}Ta_{q,j}x_j\le c_q\ \forall q\in M,\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \forall j\in N\Big\}.$$

In (Reduced), $x_j$ is the expected number of visits to product $j$ while it is available and $z_j$ the expected number of visits while it is not.

Formalization targets

Goal: Theorem 7

Let $(\hat x,\hat z)$ be an optimal solution of (Reduced). Then there are subsets $S^1,\dots,S^K\subseteq N$ and positive scalars $\gamma^1,\dots,\gamma^K$ with $\sum_k\gamma^k=1$ such that

$$\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},$$

and for any such subsets and scalars the vector $\hat u$ with $\hat u_{S^k}=\gamma^k$ and $\hat u_S=0$ for $S\notin\{S^1,\dots,S^K\}$ is optimal for (Choice Based), with objective value equal to that of $(\hat x,\hat z)$ in (Reduced). In particular the two programs have the same optimal value.

Milestones

1. (Balance) has a unique and nonnegative solution for every offer set (§2, p. 1325).
2. Lemma 1: an extreme point $(\hat x,\hat z)$ of $\mathcal H$ equals $(P_{S},R_{S})$ for $S=\{j:\hat x_j>0\}$ (p. 1326).
3. Lemma 10: $\mathcal H$ is bounded (quoted on p. 1331; proved in the online appendix).
4. Every point of $\mathcal H$ is a positive convex combination of finitely many extreme points of $\mathcal H$ (proof of Theorem 7, p. 1331).
5. Every feasible $u$ of (Choice Based) yields the feasible point $\tilde x_j=\sum_S P_{j,S}u_S$, $\tilde z_j=\sum_S R_{j,S}u_S$ of (Reduced), with the same objective value (proof of Theorem 7, p. 1332).

Significance

The result. Theorem 7 replaces a program with $2^n$ columns by one with $2n$ variables and $m+n$ constraints, solvable directly by any LP solver, and it returns an optimal solution of the original program, not only its value. The optimal value is the standard upper bound on the optimal expected revenue of a network revenue management policy, and the dual variables of the capacity constraints are the bid prices used to control sales. The decomposition of part 1 is what turns the small program's solution back into offer-set frequencies that a policy can implement; Section 7 of the paper makes that decomposition algorithmic (a separate mission of this series).

Formalizing it. The theorem is proved in the paper; to the best of available knowledge no machine-checked version exists. A formal proof checks the link between polyhedral geometry (extreme points of $\mathcal H$ and the solutions of (Balance)) and linear-programming optimality, and records exactly which properties of the Markov chain choice model are used: the standing assumptions enter through uniqueness and nonnegativity of $(P_S,R_S)$ and through boundedness of $\mathcal H$.

Difficulty

The inequality "(Reduced) $\ge$ (Choice Based)" is a direct computation: averaging the (Balance) equations with weights $u_S$ lands in $\mathcal H$. The reverse direction is where the obvious argument fails. A point of $\mathcal H$ has no offer set attached to it, and a general polyhedron need not be the convex hull of its extreme points: it can contain lines or rays. The argument requires that $\mathcal H$ is bounded, which depends on the substochasticity $\sum_i\rho_{j,i}<1$, and that each extreme point is exactly some $(P_S,R_S)$, which uses the structure of the balance equations and the uniqueness of their solution. Neither follows from general linear-programming facts. In Lean, the finite vertex representation of a bounded polyhedron is also not a one-line consequence of Mathlib's Krein–Milman theorem, which gives only the closure of the convex hull.

Formalization scope

Products are Fin n, offer sets Finset (Fin n), resources Fin m. The model is a structure Model n holding $\lambda$, $\rho$ (rho j i $=\rho_{j,i}$, the transition from $j$ to $i$) and the standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$; the nonnegativity $\rho_{j,i}\ge0$, implicit in the paper because the $\rho_{j,i}$ are probabilities, is an added field. $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon, and milestone 1 is what identifies it with the paper's unique solution. $\mathcal H$ is a subset of (Fin n → ℝ) × (Fin n → ℝ), extreme points are Mathlib's Set.extremePoints ℝ, and boundedness is Bornology.IsBounded. $T$ is a natural number entering as a real factor exactly where the paper writes it; $c$, $a$, $r$ carry no sign conditions, as in the paper. "Optimal solution" means feasible and at least as good as every feasible point; no supremum is used.

Two conventions are disclosed. The paper defines $\hat u$ by $\hat u_{S^k}=\gamma^k$; the formalization sets $\hat u_S=\sum_{k:S^k=S}\gamma^k$, which agrees when the $S^k$ are distinct and is the only consistent reading otherwise. Milestone 5 is stated for every feasible $u$ of (Choice Based), while the paper applies it to an optimal one; its argument uses only feasibility. No printed statement needed correction.

The goal is not only the decomposition of part 1, which is milestones 2 and 4 combined: it also asserts optimality of $\hat u$ and equality of the optimal values, and a formalization that drops part 2 does not state Theorem 7. Part 2 is required for every decomposition, and part 1 guarantees one exists, so part 2 is not vacuous.

A complete development needs the vertex representation of polytopes (reusable beyond this mission; LinearOptimization.polyhedron_resolution on the platform proves the resolution theorem in another encoding), the theory of substochastic matrices behind (Balance) (invertibility of $I-\bar Q$ with a nonnegative inverse), and finite-sum manipulations over Finset (Fin n). Contributions to any milestone, and bridges to existing polyhedral results, are welcome.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0172
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, Computational Optimization Research Center Technical Report TR-2004-01, Columbia University, 2004 (technical report; no DOI).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Airlines, hotels and rental firms sell a fixed stock of capacity (seats on a flight leg, rooms on a night) over a finite selling horizon, and control revenue mainly by deciding which products (fare classes, rate plans) to make available at each moment. When customers substitute between products, the decision in each period is an assortment: a subset of products to offer. Talluri and van Ryzin (Management Science 2004) formulated this single resource revenue management problem as a dynamic program for a general choice model, and showed that structural properties of the optimal policy depend strongly on how customers choose.

The Markov chain choice model of Blanchet, Gallego and Goyal (technical report 2013; Oper. Res. 2016) describes substitution by a Markov chain on the products and approximates a broad class of random-utility models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study assortment and revenue management problems under this model. This mission formalizes their structural result for the single resource problem (Theorem 5): there is an optimal policy whose offer sets are nested in the remaining capacity and in the remaining time, so that it can be implemented by protection levels, one capacity threshold per product and period.

Setting

There are $n$ products $N=\{1,\dots,n\}$. A customer arrives to purchase product $j$ with probability $\lambda_j$. If $j$ is offered she buys it; otherwise she moves to product $i$ with probability $\rho_{j,i}$, and leaves with probability $1-\sum_{i\in N}\rho_{j,i}$. The paper assumes $\lambda_j>0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j$. For an offer set $S\subseteq N$, the purchase probabilities $P_{j,S}$ and the visit counts $R_{j,S}$ of unavailable products solve the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j,\qquad P_{j,S}=0\ \ (j\notin S),\qquad R_{j,S}=0\ \ (j\in S).$$

With product revenues $r_j$, the (Assortment) problem is $\max_{S\subseteq N}\sum_{j}P_{j,S}r_j$, and its (Dual) linear program is

$$\min_{v\in\mathbb R^n}\Big\{\sum_{j}\lambda_jv_j : v_j\ge r_j,\ v_j\ge\sum_{i}\rho_{j,i}v_i\ \ \forall j\Big\}.$$

In the single resource problem there are $T$ periods and $c$ units of capacity. In each period at most one customer arrives; a sale of product $j$ earns $r_j$ and uses one unit. The optimal expected revenue $V_t(x)$ from period $t$ on with $x$ units left satisfies the (Single Resource) dynamic program

$$V_t(x)=\max_{S\subseteq N}\Big\{\sum_{j\in N}P_{j,S}\{r_j+V_{t+1}(x-1)-V_{t+1}(x)\}\Big\}+V_{t+1}(x),$$

with $V_{T+1}(x)=0$ and $V_t(0)=0$. An optimal subset $\hat S_t(x)$ is a maximizer of the problem on the right side. The marginal value of capacity is $\Delta V_t(x)=V_t(x)-V_t(x-1)$.

Formalization targets

Goal: Theorem 5 (p. 1329)

There exists an optimal policy, i.e. a choice of maximizers $\hat S_t(x)$ for all $1\le t\le T$, $1\le x\le c$, such that

$$\hat S_t(x-1)\subseteq \hat S_t(x)\qquad\text{and}\qquad \hat S_{t-1}(x)\subseteq\hat S_t(x).$$

The offer set shrinks as capacity runs down, and it is smaller when more periods remain.

Milestones

1. (§2, p. 1325) The (Balance) equations have a unique nonnegative solution for every $S$.
2. (Theorem 2, p. 1326) If $\hat v$ is optimal for (Dual), then $\{j:\hat v_j=r_j\}$ is optimal for (Assortment).
3. (Lemma 3, p. 1327) For $\eta\ge0$, with $\hat v^\eta$ optimal for (Dual) with revenues $r_j-\eta$,

$$\{j:\hat v^\eta_j=r_j-\eta\}\subseteq\{j:\hat v^0_j=r_j\}.$$

4. ((Single Resource), pp. 1328–1329) The value functions satisfy the printed recursion $V_t(x)=\max_S\{\sum_jP_{j,S}\{r_j+V_{t+1}(x-1)\}+\{1-\sum_jP_{j,S}\}V_{t+1}(x)\}$ and the boundary conditions.
5. (Proof of Theorem 5, p. 1329) $\Delta V_{t+1}(x)\le\Delta V_{t+1}(x-1)$ and $\Delta V_{t+1}(x)\le\Delta V_t(x)$.

Significance

Theorem 5 makes the optimal policy a protection level policy: for each product $j$ and period $t$ there is a threshold $\bar x_{jt}$ such that $j$ is offered exactly when at least $\bar x_{jt}$ units remain. The policy can then be stored as $n\,T$ numbers instead of a table of subsets, and each product can be controlled separately, which is how airline inventory systems are organized. The paper also shows (Table 2, p. 1330) that the products need not be closed in revenue order: a higher-fare product can be closed before a lower-fare one, so the result is genuinely about nested sets, not about nested fare classes. Talluri and van Ryzin (2004) show that under the multinomial logit model an optimal assortment consists of a number of products with the largest revenues; the Markov chain choice model does not have this property (Table 1, p. 1328), so their structure of the optimal policy does not carry over directly.

The result is proved in the paper. No part of it is formalized on Prove2Me. The monotonicity of marginal values for an abstract choice model is published and proved as RevenueManagement.choice_marginal_values, stated over the definitions RevenueManagement_singleResource; milestone 5 is the same statement for this paper's dynamic program and can be bridged to it. A complete development here produces machine-checked Theorem 2 and Lemma 3 for the Markov chain choice model, which are reusable for any assortment problem under this model.

Difficulty

The obvious argument chooses, for each $(t,x)$, any maximizer of the stage problem. This fails: the stage problems have ties, and an arbitrary choice of maximizers need not be nested, so the theorem is an existence statement about a coordinated choice. The dependence of $P_{j,S}$ on $S$ is through the solution of a linear system, so the effect of adding or removing a product on the other purchase probabilities has no simple sign, and optimal assortments need not be nested by revenue (Table 1, p. 1328). The link between two stage problems is that their revenues differ by the same constant for all products, and what has to be shown is that such a uniform shift moves an optimal assortment in a controlled direction. Revenues in the stage problems, $r_j-\Delta V_{t+1}(x)$, can be negative.

Formalization scope

Products are Fin n, offer sets Finset (Fin n), the paper's $\subset$ is non-strict inclusion $\subseteq$. The model is a structure with fields $\lambda$, $\rho$ and the standing assumptions $\lambda_j>0$, $\sum_i\rho_{j,i}<1$; $\rho_{j,i}\ge0$ is added as a field because the $\rho_{j,i}$ are probabilities. $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it is the unique nonnegative one. The value function is defined by recursion on the number of periods to go, and $V_t$ is used only for $1\le t\le T+1$. Maxima over $S\subseteq N$ are taken over the finite family of all subsets, so they are attained; dual optimality is "feasible and no worse than every feasible point".

One hypothesis is added to Theorem 5 and milestone 5, and disclosed: $\sum_j\lambda_j\le1$, implied by the paper's description of at most one arrival per period (it makes $1-\sum_jP_{j,S}$ a probability). No sign condition is placed on the revenues, as on the page. Theorem 2 and Lemma 3 are stated for arbitrary real revenues, as the proof of Theorem 5 applies them to $r_j-\Delta V_{t+1}(x)$. The first inclusion of Theorem 5 is stated for $x\ge2$: with $x-1=0$ units there is no decision, and the paper reads $\hat S_t(0)$ as $\emptyset$. The existential requires every $\hat S_t(x)$ in range to be optimal for its stage problem; a statement without that clause would be satisfied by the empty sets and is ruled out.

Theorem 2 and Lemma 3 need LP duality for (Dual) and the (Balance) system; milestone 5 needs the standard induction on the dynamic program, or a bridge to the published choice_marginal_values (with arrival probabilities $1$ and choice model $P_{j,S}$). Proofs of any milestone, and bridges to published Mathlib or platform LP duality results, are welcome.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• K. Talluri, G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Motivation

A retailer or an airline decides which products to make available, and customers choose among what is offered. When a preferred product is missing, many customers substitute to another product instead of leaving. Assortment optimization asks which subset of products to offer so that the expected revenue from a customer is as large as possible, and its answer depends entirely on the choice model used to describe substitution.

The Markov chain choice model was introduced by Blanchet, Gallego and Goyal (EC 2013; Oper. Res. 64(4), 2016), who showed that it contains the multinomial logit model as a special case and proposed it as an approximation of general random-utility choice models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study revenue management under this model. Their first result, the subject of this mission, is that the assortment problem, a search over all $2^n$ offer sets, is solved by one linear program with $n$ variables. The same paper uses this result for its dynamic single-resource and network results, which are the subjects of the companion missions II–IV of this series.

Timeline:

• 2013/2016: Blanchet, Gallego and Goyal introduce the model and give a polynomial-time assortment algorithm.
• 2017: Feldman and Topaloglu show that the optimal assortment is read off an optimal solution of a dual linear program (their Theorem 2), and derive structural and capacity-control consequences.

Setting

There are $n$ products $N=\{1,\dots,n\}$. A customer arrives to purchase product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she transitions to product $i$ with probability $\rho_{j,i}$ and checks whether $i$ is offered, or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. Throughout, $\lambda_j>0$, $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j$.

For an offer set $S\subseteq N$, let $P_{j,S}$ be the expected number of visits to product $j$ while it is offered (the probability that $j$ is purchased) and $R_{j,S}$ the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the unique solution of the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .$$

With revenue $r_j\in\mathbb R$ for product $j$, the (Assortment) problem is $\max_{S\subseteq N}\sum_{j\in N}P_{j,S}r_j$. Two linear programs enter: the maximization of $\sum_j r_jx_j$ over the polyhedron

$$\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+:\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\},$$

and its dual

$$\min_{v\in\mathbb R^n}\Big\{\sum_{j\in N}\lambda_jv_j:\ v_j\ge r_j\ \ \forall j\in N,\ \ v_j\ge\sum_{i\in N}\rho_{j,i}v_i\ \ \forall j\in N\Big\}.\qquad\text{(Dual)}$$

Formalization targets

Goal: Theorem 2 (p. 1326)

For every optimal solution $\hat v$ of (Dual), the set $\hat S=\{j\in N:\hat v_j=r_j\}$ is an optimal assortment:

$$\sum_{j\in N}P_{j,S}\,r_j\ \le\ \sum_{j\in N}P_{j,\hat S}\,r_j\qquad\text{for all } S\subseteq N .$$

Milestones, in the order the paper uses them

1. (p. 1325) The (Balance) equations have a unique nonnegative solution for every $S$.
2. Lemma 1 (p. 1326): for an extreme point $(\hat x,\hat z)$ of $\mathcal H$ and $S_{\hat x}=\{j:\hat x_j>0\}$, $P_{j,S_{\hat x}}=\hat x_j$ and $R_{j,S_{\hat x}}=\hat z_j$ for all $j$.
3. (p. 1326) The linear program over $\mathcal H$ has an optimal solution, and its optimal value equals the optimal value of (Assortment).
4. (p. 1326) (Dual) has an optimal solution, and its optimal value equals that of the linear program over $\mathcal H$.
5. (p. 1326, proof of Theorem 2) An optimal $\hat v$ satisfies $\hat v_j=r_j$ or $\hat v_j=\sum_i\rho_{j,i}\hat v_i$ for each $j$.

Significance

Theorem 2 reduces a combinatorial problem over $2^n$ offer sets to a linear program, so the assortment problem under the Markov chain choice model is solvable in polynomial time. The same structure drives the rest of the paper: the dual variables $\hat v_j$ are used to show that optimal offer sets shrink when all revenues fall by a common amount, to show that the optimal offer sets of the single-resource dynamic program are nested in the remaining capacity and time, and to reduce the choice-based network linear program to a compact one.

The result is proved in the paper. This mission produces a machine-checked version of it and of its supporting lemmas; to the knowledge of the mission author no formalization of the Markov chain choice model exists. The definition layer (the model, the (Balance) solution, $\mathcal H$ and (Dual)) is the first formal encoding of this choice model and is shared, with the same encoding, by missions II–IV.

Difficulty

The obvious route, comparing $\sum_jP_{j,S}r_j$ across offer sets directly, fails because $P_{j,S}$ is defined only implicitly through a linear system whose coefficient matrix changes with $S$; there is no closed-form expression that can be compared across offer sets, and enumerating the $2^n$ sets is exponential. The connection to linear programming needs an exact correspondence between the vertices of $\mathcal H$ and the (Balance) solutions, which is a statement about polyhedra, not about Markov chains. Even well-posedness is not free: existence, uniqueness and nonnegativity of $(P_S,R_S)$ depend on the row sums $\sum_i\rho_{j,i}$ being strictly below one. Mathlib has extreme points of convex sets but no ready-made theory of vertices of polyhedra or of linear programming duality in this form.

Formalization scope

Products are Fin n (0-based), offer sets are Finset (Fin n) (the paper's $S\subset N$ is non-strict inclusion, so every subset including $\emptyset$ and $N$ is an offer set), and rho j i is $\rho_{j,i}$, the transition from $j$ to $i$. The model structure carries the paper's standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$ (p. 1325) and the implicit nonnegativity $\rho_{j,i}\ge0$. Revenues are arbitrary reals with no sign assumption. $\mathbb R^{2n}$ is (Fin n → ℝ) × (Fin n → ℝ), and extreme points are Mathlib's Set.extremePoints ℝ.

The pair $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it satisfies (Balance), is nonnegative and equals every solution, so all statements are about the paper's $(P_S,R_S)$ and not about a junk value. Every optimum (of (Assortment), of the linear program over $\mathcal H$, of (Dual)) is stated as "feasible and at least as good as every feasible point", never through sSup or sInf. The goal is stated for every optimal $\hat v$ of (Dual), which is what the proof uses; uniqueness of $\hat v$ is neither assumed nor claimed. Replacing the hypothesis "$\hat v$ optimal for (Dual)" by "$\hat v$ feasible for (Dual)" would make the statement false, and an existential over $\hat v$ would weaken it; neither is the target.

No hypothesis beyond the paper's is added. Two printed index slips on pp. 1325–1326 (a garbled sum in the discussion after (Balance), and $\sum_i\rho_{i,j}\hat z_j$ for $\sum_i\rho_{i,j}\hat z_i$ in the proof of Lemma 1) are not part of any statement here.

Welcome contributions: the existence and uniqueness of (Balance) solutions via Neumann series for substochastic matrices, a characterization of vertices of polyhedra given by equality constraints and nonnegativity, and a strong duality statement usable for this primal–dual pair. These are reusable well beyond this mission.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Insertion heuristics build a traveling salesman tour one city at a time: start from a single city, and at each step choose a city not yet on the subtour and splice it into the subtour where it lengthens the subtour least. Local search heuristics start from a tour and repeatedly replace a few of its edges by others while this shortens the tour. Both families are standard in practice, and a natural engineering idea is to combine them: run an insertion heuristic, then polish the result by local search. The question this mission formalizes is whether local optimality of the insertion tour certifies anything about its quality.

Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) answered this for graphs satisfying the triangle inequality. Their §4 proves that nearest and cheapest insertion always return a tour of length at most $2(1-1/n)$ times the optimal length, and their Theorem 5 shows this bound is attained. Their §7 then shows that the very tour attaining the bound is $k$-optimal for every $k\le n/4$: no exchange of $k$ edges shortens it. So the insertion bound is tight even for tours that local search with $k$-changes cannot improve.

Timeline, as far as this mission is concerned:

• 1965: Lin (Bell System Tech. J. 44) defines $k$-optimal tours and uses 3-optimal local search.
• 1973: Lin and Kernighan (Oper. Res. 21) generalize the edge-exchange neighbourhoods.
• 1977: Rosenkrantz, Stearns and Lewis prove the $2(1-1/n)$ upper bound for nearest and cheapest insertion (Theorem 4 and its corollary), its tightness for $n\ge 6$ (Theorem 5), the existence of $k$-optimal tours with the same ratio (Theorem 6, stated for $n\ge 8$), and the Corollary combining the two.

Setting

A traveling salesman graph on $n$ nodes is the node set $N=\{1,\dots,n\}$ with a distance $d(i,j)\ge 0$ that is symmetric and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$. A tour is a Hamiltonian circuit; its length is the sum of its edge lengths; OPTIMAL is the least length of a tour. As in the paper, the identically zero distance is excluded, so OPTIMAL $>0$.

A subtour is a circuit on a subset of the nodes (a single node is a subtour without edges). For a subtour $T$ and a node $k\notin T$, TOUR$(T,k)$ is obtained by deleting an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and adding $(x,k)$ and $(k,y)$; COST$(T,k)$ is the resulting increase in length. An insertion method chooses nodes $a_0,a_1,\dots,a_{n-1}$, starts from $T_1=\{a_0\}$ and sets $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$; INSERT is the length of $T_n$. Nearest insertion chooses $a_i$ minimizing $d(T_i,x)=\min_{y\in T_i}d(y,x)$ over $x\notin T_i$; cheapest insertion chooses $a_i$ minimizing COST$(T_i,x)$. Ties are broken arbitrarily.

A $k$-change of a tour deletes $k$ of its edges and adds $k$ other edges so that another tour is obtained. A tour is $k$-optimal if no $k$-change produces a strictly shorter tour.

The extremal instance is the circle $(N_n,d_n)$: $n$ cities equally spaced on a circular road, with $d_n(i,j)$ the smallest $m\ge 0$ with $i-j\equiv m$ or $j-i\equiv m \pmod n$. The insertion run of Theorem 5 inserts the cities in the order $1,2,\dots,n$ and produces the zig-zag tour $T_n$: city 1, then the even cities in increasing order, then the odd cities in decreasing order.

Formalization targets

Goal: the Corollary to Theorem 6

For $n\ge 6$ and $4k\le n$ there is a traveling salesman graph with OPTIMAL $>0$ on which some run of nearest insertion, and some run of cheapest insertion, return a $k$-optimal tour with

$$\frac{\mathrm{INSERT}}{\mathrm{OPTIMAL}}=2\left(1-\frac1n\right).$$

Milestones

1. The insertion run on the circle: the subtours $T_i$ and nodes $a_i=i+1$ form an insertion run that obeys both the nearest and the cheapest rule (proof of Theorem 5).
2. On the circle, $T_n$ has length $2(n-1)$ and OPTIMAL $=n$ (proof of Theorem 5).
3. Theorem 5: for $n\ge 6$ there is a graph with INSERT/OPTIMAL $=2(1-1/n)$ for both methods.
4. Equation (7.4): the length of a tour of the circle is the sum over unit edges $e$ of COUNT$(e,T)$, the number of times $e$ is traversed when each tour edge is replaced by a shortest arc.
5. Every tour of the circle is odd or even (all counts of one parity), eq. (7.5).
6. $T_n$ is the shortest even tour, so every tour shorter than $T_n$ is odd.
7. $T_n$ is $k$-optimal for every $k\le n/4$.
8. Theorem 6: for $n\ge 8$ there is a graph with a tour that is $k$-optimal for all $k\le n/4$ and has LOCALOPT/OPTIMAL $=2(1-1/n)$.

Significance

The result. The Corollary shows that the $2(1-1/n)$ worst-case guarantee of nearest and cheapest insertion cannot be improved by requiring that the returned tour survive $k$-change local search, for $k$ up to a quarter of the number of cities. Theorem 6 says more generally that $k$-optimality with $k\le n/4$ does not bound the ratio to the optimum below $2(1-1/n)$. Together with the paper's upper bound, the insertion guarantee is exact, and it stays exact after local polishing with small neighbourhoods.

Formalizing it. All statements are proved in the paper; none, to our knowledge, has been machine-checked. The platform has an upper bound for nearest insertion (SupplyChainTheory, Theorem 10.7, ratio at most 2) but no tightness example and no notion of $k$-optimality. This mission produces a reusable definition of $k$-changes against arbitrary tours, the circle metric, and the parity-counting argument on a cycle, and it supplies the calculations the paper omits ("We omit these calculations but note that they require the assumption $n\ge 6$").

Difficulty

Two steps carry the weight. First, the omitted calculations for the insertion run: at each stage one must show that inserting $a_i$ between $i-1$ and $i$ minimizes the insertion increase over every edge of the zig-zag subtour, and that no other outside city can be inserted for less than 2; the claim fails for $n=4$ and $n=5$, so the verification must use $n\ge 6$ in an essential way. Second, $k$-optimality is a statement about every tour at edge difference $k$, not about 2-opt segment reversals or any specific move family. A search over moves of a special form does not establish it; the argument must bound the length of an arbitrary tour at edge difference $k$ from below.

Formalization scope

Nodes are Fin n, so the paper's node $m$ is index $m-1$ and $a_i=i+1$ is index $i$; subtour indices stay 1-based ($T_1=[a_0]$, approximation $T_n$). A distance is d : Fin n → Fin n → ℝ with the structure IsTSPDist (symmetric, nonnegative, triangle inequality, and $d(i,i)=0$; the last is a normalization absent from the paper that changes no length). A tour is an Equiv.Perm (Fin n), a subtour a list read cyclically; OPTIMAL is Finset.univ.inf' over permutations, the true minimum. TOUR$(T,k)$ is insertion at a position minimizing the new length; COST is a minimum over positions; the nearest-insertion distance (4.1) takes values in WithTop ℝ, so no junk value arises. $k$-optimality compares the tour with every permutation whose edge set (unordered pairs) misses exactly $k$ of the tour's edges. Ratios are multiplied out.

COUNT$(e,T)$ needs a choice of shortest arc for antipodal pairs when $n$ is even; the formalization takes the arc through $\min(x,y),\dots,\max(x,y)$. The paper's argument does not depend on this choice.

Deviations from the printed text: the Corollary is stated for $n\ge 6$ (the printed statement says only $4k\le n$, but its proof uses the example of Theorem 5, which exists for $n\ge 6$; for $k=0$, $n=3$ the printed statement is false). Theorem 6 keeps its printed $n\ge 8$. In the proof of Theorem 5 the paper writes "(4.2) holds" where the cheapest-insertion condition (4.3) is meant; the formal statement uses (4.3).

The existence statements carry OPTIMAL $>0$, the paper's standing assumption (1.1). Without it, the zero distance would make every length zero and every tour $k$-optimal, which would satisfy the ratio equations trivially; that formalization is ruled out.

Contributions welcome: proofs of any milestone, in particular the omitted insertion calculations and the parity lemma, and reusable lemmas on cyclic lists and edge sets of permutations.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• S. Lin, Computer solutions of the traveling salesman problem, Bell System Tech. J. 44:2245–2269, 1965. https://doi.org/10.1002/j.1538-7305.1965.tb04146.x
• S. Lin, B. W. Kernighan, An effective heuristic algorithm for the traveling-salesman problem, Oper. Res. 21(2):498–516, 1973. https://doi.org/10.1287/opre.21.2.498

Motivation

In a combinatorial auction a set of $m$ items is sold to $n$ bidders who value bundles of items rather than single items. Spectrum auctions, procurement of transportation lanes and the allocation of cloud resources all have this form, and the central algorithmic question is how to allocate the items so as to maximize the social welfare, the sum of the bidders' values for what they receive. Even to describe a general valuation takes $2^m$ numbers, so algorithms access the bidders through queries, and the achievable approximation depends on the class of valuations allowed.

Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) study bidders without complementarities. For the class of XOS valuations, maxima of additive valuations, which strictly contains the submodular valuations, they give LP-based algorithms and, in §3.3, a purely combinatorial algorithm: bidders arrive one at a time, take their demanded bundle at the current item prices, and raise the prices of what they took. Its analysis charges the welfare of any allocation to the item prices the algorithm sets, an argument that uses only the demand and XOS oracles.

Setting

The items are $M=\{1,\dots,m\}$ and the bidders $1,\dots,n$.

• An additive valuation (a clause) $w$ assigns nonnegative values $w(1),\dots,w(m)$ to the items and $w(S)=\sum_{j\in S}w(j)$ to a bundle $S\subseteq M$.
• An XOS valuation $v$ is given by a nonempty finite set of clauses $\{w_1,\dots,w_t\}$ (its XOS expression) through $v(S)=\max_k w_k(S)$. A clause $w_k$ with $w_k(S)=v(S)$ is a maximizing clause for $S$. Every XOS valuation is normalized, $v(\emptyset)=0$, and monotone.
• An allocation is a tuple of pairwise disjoint bundles $O_1,\dots,O_n$; items may stay unallocated. Its welfare is $\sum_i v_i(O_i)$.
• A demand oracle for bidder $i$ answers, given item prices $p\in\mathbb R^m$, a bundle maximizing $v_i(T)-\sum_{j\in T}p_j$. An XOS oracle answers, given a bundle $S$, a maximizing clause for $S$ in $v_i$.

The greedy price-update algorithm. Start with all bundles empty and all prices $p_j=0$. For $i=1,\dots,n$: let $S_i$ be bidder $i$'s demand at the current prices; remove the items of $S_i$ from the bundles of the earlier bidders; let $q^i$ be the maximizing clause for $S_i$ in $v_i$; set $p_j=q^i_j$ for $j\in S_i$. Write $p^k$ for the prices after stage $k$ ($p^0=0$), $p^k(T)=\sum_{j\in T}p^k_j$, and $A_1,\dots,A_n$ for the final bundles.

In the Lean development these objects are XOSExpr, XOSExpr.val, IsAllocation, welfare, IsDemandOracle, IsXOSOracle, greedyState, greedyPrices and greedyAlloc in the namespace ComplementFreeCA.XOSGreedy.

Formalization targets

Goal: Theorem 3.3

For XOS valuations $v_1,\dots,v_n$, every demand oracle and every XOS oracle, and every allocation $O_1,\dots,O_n$,

$$\sum_{i=1}^n v_i(O_i)\;\le\;2\sum_{i=1}^n v_i(A_i).$$

The comparison with every allocation is the paper's comparison with the optimal allocation.

Milestones

1. Lemma 3.4. The final prices are paid for by the algorithm's welfare:

$$p^n(M)\le\sum_i v_i(A_i).$$

2. Lemma 3.5. Prices never decrease: $p^k_j\le p^{k'}_j$ for all items $j$ and stages $k\le k'$.
3. Lemma 3.6. For every allocation $O$,

$$\sum_i v_i(O_i)\le 2\,p^n(M).$$

Three further statements are included without being milestones: the output $A_1,\dots,A_n$ is an allocation (used implicitly by the paper); the first sentence of the proof of Lemma 3.6, that with $\Delta^i=p^i(M)-p^{i-1}(M)$ one has $\Delta^i=\max_{T\subseteq M}\bigl(v_i(T)-p^{i-1}(T)\bigr)$; and the factor $2$ is attained on the paper's two-item, two-bidder example (p. 9).

Significance

Theorem 3.3 shows that a factor-2 approximation of the optimal welfare for XOS bidders needs no linear program: one pass over the bidders, one demand query and one XOS query each. The paper's LP-based algorithm of §3.2 attains the better ratio $e/(e-1)$, and Theorem 4.1 of the paper shows that for the larger class of complement-free bidders no $(2-\epsilon)$-approximation is possible with polynomial communication.

The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. This mission produces a formal model of XOS valuations, demand and XOS oracles and the greedy run that is reusable for other price-based arguments, and a formal proof of the guarantee for every tie-breaking in both oracles.

Difficulty

The argument is elementary, but its bookkeeping is where a formal proof can go wrong. Items move between bidders: an item taken from an earlier bidder in step (b) is re-priced in step (d), and every priced item lies in exactly one final bundle. Lemma 3.4 needs this invariant across all $n$ stages, together with the fact that a maximizing clause for the demanded set bounds $v_i$ on every subset, which holds because it is a clause of $v_i$ itself, not merely an additive function agreeing with $v_i$ on $S_i$. Lemma 3.5 is a contradiction argument using optimality of the demand; Lemma 3.6 telescopes the price increases and needs prices to stay nonnegative. The argument must hold for arbitrary oracle answers, so no canonical demand can be assumed.

Formalization scope

• Bidders are Fin n, items Fin m, bundles Finset (Fin m), values in ℝ. An XOS valuation is represented by its expression: a nonempty Finset (Fin m → ℝ) of clauses with nonnegative entries, evaluated with Finset.sup'. The paper's standing assumptions, normalized and monotone valuations (p. 1), hold automatically in this representation.
• The oracles are function parameters dem : Fin n → (Fin m → ℝ) → Finset (Fin m) and cl : Fin n → Finset (Fin m) → (Fin m → ℝ) with hypotheses IsDemandOracle and IsXOSOracle; every theorem holds for every such pair, so no tie-breaking rule is fixed.
• The run is a recursion on the stage: stage $k+1$ processes the 0-based bidder $k$, i.e. the paper's bidder $k+1$; after stage $n$ the state is constant.
• The paper's goal compares with the optimal allocation; the Lean goal compares with every allocation, which is equivalent and avoids an argmax. Stating the bound against one particular allocation, or against the algorithm's own output, would be trivial and is excluded.
• There are no $O(\cdot)$ constants: the factor $2$ is the paper's.
• Printed slip: the model on p. 1 writes an allocation as $S_1,\dots,S_m$; it is one bundle per bidder, $S_1,\dots,S_n$.
• Out of scope: running time, the cost of simulating oracles (Proposition 2.1), and communication lower bounds.

Contributions welcome: proofs of the three milestones and of the goal, and reusable lemmas on the invariant that every priced item lies in exactly one final bundle.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• B. Lehmann, D. Lehmann, N. Nisan, Combinatorial auctions with decreasing marginal utilities, Games and Economic Behavior 55(2):270–296, 2006. https://doi.org/10.1016/j.geb.2005.02.006