The OR Formalization Drive

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts IV: Competing Newsvendors with Proportional Allocation Have a Unique Equilibrium, and a Coordinating Buy-Back Gives the Supplier ((p(n − 1) + b)/(pn))Π(q°)Textbook

Why competing retailers change the contracting problem

A supplier who sells through a single newsvendor retailer faces double marginalization: the retailer bears the whole cost of leftover stock but earns only the retail margin, so under a plain wholesale-price contract he orders less than the integrated supply chain would. The literature reviewed in G. P. Cachon's chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) shows that buy-back, revenue-sharing and related contracts correct this distortion. Section 6.5 asks what happens when the supplier sells through several retailers who compete for the same customers.

Competition can push in the opposite direction. When customers buy wherever stock is available, a retailer who stocks more also takes demand from his rivals, and he does not count that loss as a cost. This demand-stealing effect pushes the retailers towards over-ordering, which offsets double marginalization. §6.5.1 makes this precise in the proportional allocation model, in which total demand is split among the retailers in proportion to their inventories. The model goes back to the deterministic version of Wang and Gerchak (2001); related allocation models are those of Lippman and McCardle (1997) and Anupindi and Bassok (1999), and Mahajan and van Ryzin (2001) observe the same mitigation of the need for coordinating contracts.

This mission formalizes §6.5.1 of the chapter's January 2003 third draft, pp. 48–53.

The proportional allocation model

There are $n \ge 2$ retailers and one supplier. Total retail demand $D \ge 0$ is random, with distribution function $F$ that is differentiable on $(0,\infty)$ with density $f$ , strictly increasing on $[0,\infty)$ , and satisfies $F(0)=0$ . The retail price is $p$ and the supplier's unit production cost is $c$ , with $0 < c < p$ . Goodwill costs, the salvage value and the retailers' handling cost are zero.

Retailer $i$ orders $q_i \ge 0$ . Write $q = \sum_j q_j$ and $q_{-i} = q - q_i$ . Retailer $i$ receives the demand $D_i = (q_i/q)D$ . Under a buy-back contract $(w, b)$ he pays $w$ per unit ordered and is refunded $b$ per unit left over; $b = 0$ is the wholesale-price contract. His expected profit is

\pi_i(q_i, q_{-i}) = \mathbb E\big[p\min(q_i, D_i) + b(q_i - D_i)^+\big] - wq_i = (p-w)q_i - (p-b)\frac{q_i}{q}\int_0^q F(x)\,dx .

Because total sales $\min(q, D)$ depend only on the total stock, the integrated chain earns $\Pi(q) = pS(q) - cq$ with $S(q) = \mathbb E[\min(q,D)]$ , and its optimal stock $q^o$ solves the newsvendor equation $F(q^o) = (p-c)/p$ , Eq. (20). A Nash equilibrium is a profile of orders in which each $q^*_i$ maximizes $\pi_i(\cdot, q^*_{-i})$ over all orders $x \ge 0$ . A contract coordinates the chain when its equilibrium total order is $q^o$ .

Two contract prices appear on p. 52: the wholesale price $\widehat w(q) = p\big(1 - \tfrac1n F(q) - \tfrac{n-1}{n}\cdot\tfrac1q\int_0^qF\big)$ that induces total stock $q$ , and the buy-back wholesale price

w_b(b) = p - (p-b)\left[\frac1n\cdot\frac{p-c}{p} + \frac{n-1}{n}\cdot\frac{1}{q^o}\int_0^{q^o}F(x)\,dx\right].

Formalization targets

Goal: the coordinating buy-back contract (pp. 51–53)

For $n \ge 2$ , $b < p$ and $q^o$ solving (20), with $w = w_b(b)$ : $q^o$ maximizes $\Pi$ ; $b < w_b(b) < p$ ; the profile in which every retailer orders $q^o/n$ is the unique Nash equilibrium; and at that equilibrium

\pi_i = \frac{p-b}{pn^2}\,\Pi(q^o), \qquad \pi_s = wq^o - cq^o - b\,\mathbb E[(q^o-D)^+] = \frac{p(n-1)+b}{pn}\,\Pi(q^o).

Milestones

The milestones are the section's own claims, in attack order: the newsvendor characterization (20); the inequality $\frac1q\int_0^qF < F(q)$ ; the closed form of $\pi_i$ and its strict concavity in the retailer's own order (p. 50); the first-order condition and Eq. (21); the monotonicity and limits of the left side $L_n$ of Eq. (22), giving a unique root for $b < w < p$ ; the unique, symmetric Nash equilibrium for every $b < w < p$ ; the increase of the equilibrium total in $n$ ; that $\widehat w(q)$ induces $q$ , that $\widehat w(q^o) > c$ , and that the supplier's profit under wholesale pricing has negative slope at $q^o$ ; the coordinating price $w_b(b)$ with $w_b(b) > \widehat w(q^o)$ for $b > 0$ ; and the ratio $\pi_s(q^o, w_b(0), 0)/\Pi(q^o) = (n-1)/n$ (p. 53). A companion item states the endpoint $b = p$ , at which the supplier takes all of $\Pi(q^o)$ .

Significance

The section answers two questions. First, with competing retailers a plain wholesale-price contract can coordinate the chain and still leave the supplier a positive margin, which a single retailer never allows. Second, that contract is not the supplier's best wholesale price, and it fixes a single division of profit. Buy-back contracts remove both limitations: the family $(w_b(b), b)$ coordinates for every $b < p$ and moves the supplier's share continuously from $(n-1)/n$ to all of $\Pi(q^o)$ . The ratio $(n-1)/n$ also measures how little a coordinating contract adds when many retailers compete (80% of the optimal profit at $n = 5$ ).

The results are proved in the chapter, mostly by short computations, and none of them has been machine-checked. The formalization makes explicit what the page leaves implicit: that no equilibrium has a retailer ordering zero, the limits behind "from 0 to 1", and the density condition behind the strict sign on p. 52. It also produces a reusable proportional-allocation game and a Nash-equilibrium predicate for nonnegative real strategies.

Difficulty

The algebraic identities (the profits at the coordinating contract, the ratio $(n-1)/n$ , the derivative at $q^o$ ) are routine once $\pi_i$ has its closed form. The closed form itself requires computing the expectation with proportional shares and identifying $\mathbb E[\min(q,D)]$ with $q - \int_0^q F$ .

The real obstacle is the uniqueness of the equilibrium. The page argues from first-order conditions, which describe only interior best responses. A complete proof must show that each retailer's profit is strictly concave in his own order, that no retailer orders zero in equilibrium, and that the all-zero profile (where $\pi_i$ has $q = 0$ in a denominator) is not an equilibrium. Strict concavity is the delicate step. The second derivative mixes the density with the term $\frac{2q_{-i}}{q^3}\big(qF(q) - \int_0^qF\big)$ , and concavity has to be established on the closed half-line, including the boundary $q_i = 0$ .

Formalization scope

Retailers are indexed by Fin n with $n \ge 2$ (the page's $n > 1$ ). The comparison in $n$ also allows a single retailer, as the page does. Orders are real numbers $q_i \ge 0$ , and best responses range over all $x \ge 0$ . The demand law is a probability measure on $\mathbb R$ carried by $[0,\infty)$ with finite mean, $F$ is its cdf, and $f$ is a field with HasDerivAt F (f y) y for $y > 0$ . These are the chapter's standing assumptions (p. 7). The condition $c > 0$ is needed for (20) to have a solution. The integrated optimum $q^o$ enters each theorem through the hypothesis $F(q^o) = (p-c)/p$ , which determines it uniquely. Transfers run from the retailers to the supplier.

Added or made explicit relative to the page: $b < p$ in the concavity claim (at $b = p$ the profit is linear); $f(q^o) > 0$ for the strict sign of the supplier's marginal profit; positivity of the total order wherever $\frac1q\int_0^qF$ appears. The page's printed slips (the first-order condition rescaled by $q^*/(p-b)$ , " $F(q^o) = (p-c)/c$ ", " $w(b)$ ") are corrected in the statements and kept in the milestone quotes.

Ruled out as trivializing: $\widehat w$ and $w_b$ are the printed formulas, not "the price at which $q^o$ is an equilibrium"; the supplier's profit is computed from the transfers, not as $\Pi$ minus the retailers' profits; the equilibrium statement quantifies over all nonnegative deviations, so restricting attention to interior or symmetric profiles is not an option.

A complete development needs interval integrals of a cdf, the fundamental theorem of calculus for $q \mapsto \int_0^qF$ , and strict concavity from a strictly decreasing derivative. The proportional-allocation game and the Nash predicate are reusable for the other allocation models of §6.5. No platform item is referenced: the competing-retailer game of Cachon and Lariviere (2005), RevShareCoord.Competing.*, uses deterministic revenue functions and is a different model.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; read in the author's 3rd draft (Jan. 2003), §6.5.1. https://doi.org/10.1016/S0927-0507(03)11006-7
Y. Wang and Y. Gerchak, Supply chain coordination when demand is shelf-space dependent, Manufacturing & Service Operations Management 3(1), 2001, 82–87. https://doi.org/10.1287/msom.3.1.82.9998
S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 1997, 54–65. https://doi.org/10.1287/opre.45.1.54
S. Mahajan and G. van Ryzin, Inventory competition under dynamic consumer choice, Operations Research 49(5), 2001, 646–657. https://doi.org/10.1287/opre.49.5.646.10603
G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

18 thms4 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Motivation

Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling problems. Their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, Report BW 43/75, 1975; journal version in Annals of Discrete Mathematics 1, 1977) introduced the four-field notation $n|m|\ell,\lambda|k$ that, in refined form, is still the standard classification of scheduling problems, and proved NP-completeness of the "easiest" hard problems by explicit reductions.

Single-machine problems with due dates sit right at that boundary. Minimizing the maximum lateness $L_{\max}$ is solved by Jackson's earliest-due-date rule (1955), and minimizing the number of late jobs by Moore's algorithm (1968). Theorem 4 of the report shows that small changes to these problems — one release date, job weights, or due dates turned into deadlines under a weighted completion-time objective — make them NP-complete, by reduction from KNAPSACK. This mission formalizes four of those reductions, parts (b), (c), (e) and (f) of Theorem 4.

Timeline, as far as this mission is concerned:

1955: Jackson — $n|1||L_{\max}$ is solved by sequencing in order of nondecreasing due dates.
1968: Moore — $n|1||\sum U_j$ (unit weights, no release dates) is solvable in polynomial time.
1972: Karp — KNAPSACK (in the subset-sum form used here) is NP-complete; Karp also notes the reduction to $n|1||\sum w_jU_j$ , which the report cites for part (e).
1975: Brucker, Lenstra and Rinnooy Kan — Theorem 4: KNAPSACK reduces to ten scheduling problems, including the four single-machine problems of this mission.

Setting

A single-machine instance consists of $n\ge1$ jobs $J_1,\dots,J_n$ . Job $J_j$ needs $p_{j1}$ units of processing on the machine $M_1$ , has a weight $w_j$ , a release date $r_j$ and a due date $d_j$ ; all data are nonnegative integers. A schedule assigns to each job a starting time $B_j\ge r_j$ such that the occupied intervals $[B_j,B_j+p_{j1})$ of distinct jobs are disjoint. Idle time is allowed; a job with $p_{j1}=0$ occupies an empty interval. The completion time is $C_j=B_j+p_{j1}$ , the lateness is $L_j=C_j-d_j$ (possibly negative), and $U_j$ is $0$ if $C_j\le d_j$ and $1$ otherwise. The criteria are

L_{\max}=\max_j L_j,\qquad \sum w_jC_j=\sum_{j=1}^n w_jC_j,\qquad \sum w_jU_j=\sum_{j=1}^n w_jU_j .

The problem class is written in the $\lambda$ field: by default every $r_j=0$ ; $r_n\ge0$ allows a nonzero release date for the last job $J_n$ only; $w_j=1$ fixes unit weights; $L_{\max}\le0$ admits only schedules that meet every due date. A problem is turned into a yes/no question by asking whether a schedule with value $\le y$ exists.

KNAPSACK (Theorem 2(b) of the report): given positive integers $a_1,\dots,a_t,b$ , is there a subset $S\subseteq T=\{1,\dots,t\}$ with $\sum_{j\in S}a_j=b$ ? Write $A=\sum_{j\in T}a_j$ .

A problem $P'$ is reducible to $P$ , $P'\propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ whose answer is the same.

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

\mathsf{KNAPSACK}\propto n|1|L_{\max}\le0|\textstyle\sum w_jC_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0|L_{\max},

\mathsf{KNAPSACK}\propto n|1||\textstyle\sum w_jU_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0,w_j=1|\textstyle\sum w_jU_j ,

as polynomial-time many-one reductions between languages of binary strings.

Milestones: the four yes-instance equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A$ , and the paper's constructions:

4(c): $n=t+1$ ; $r_j=0$ , $p_{j1}=a_j$ , $d_j=A+1$ for $j\in T$ ; $r_n=b$ , $p_{n1}=1$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule has $L_{\max}\le0$ .
4(f): the same instance with unit weights; KNAPSACK has a solution iff some schedule has $\sum U_j\le0$ .
4(e): $n=t$ ; $p_{j1}=w_j=a_j$ , $d_j=b$ . KNAPSACK has a solution iff some schedule has $\sum w_jU_j\le A-b$ .
4(b): $n=t+1$ ; $p_{j1}=w_j=a_j$ , $d_j=A+1$ for $j\in T$ ; $p_{n1}=1$ , $w_n=0$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule meeting all due dates has

\sum w_jC_j\le y=\sum_{j,k\in T,\ j\le k}a_ja_k+A-b .

Significance

The result. Combined with the NP-completeness of KNAPSACK, the four reductions show that the four problems are NP-hard (in the ordinary sense; they admit pseudo-polynomial algorithms). Part (c) shows that Jackson's rule cannot be extended to a single nonzero release date unless P = NP; part (f) does the same for Moore's algorithm; part (e) explains why weights are essential in the late-jobs problem; part (b) shows that deadlines turn the weighted completion-time problem, solved by Smith's ratio rule without them, into a hard one. These are entries of the complexity tables that every later scheduling classification builds on.

Formalizing it. The reductions are classical and proved on paper, in a few lines each: for (c), (e) and (f) the report gives only the construction and a figure. None of them has a machine-checked proof. A complete formalization supplies the explicit equivalence over all feasible schedules (including schedules with idle time and arbitrary processing order), the handling of the inputs the proof sets aside by "we may assume that $0<b<A$ ", and the polynomial-time computability of the constructions in a Turing-machine model.

Difficulty

Each equivalence has an easy direction: a subset $S$ with sum $b$ gives the schedule "jobs of $S$ , then $J_n$ , then the rest" (Figures 4 and 7 of the report). The other direction must rule out every feasible schedule, not only the idle-free ones in the displayed order. The report gives no argument for this direction in (c), (e) and (f), and for (b) only a computation for idle-free schedules of one shape. The equivalences are false outside $0<b<A$ in some cases (for (c), any $b>A$ makes every schedule on time), so the goal's reduction must treat those inputs separately.

The heavier part is polynomial-time computability: the reduction must be a function on strings, computed by a one-tape Turing machine within a polynomial number of steps, that parses a binary-coded KNAPSACK instance, computes $A$ and the threshold (for (b), a sum of $O(t^2)$ products), and writes the coded scheduling instance — and maps malformed strings outside the target language.

Formalization scope

Model. Jobs are Fin n (0-based; $J_n$ is the last index), with $n>0$ in each target language. Starting times are natural numbers: Section 3 computes them from processing orders on integer data, and since all criteria here are regular and release dates survive left shifts, real starting times give the same yes-instances. Feasibility requires disjoint occupied intervals, including empty intervals when $p_{j1}=0$ . Idle time is allowed. Lateness is an integer.
Problem classes are binding. $r_n\ge0$ means at least one job and release date $0$ for every job except the last; $L_{\max}\le0$ in (b) is a constraint on schedules, not the criterion. Instances outside the class are not in the target language.
Thresholds. $y\in\mathbb N$ in all four languages; for $L_{\max}$ this restricts to nonnegative thresholds, enough for the paper's $y=0$ . " $L_{\max}\le y$ " is stated as " $L_j\le y$ for all $j$ ".
Codes. An instance with threshold $y$ is the list $n$ , then $p_{j1},w_j,r_j,d_j$ per job, then $y$ , each number in binary.
Reducibility. "Reducible" (Section 2) is read as Karp reducibility, CookPvsNP.PolyReducible from the published definition CookPvsNP_defs. The alphabet and binary number codes are those of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann); its SUBSET SUM language is not reused because it admits zero sizes, while the paper's KNAPSACK is over positive integers.
Explicit readings of loose phrases. "We may assume that $0<b<A$ " becomes a hypothesis of each milestone and an obligation on the goal's reduction. "Cf. reduction (i) and Figure 4", "Cf. Karp [19] and Figure 7" and "The equivalence follows immediately" become the stated equivalences over all feasible schedules. Reduction (c) does not specify weights; the shared construction uses unit weights.
Not trivializable. The equivalences are stated for the paper's explicit constructions, not for an existentially chosen instance; the target languages enforce the problem class; and the goal demands polynomial-time computability, not only the equivalence.
Infrastructure. A Turing-machine library for arithmetic on binary codes (parsing, addition, multiplication, comparison) is reusable across all seven missions of this series and across every reduction posed in the same framework. Contributions of such general lemmas are welcome.

Parts (a), (d) and (g)–(j) of Theorem 4 are formalized in other missions of this series.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum, Report BW 43/75, Amsterdam, 1975; journal version: J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in: Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
J. M. Moore, An n job, one machine sequencing algorithm for minimizing the number of late jobs, Management Science 15 (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
J. R. Jackson, Scheduling a production line to minimize maximum tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.

11 thms3 active usersReviewed

Combinatorics Operations Research Probability+1·Captain: mikedeng1

An Optimal Algorithm for On-line Bipartite Matching 1: RANKING Finds a Matching of Expected Size at Least n(1 − 1/e) − o(n) on Every Graph with a Perfect MatchingResearch Paper

Motivation

Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has a perfect matching, a fixed greedy priority can leave many girls unmatched. The paper introduced RANKING, which randomly chooses the boys' priority order once and then uses that order for every arrival.

The question is quantitative: how many pairs does RANKING guarantee in expectation against a graph and an arrival order chosen before its random ranking? The paper's target is a fraction approaching $1-1/e$ of the $n$ pairs in a perfect matching. Its printed Theorem 1 concerns an auxiliary algorithm called EARLY; the RANKING statement follows the intended chain through Lemmas 3 and 5. The original EARLY analysis has a gap for general upper-triangular matrices, so this mission states the RANKING target and the earlier, unaffected lemmas separately. This distinction matters because an assertion about EARLY would be a different formalization target.

Setting

A bipartite graph has a boy side $U$ and a girl side $V$ , each with $n$ vertices. An edge $(u,v)$ means that boy $u$ may be paired with girl $v$ . A matching is a collection of edges in which no boy or girl occurs twice. The standing hypothesis for the performance guarantee is that the graph has a perfect matching: some bijection from boys to girls selects an edge for every boy. The graph is otherwise arbitrary.

Girls arrive in a predetermined order. When girl $v$ arrives, only her incident edges are revealed. RANKING first chooses a uniformly random permutation $\pi$ of the boys. For each arriving girl, it selects the highest-ranked adjacent boy who is still unmatched, if one exists. Write $M_{\mathrm R}(G,\pi)$ for the final matching. The expected size is the finite average over all $n!$ rankings. The guarantee must hold for every graph and every predetermined arrival order; relabeling girls lets the formal statement fix their order to $n,n-1,\ldots,1$ .

The paper also uses a dual rows-arrive view. Boys arrive in an order and choose among eligible girls, whose priority order is fixed. This is the same greedy rule with the sides exchanged. For its triangular reduction, the columns are numbered $1,\ldots,n$ and column $n$ has highest priority. An upper-triangular matrix with unit diagonal is a graph with every edge $(i,i)$ and with an edge $(i,j)$ only when $i\le j$ . On such a graph, the auxiliary algorithm EARLY declines to match row $i$ if column $i$ is already covered by EARLY's own matching. For any matching $M$ , $D(M)$ denotes the indices for which both row $i$ and column $i$ are covered.

Formalization targets

RANKING guarantee

For every $\varepsilon>0$ , one threshold $N$ must work for every size $n\ge N$ and every graph $G$ with a perfect matching:

\mathbb E_{\pi\sim\mathrm{Unif}(S_n)}|M_{\mathrm R}(G,\pi)| \ge (1-e^{-1}-\varepsilon)n.

This is the uniform lower-bound reading of the paper's $n(1-1/e)-o(n)$ target. It does not prescribe a finite- $n$ additive constant. The mission goal is the RANKING assertion drawn from the paper's Theorem 1 and Lemmas 3 and 5. The six milestones formalize the paper's Lemmas 1–5 and the corollary to Lemma 4, in their source order. They cover the side-exchange identity, arbitrary refusal algorithms, the triangular reduction, the matching-count identity, its expected form, and the pointwise comparison with EARLY.

Significance

The guarantee gives a concrete worst-case floor for a simple randomized allocation rule: as the graph size grows, RANKING matches at least an asymptotic $1-1/e$ fraction of the pairs available in a perfect matching, in expectation. The order is selected before the random permutation, matching the paper's performance measure. The lower bound remains meaningful on sparse graphs and does not rely on a density assumption. The original paper also studies the limit on what any randomized online algorithm can guarantee; that upper-bound result is treated in a separate mission.

A formal development here would provide reusable finite definitions for online greedy matching, arbitrary state-dependent refusal, fixed-order duality, and uniform expectation over permutations. The goal is a theorem statement awaiting a machine-checked proof; compiling the draft declarations verifies their Lean syntax and types, not their truth. The local mission separates the valid early structural statements from later statements whose published EARLY argument does not justify them on general upper-triangular graphs.

Difficulty

The random permutation does not make the fate of different vertices independent. Matching one girl removes a boy who might be essential to a later girl, so a per-arrival probability estimate cannot simply be added across all arrivals. The dual and triangular views capture useful structure, but turning that structure into a uniform bound for every graph is the main obstacle. In particular, reasoning about EARLY as if its matched-column set had the same monotonicity as unrestricted RANKING fails on some upper-triangular matrices. A proof of the goal must establish the RANKING guarantee without treating those later EARLY statements as available facts.

Formalization scope

Boys and girls are both Fin n; an adjacency matrix is a relation between them. A published predicate represents a perfect matching as an edge-preserving bijection. The generic greedy run processes arrival times in increasing order and interprets a smaller priority index as higher rank. It makes a new matching decision only from the current matching and the arriving vertex. RANKING's returned edges are consistently ordered as (boy, girl), even though girls arrive. The dual run has rows arriving in an arbitrary permutation and takes column $n-1$ as highest priority in Lean's zero-based numbering. EARLY's refusal test consults the matching constructed by EARLY itself.

All expectations are finite averages over Equiv.Perm (Fin n), scaled by $1/n!$ . The formal $o(n)$ claim is $\forall\varepsilon>0,\ \exists N,\ \forall n\ge N,\ \forall G$ with a perfect matching, the displayed lower bound. Placing $N$ before $G$ preserves the worst-case meaning. The perfect-matching condition is essential: the empty graph cannot satisfy a positive linear guarantee. The triangular matrix in Lemma 3 retains every diagonal edge, so a zero matrix cannot witness the reduction. These conventions rule out vacuous versions of the goal and reduction.

The definitions of partial matching, covered vertices, greedy run, RANKING, EARLY, and uniform average are part of the mission. A complete proof may build further finite counting and permutation machinery; such lemmas can be shared beyond this paper. Contributions toward the six milestone statements, the goal, and faithful supporting results are in scope. Lemmas 6–12 and the printed EARLY Theorem 1 are outside this mission because their analysis depends on claims that fail for some matrices allowed by their surrounding assumptions.

Selected references

Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, 1990, pp. 352–358. DOI: 10.1145/100216.100262.

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Supply Chain Coordination with Contracts V: With Market-Clearing Prices the Best Wholesale Price Earns θ/(2(1 + θ)) or θ/8, Below the (1 + θ)/8 a Full-Refund Buy-Back AttainsTextbook

Motivation

A supplier that sells through many competing retailers usually worries that competition among them pushes orders too high, because each retailer ignores the demand it takes from the others. Deneckere, Marvel and Peck (1997) identified the opposite failure. When the retail price is set by the market after demand is realized, retailers who hold too much stock in a weak market bid the price down, and anticipating this, perfectly competitive retailers order too little. The supplier then needs a contract that raises orders, and the classical justification for resale price maintenance (a price floor imposed on retailers) comes out of this model. G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents the model in §6.5.2 as a closed-form example. In it the supplier's best wholesale price contract is computed explicitly and compared with two contracts that recover the monopoly profit: resale price maintenance and a full-refund buy-back.

This mission is volume V of a series that formalizes the section capstones of that chapter, read in the author's 3rd draft (January 2003), pp. 53–58.

Setting

Fix $\theta>1$ . Industry demand is low or high, each with probability $1/2$ . If the retailers hold a total stock $q$ , the market clearing price is

p_l(q)=(1-q)^+\ \text{(low state)},\qquad p_h(q)=\Big(1-\frac q\theta\Big)^+\ \text{(high state)}.

Leftover inventory has no salvage value, and the supplier's production cost is zero.

Monopolist benchmark. A single firm orders a stock $Q$ , observes the state, and sells $x_l\le Q$ (low) or $x_h\le Q$ (high) at the market clearing price. Its expected profit is $\tfrac12p_l(x_l)x_l+\tfrac12p_h(x_h)x_h$ , and $\Pi^o$ is the maximum of this.
Wholesale price contract. The supplier charges $w$ per unit. A continuum of retailers orders before demand is known and sells everything at the market clearing price. Their aggregate expected profit is

\pi(q)=\tfrac12p_l(q)q+\tfrac12p_h(q)q-wq .

Perfect competition means the retailers keep ordering until expected profit is zero. The competitive order is the $q>0$ with $\pi(q)=0$ and $\pi>0$ on $(0,q)$ . The supplier earns $wq$ .

Resale price maintenance $(\bar p,w)$ : retailers may not sell below $\bar p$ . When the clearing price would fall below $\bar p$ , only the demand at $\bar p$ is sold, allocated in proportion to stock.
Buy-back $(w,b)$ : the supplier pays $b$ per unsold unit. The market price then cannot fall below $b$ , and retailers sell at most $1-b$ units (low) and $\theta(1-b)$ units (high).

The page's notation $q_1(w)=\frac{2\theta}{1+\theta}(1-w)$ , $q_2(w)=\theta(1-2w)$ , $\pi_s(w)$ and $w^*(\theta)$ is kept in Lean under the names q1, q2, supplierProfit, wStar.

Formalization targets

Goal (pp. 55, 57)

With

\pi_s^*=\begin{cases}\dfrac{\theta}{2(1+\theta)}&\theta\le3,\\[4pt]\dfrac\theta8&\theta>3,\end{cases}

the goal states four things:

$\pi_s^*$ is the greatest supplier profit $wq$ over all wholesale prices and their competitive orders.
$w^*(\theta)$ attains it.
The monopolist's maximum is $\Pi^o=(1+\theta)/8$ , and $\pi_s^*<\Pi^o$ .
Under the buy-back $b=w=1/2$ the competitive order is $\theta/2$ and the supplier earns exactly $\Pi^o$ .

Milestones

$\Pi^o=(1+\theta)/8$ (p. 54).
The competitive order is $q_1(w)$ if $w\ge\tfrac12-\tfrac1{2\theta}$ and $q_2(w)$ otherwise, for $0\le w<1$ (p. 55).
$w^*(\theta)$ maximizes $\pi_s$ on $[0,1)$ , with the value $\pi_s^*$ (p. 55).
The orders and market clearing prices at $w^*(\theta)$ (p. 55).
Under resale price maintenance with $\bar p=1/2$ and total stock $\theta/2$ , $\pi_r(t)=q(t)\big(\frac{1+\theta}{4\theta}-w\big)$ (p. 56).
Under $(\bar p,\bar w)$ the competitive order is $\theta/2$ and the supplier earns $\Pi^o$ (p. 57).
Under the buy-back $b=1/2$ the retailers' profit is $q\big(\frac34-w-\frac q{2\theta}\big)$ for $1/2<q<\theta/2$ (p. 57).
$1/2>(1+\theta)/(4\theta)$ (p. 57).

Significance

The goal shows that in this model a wholesale price contract always falls short of the integrated profit, whatever $\theta$ . It also shows where the shortfall comes from: at the optimal wholesale price the low-state market price falls below the monopoly price $1/2$ (milestone 4). Restoring the monopoly profit therefore requires a mechanism that holds the low-state price at $1/2$ . Resale price maintenance and a full-refund buy-back both do this, so the section gives a closed-form efficiency argument for vertical restraints that are often treated as anticompetitive. The section also contrasts the buy-back with revenue sharing, which coordinates the single newsvendor (§6.2) but not this model.

The results are proved on the printed pages by elementary algebra. None of them has a machine-checked proof, and nothing on Prove2Me covers this model. The mission produces checked versions of the case analysis, including the $\theta=3$ tie and the two regimes of the competitive order. It also adds a reusable encoding of "perfect competition" as the first zero of aggregate expected profit.

Difficulty

Every statement reduces to one-variable inequalities, but the case structure is easy to get wrong.

The retailers' profit is piecewise (prices hit zero at $q=1$ in the low state and at $q=\theta$ in the high state). The competitive order lies on either side of $q=1$ depending on $w$ .
The supplier's profit $\pi_s$ is piecewise in $w$ , and its second branch peaks at $w=1/4$ only when $\theta>2$ .
The global optimum switches at $\theta=3$ , where both prices are optimal.
A statement "the competitive order is $q_1(w)$ " needs the order to exist, to be unique, and to have positive profit everywhere below it. Exhibiting a root is not enough.
The buy-back profit is identically zero for $q\ge\theta/2$ when $b=w=1/2$ . Only the "first zero" reading of perfect competition pins the order at $\theta/2$ .

Formalization scope

All quantities are real numbers and $\theta>1$ throughout. The continuum of retailers enters only through the total order. No measure space of retailers is formalized, and footnote 26's multiplicity of individual equilibria is not stated. The sales rules under resale price maintenance (proportional allocation) and under the buy-back (price floor $b$ ) are written into the contract definitions, as the page describes them in words. The theorems use only $\bar p=b=1/2$ .

The formulas $q_1$ , $q_2$ , $\pi_s$ and $w^*$ are definitions transcribed from the page. That they are the competitive order and the optimum is the content of the theorems. Defining $\Pi^o$ or the competitive order by its closed form would trivialize the mission, so the competitive order is defined only by the zero-profit property and $\Pi^o$ as a greatest element of the monopolist's feasible profits. The goal is stated over all real wholesale prices, so it also rules out profitable prices outside $[0,1)$ . Uniqueness of $w^*(\theta)$ is not asserted at $\theta=3$ .

The chapter's standing assumptions used here are risk neutrality and full information, together with the model paragraph of pp. 53–54 (two equally likely states, zero salvage value, zero production cost). No platform definition is referenced: no published item formalizes this model.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves, T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, §6.5.2 (3rd draft, January 2003, pp. 53–58). https://doi.org/10.1016/S0927-0507(03)11006-7
R. Deneckere, H. P. Marvel, J. Peck, Demand Uncertainty and Price Maintenance: Markdowns as Destructive Competition, American Economic Review 87(4), 619–641, 1997. https://www.jstor.org/stable/2951366
R. Deneckere, H. P. Marvel, J. Peck, Demand Uncertainty, Inventories, and Resale Price Maintenance, Quarterly Journal of Economics 111(3), 885–913, 1996. https://doi.org/10.2307/2946675

11 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VII: In the Single-Location Base-Stock Model the Transfers t_I = (1 − λ)h_r, t_B = β_r − λβ Make the Retailer's Cost λc(s_r)Textbook

Motivation

A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.

The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).

Setting

Let $D_r$ denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean $\mu_r=\mathbb E[D_r]$ , distribution function $F_r$ , and density $f_r$ . At inventory level $s\in\mathbb R$ , expected inventory is $I_r(s)=\mathbb E[(s-D_r)^+]$ and expected backorders are $B_r(s)=\mathbb E[(D_r-s)^+]$ , where $x^+=\max(x,0)$ . The section assumes $F_r(0)=0$ and a strictly increasing differentiable $F_r$ on nonnegative levels. These assumptions place the optimum above zero.

The retailer pays holding cost $h_r I_r(s)$ and its own backorder cost $\beta_r B_r(s)$ . The supplier pays a further backorder cost $\beta_s B_r(s)$ . All three cost rates are positive. Thus $c_r(s)=h_r I_r(s)+\beta_r B_r(s)$ and $c_s(s)=\beta_s B_r(s)$ are the firms' costs, while $c(s)=c_r(s)+c_s(s)$ is the channel cost. Write $\beta=\beta_r+\beta_s$ . Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.

The proposed contract pays the retailer $t_I I_r(s)+t_B B_r(s)$ from the supplier, where $t_I$ and $t_B$ are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter $\lambda\in(0,1]$ , the contract sets $t_I=(1-\lambda)h_r$ and $t_B=\beta_r-\lambda\beta$ . The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter $\lambda$ describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.

Formalization targets

The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum $s_r^\circ$ is unique and satisfies

F_r(s_r^\circ)=\frac{\beta}{h_r+\beta};

the uncontracted retailer has its own unique optimum $s_r^*$ with $s_r^*<s_r^\circ$ . Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family ( $t_I\ge0$ , with $t_I>0$ exactly for $\lambda<1$ , and $\{t_B:0<\lambda\le1\}=[-\beta_s,\beta_r)$ ); the decomposition

t_I I_r(y)+t_B B_r(y)=(t_I+t_B)I_r(y)+t_B(\mu_r-y);

and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price $p=h_r+\beta_r$ and wholesale price $w=h_r$ , the newsvendor retailer's profit $pS(q)-wq$ , with expected sales $S(q)=\mathbb E[\min(q,D_r)]$ , equals $-c_r(q)+\beta_r\mu_r$ . The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:

c_r^\lambda(s)=\lambda c(s),\qquad c_s^\lambda(s)=(1-\lambda)c(s) \quad\text{for all }s\in\mathbb R\text{ and }0<\lambda\le1.

Consequently, the retailer's contracted cost has the same unique minimizer $s_r^\circ$ as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in $\lambda$ , which is the page's statement that the retailer's share of the cost increases with $\lambda$ . The result does not prescribe one fixed allocation of cost: each $\lambda$ in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.

Significance

The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to $\beta_r$ , while the channel's stock decision uses $\beta_r+\beta_s$ . Under the contract, the retailer bears the fraction $\lambda$ of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.

The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).

Difficulty

The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as $\lambda c$ would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.

Formalization scope

Lean represents $D_r$ by a probability measure on $\mathbb R$ supported on $[0,\infty)$ , with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on $[0,\infty)$ , equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates $h_r,\beta_r,\beta_s$ are fields of one model, and $I_r,B_r$ are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.

Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that $t_I>0$ for all $\lambda\in(0,1]$ fails at $\lambda=1$ , where $t_I=0$ ; the formal statement asserts $t_I\ge0$ with strict positivity exactly for $\lambda<1$ . The contract range is exactly $0<\lambda\le1$ ; $\lambda=0$ would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.

Selected references

Gérard P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; source used here: author's third draft, January 2003, §6.7. DOI.

12 thms3 active usersReviewed

Discrete Geometry Linear Optimization Number Theory+1·Captain: mikedeng1

Integer Programming with a Fixed Number of Variables 1: If B(p,r) ⊂ τK ⊂ B(p,R) with R/r ≤ c₁ and τK Misses the Lattice, Fewer Than 1 + c₁c₂√n Lattice Hyperplanes H + kbₙ Meet B(p,R)Research Paper

Motivation

The integer linear programming feasibility problem asks, for an integer $m\times n$ matrix $A$ and $b\in\mathbb Z^m$ , whether some $x\in\mathbb Z^n$ satisfies $Ax\le b$ . It is NP-complete, so no algorithm polynomial in the length of the data is expected. H. W. Lenstra, Jr. (Math. Oper. Res. 8 (1983) 538–548) showed that the picture changes when the number of variables $n$ is fixed: the problem is then solvable in polynomial time. The proof is a short argument from the geometry of numbers, and it became the starting point of lattice methods in integer programming, including Kannan's improved algorithm and the later flatness-based branching schemes.

Lenstra's introduction (p. 538) describes the idea as transforming the problem into an equivalent one in which "either the existence of a vector $x \in \mathbb Z^n$ satisfying $Ax \le b$ is obvious; or it is known that the last coordinate of any such $x$ belongs to an interval whose length is bounded by a constant only depending on $n$ ." This mission formalizes the geometric statement behind that dichotomy, §1 of the paper.

Timeline. For $n = 2$ , Hirschberg and Wong and Kannan gave polynomial algorithms in special cases, and Scarf treated the case $n=2$ completely; the case of general fixed $n$ was conjectured by Hirschberg–Wong and Scarf (as recounted on p. 538). Lenstra's paper (received 1981, published 1983) settled the conjecture. Its lattice reduction step uses the algorithm of Lenstra, Lenstra and Lovász (1982). Kannan (1987) later reduced the dependence on $n$ to $n^{O(n)}$ .

Setting

Work in $\mathbb R^n$ with the Euclidean length $|\cdot|$ , and write $B(p,z)=\{x\in\mathbb R^n : |x-p|\le z\}$ for the closed ball with centre $p$ and radius $z>0$ .

A lattice is $L=\sum_{i=1}^n \mathbb Z b_i$ for a basis $b_1,\dots,b_n$ of $\mathbb R^n$ . Its determinant $d(L)=|\det(b_1,\dots,b_n)|$ (the $b_i$ as columns) is the volume of the parallelepiped $\sum_i[0,1)\,b_i$ and does not depend on the basis. Hadamard's inequality (6) says $d(L)\le\prod_i|b_i|$ . A basis is reduced in Lenstra's sense if, for a constant $c_2$ depending only on $n$ ,

\prod_{i=1}^n |b_i| \le c_2\cdot d(L). \tag{7}

Singling out $b_n$ , let $H=\sum_{i=1}^{n-1}\mathbb R b_i$ be the hyperplane spanned by the other vectors, $L'=\sum_{i=1}^{n-1}\mathbb Z b_i$ the lattice inside it, and $h$ the distance of $b_n$ to $H$ . Then $L\subset\bigcup_{k\in\mathbb Z}(H+kb_n)$ : the lattice lies on a family of parallel hyperplanes $H + kb_n$ at successive distance $h$ .

In the paper, $K=\{x : Ax\le b\}$ is bounded with positive volume, and a linear map $\tau$ makes it "round":

B(p,r)\subset\tau K\subset B(p,R)\quad(3),\qquad R/r\le c_1\quad(4),

with $c_1$ depending only on $n$ . Then $K\cap\mathbb Z^n=\emptyset$ if and only if $\tau K\cap L=\emptyset$ for $L=\tau\mathbb Z^n$ , a lattice with basis $b_i=\tau(e_i)$ .

Formalization targets

Goal (§1, p. 541)

Let $b_1,\dots,b_n$ be a basis with (7), numbered so that $|b_n|=\max_i|b_i|$ , and let $\tau K$ satisfy (3) and (4). Then

\tau K\cap L\neq\emptyset\quad\text{or}\quad t-1<c_1c_2\sqrt n,

where $t$ is the number of hyperplanes $H+kb_n$ , $k\in\mathbb Z$ , that meet $B(p,R)$ (finiteness included).

Milestones, in the order the paper uses them

LEMMA (8), p. 540: every $x$ has $y\in L$ with $|x-y|^2\le\frac14(|b_1|^2+\cdots+|b_n|^2)$ .
(10), p. 540: if $|b_n|$ is maximal, $|x-y|\le\frac12\sqrt n\,|b_n|$ .
(11), p. 540: $d(L)=h\cdot d(L')$ .
(12), pp. 540–541: under (7), $c_2^{-1}|b_n|\le h\le|b_n|$ .
p. 541: if $B(p,r)\subset\tau K$ and $\tau K\cap L=\emptyset$ , then $r<\frac12\sqrt n\,|b_n|$ .
p. 541: if precisely $t$ hyperplanes $H+kb_n$ meet $B(p,R)$ , then $t-1\le 2R/h$ .

The goal leaves $c_1$ and $c_2$ free, so it remains valid for any reduction algorithm and any rounding procedure; the companion mission (Integer Programming with a Fixed Number of Variables 2) supplies $c_1 = 2n^{3/2}$ , and the LLL algorithm supplies $c_2=2^{n(n-1)/4}$ .

Significance

The result. The goal is the branching step of Lenstra's algorithm. It says that a lattice-point-free convex body that is well rounded is "flat" in the lattice direction dual to $H$ : only boundedly many lattice hyperplanes meet it. The search for a lattice point in dimension $n$ therefore reduces to fewer than $1+c_1c_2\sqrt n$ searches in dimension $n-1$ , which with $n$ fixed gives polynomial running time. Sharper forms of the same dichotomy, such as Kannan's bounds, are the basis of later lattice-based integer programming algorithms.

Formalizing it. The results are classical and proved on paper; to our knowledge none of the statements of §1 is machine-checked. Hadamard's inequality (6) is in Mathlib (Orientation.abs_volumeForm_apply_le). The published platform theorem KannanLattice.Core.exists_lattice_point_near_projection (Kannan 1987, Proposition 4.2) proves a stronger form of (8) and (10), with Gram–Schmidt lengths in place of $|b_i|$ ; for $L=\mathbb Z^n$ , (10) is the published QFS.exists_lattice_mem_closedBall. What remains is the "base times height" identity (11) relating a full-rank determinant to the distance of a vector from a hyperplane, the spacing bound (12), the count of hyperplanes meeting a ball, and their assembly. This is one of the two geometric ingredients of Lenstra's polynomial algorithm; the algorithm itself and its running time are not formalized.

Difficulty

The argument is short on paper, and each step is "clear" there. The work lies in connecting three descriptions of the same geometry that Mathlib keeps apart: the determinant of a coordinate matrix ( $d(L)$ ), the metric distance of a point to a subspace ( $h$ ), and the $(n-1)$ -dimensional volume of $L'$ . Identity (11) needs exactly this bridge, and (12) needs Hadamard's inequality for the lower-dimensional lattice $L'$ inside a hyperplane of $\mathbb R^n$ , not for a full-rank matrix. Bounding the number of hyperplanes meeting a ball needs the normal direction of $H$ and the fact that the hyperplanes are $h$ apart along it. A tempting shortcut is to define $h$ as the length of the last Gram–Schmidt vector and $d(L)$ as the product of Gram–Schmidt lengths: that turns (11) into a tautology and is ruled out below.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so norms are Euclidean and balls round; $B(p,z)$ is Metric.closedBall p z with $z>0$ as a hypothesis where the paper writes a ball.
Where $b_n$ is singled out, $n=k+1$ , the basis is b : Fin (k+1) → ℝⁿ, $b_n$ = b (Fin.last k) and $b_1,\dots,b_{n-1}$ = b ∘ Fin.castSucc. "Basis for $L$ " is linear independence of the $n$ vectors over $\mathbb R$ , and $L$ is the published KannanLattice.Core.lattice b, the $\mathbb Z$ -span.
$d(L)$ is the paper's definition, $|\det|$ of the column matrix (latDet). $h$ is Metric.infDist from $b_n$ to the span $H$ . $d(L')$ , for which the paper writes no formula, is the published KannanLattice.Core.latticeDet (the product of Gram–Schmidt lengths of $b_1,\dots,b_{n-1}$ , the $(n-1)$ -volume of their parallelepiped).
The hyperplanes $H+kb_n$ meeting $B(p,R)$ are indexed by the set of integers hitIndices b p R; $t$ is its cardinality, its finiteness is part of every conclusion (the cardinality of an infinite set is $0$ in Lean), and $t-1$ is computed in $\mathbb R$ .
The constants "only depending on $n$ ", $c_1$ and $c_2$ , are arbitrary real numbers. The reducedness (7) is a hypothesis, and so is the maximality $|b_i|\le|b_n|$ , which enters (10), the radius bound and the goal only.
$\tau K$ is an arbitrary set $X\subseteq\mathbb R^n$ satisfying (3); §1 never uses that $K$ is a polyhedron or the map $\tau$ , and every lattice is $\tau\mathbb Z^n$ for $\tau(e_i)=b_i$ . The paper's "for some $p\in\tau K$ " follows from (3).
The identity (11) is stated without (7), which the paper assumes in the surrounding sentence but does not use.
Ruled out: defining $d(L)$ or $h$ through Gram–Schmidt lengths (which makes (11) bookkeeping), dropping finiteness of the hyperplane count, and replacing the dichotomy "some lattice point lies in $\tau K$ " by a statement about one computed lattice point.

Welcome contributions: the bridge between Matrix.det of a basis and products of Gram–Schmidt lengths (reusable for any lattice development), Hadamard's inequality for a family of fewer than $n$ vectors, and the count of lattice hyperplanes meeting a ball.

Selected references

H. W. Lenstra, Jr., Integer Programming with a Fixed Number of Variables, Mathematics of Operations Research 8(4) (1983) 538–548. https://doi.org/10.1287/moor.8.4.538
A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
R. Kannan, Minkowski's convex body theorem and integer programming, Mathematics of Operations Research 12(3) (1987) 415–440. https://doi.org/10.1287/moor.12.3.415

10 thms2 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Motivation

Minimizing total weighted tardiness on a single machine, written $n|1||\sum w_jT_j$ , is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference problem for branch-and-bound methods and dominance rules throughout the 1960s and 1970s.

Close relatives are easy: with equal weights and a common due date, shortest-processing-time order is optimal. Whether the weighted problem admits a polynomial algorithm was open until the report of Brucker, Lenstra and Rinnooy Kan in 1975. Their Theorem 4(d) shows that KNAPSACK reduces to it, so the problem is NP-hard. The unweighted case $n|1||\sum T_j$ is listed there as open (Section 5) and was settled only later by Du and Leung (1990).

Timeline:

1972: Karp proves KNAPSACK NP-complete (Karp 1972).
1975: Brucker, Lenstra and Rinnooy Kan, Mathematisch Centrum Report BW 43/75, Theorem 4(d), reduce KNAPSACK to $n|1||\sum w_jT_j$ (journal version: Annals of Discrete Mathematics 1, 1977).
1977: Lawler gives a pseudopolynomial algorithm for $n|1||\sum T_j$ and shows that $n|1||\sum w_jT_j$ is strongly NP-hard (Lawler 1977).
1990: Du and Leung prove $n|1||\sum T_j$ NP-hard (Du & Leung 1990).

Setting

A KNAPSACK instance consists of positive integers $a_1,\dots,a_t$ and $b$ . It is a yes-instance if some subset $S\subseteq T=\{1,\dots,t\}$ satisfies $\sum_{j\in S}a_j=b$ . Write $A=\sum_{j\in T}a_j$ and $a_*=\max_{j\in T}a_j$ .

An instance of $n|1||\sum w_jT_j$ consists of $n$ jobs. Job $j$ has a processing time $p_j$ , a weight $w_j$ and a due date $d_j$ , all nonnegative integers, and every job is available at time $0$ . A schedule gives each job a start time $B_j\in\mathbb N$ , and no two jobs may overlap on the machine. Job $j$ completes at $C_j=B_j+p_j$ and has tardiness $T_j=\max\{0,C_j-d_j\}$ . The instance with threshold $y$ is a yes-instance if some schedule satisfies $\sum_jw_jT_j\le y$ . A processing order $\pi=(\pi(1),\dots,\pi(n))$ determines the schedule without idle time, in which $C_{\pi(k)}=\sum_{i\le k}p_{\pi(i)}$ .

Reducibility (Section 2 of the paper) is polynomial-time many-one reducibility between the recognition versions. A polynomial-time Turing machine must map codes of KNAPSACK instances to codes of scheduling instances so that yes-instances map exactly to yes-instances.

The paper's construction has $n=t+t'$ jobs: for $j\in T$ , $p_j=\tau+a_j$ , $w_j=\tau+a_j+1$ , $d_j=t\tau+b$ ; for each of the $t'$ dummy jobs, $p_j=\tau$ , $w_j=\tau+1$ , $d_j=t\tau+b$ . The threshold is $y=\tfrac12t'(t'+1)\tau(\tau+1)+(t'+1)\tau(A-b)+t'$ , with $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ and $\tau>2t'+A$ . The proof is phrased in terms of $c_\pi=C_{\pi(t)}-(t\tau+b)$ , the amount by which the $t$ -th job of the order misses the common due date.

Formalization targets

Goal: Theorem 4(d)

\text{KNAPSACK}\;\propto\;n|1||\textstyle\sum w_jT_j,

stated as CookPvsNP.PolyReducible SchedComplexity.OneMachine.knapsackLang wtLangMult. The scheduling side uses the multiplicity encoding of the paper's Remark (p. 23), in which a class of identical jobs is written once together with its cardinality.

The equivalence and its claims

Each milestone is a statement of the paper's proof (pp. 20–21) about the construction above, for every admissible $\tau$ :

removal of idle time: every schedule is matched or improved by the schedule without idle time of some processing order;
KNAPSACK has a solution iff some order has $C_{\pi(t)}=t\tau+b$ ; moreover $-b\le c_\pi\le A-b$ ;
identities and bounds (2)–(7) for the tail sums $\sum_{j>t}v_{\pi(j)}(C_{\pi(j)}-C_{\pi(t)})$ ;
claims (A) $c_\pi=0\Rightarrow\exists\pi'$ with $c_{\pi'}=0$ and $\sum w_jT_j\le y$ ; (B) $c_\pi>0\Rightarrow\sum w_jT_j>y$ ; (C) $c_\pi<0\Rightarrow\sum w_jT_j>y$ ;
the equivalence: KNAPSACK has a solution iff the constructed instance has a schedule with $\sum w_jT_j\le y$ .

Significance

The theorem places $n|1||\sum w_jT_j$ among the NP-hard problems, so (unless P = NP) the research on it has to aim at enumerative methods, pseudopolynomial algorithms or approximation, not at an exact polynomial algorithm. Together with the companion reductions of Theorem 4, it drew the boundary between easy and hard single-machine problems that the later classification of Lageweg, Lawler, Lenstra and Rinnooy Kan made systematic.

The result is proved in the paper, and Lawler's later strong NP-hardness proof supersedes it. No machine-checked proof is known to exist. A formal proof adds three things. It makes the paper's "it is easily seen" steps and the encoding argument of the Remark explicit. It produces a reusable single-machine tardiness model with processing orders. It also fixes a gap in the printed construction: the printed $t'$ need not be an integer.

Difficulty

The equivalence is not a local exchange argument. The threshold $y$ must separate orders with $c_\pi=0$ from all others, and the objective is a quadratic function of the order. The orders with $c_\pi=0$ can still differ in $\sum w_jT_j$ by the cross terms $\sum a_{\pi(j)}a_{\pi(k)}$ and by how the late jobs are arranged. The construction therefore needs a slack $t'$ that absorbs these terms, and a scale $\tau$ large enough that a nonzero $c_\pi$ always costs more than the slack. Keeping exact track of every constant, including $t'$ and $y$ , is where errors creep in.

Polynomiality is a second, separate difficulty. The construction has $\Theta(t^2a_*^2+tA)$ jobs, which is exponential in the binary length of the KNAPSACK input. The goal holds only for the encoding of the Remark, and a solver must also produce an explicit polynomial-time Turing machine.

Formalization scope

Jobs of the order-based statements are Fin n, numbered from $0$ ; a processing order is Equiv.Perm (Fin n) with π i the paper's $\pi(i+1)$ . posCompletion p π k is the paper's $C_{\pi(k)}$ for the 1-based position $k$ .
Start times are in $\mathbb N$ . Every criterion is regular and the paper determines schedules by processing orders, so integer start times lose nothing. Tardiness and $\sum w_jT_j$ are computed in $\mathbb Z$ ; the bounds with halves are stated over $\mathbb R$ exactly as printed.
Corrected gap: the printed $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ is a half-integer when $(t+1)(A-b)$ is odd. The formalization uses its ceiling and computes $y$ from the same $t'$ .
$\tau$ is quantified over all integers with $\tau>2t'+A$ ; the positivity of the $a_j$ and $0<b<A$ are hypotheses, as the paper assumes them.
Explicit readings of the paper's loose phrases: "we may assume [no idle time]" becomes a theorem that the schedule without idle time of some order is at least as good as any schedule; "easily seen" becomes the equivalence with $C_{\pi(t)}=t\tau+b$ ; "for some $\pi$ " in (5) and (7) becomes a reordering that keeps the first $t$ positions, and so keeps $c_\pi$ ; "we may assume $0<b<A$ " is a hypothesis of the milestones but not of the goal, whose reduction must handle every KNAPSACK instance.
Reducibility is CookPvsNP.PolyReducible from the published CookPvsNP_defs. Codes use the alphabet BSym and the binary numerals encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). KNAPSACK is restricted to positive integers, so that encoding's subsetSumLang is not reused.
The goal must not be weakened to the bare equivalence: polynomial-time computability of the reduction is part of the statement. The one-copy-per-job encoding of the target is ruled out: the paper does not claim polynomiality for it, and the goal uses the multiplicity encoding instead.
Welcome contributions: proofs of the claims, a reusable lemma that idle time can be removed for regular criteria, and Turing-machine constructions for arithmetic on binary numerals, which the sibling missions of this series also need.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://ir.cwi.nl/pub/9725 , https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
E. L. Lawler, A "pseudopolynomial" algorithm for sequencing jobs to minimize total tardiness, Annals of Discrete Mathematics 1 (1977) 331–342. https://doi.org/10.1016/S0167-5060(08)70742-8
J. Du, J. Y.-T. Leung, Minimizing total tardiness on one machine is NP-hard, Mathematics of Operations Research 15 (1990) 483–495. https://doi.org/10.1287/moor.15.3.483
S. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

18 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VI: With a Forecast Update, Buy-Back Terms with w₁ − w₂ + λc₂ = λc₁ Give the Retailer λΩ₁(q₁) and a Lower Period-2 Margin w₂ − c₂ < w₁ − c₁Textbook

Motivation

A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.

This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.

Setting

A demand signal $\xi \ge 0$ with density $g$ and distribution function $G$ is observed once before the selling season. Given $\xi$ , demand $D$ has distribution function $F(\cdot\,|\,\xi)$ , continuous and strictly increasing on $[0,\infty)$ . Demand is stochastically increasing in the signal: $F(x\,|\,\xi_h) < F(x\,|\,\xi_l)$ for $\xi_h > \xi_l$ . Expected sales are $S(q\,|\,\xi) = E[\min(q,D)\,|\,\xi]$ . Period 1 is before the signal and period 2 is after it. The retailer's total order is $q_1$ after period 1 and $q_2 \ge q_1$ after period 2. The supplier's unit production cost is $c_i$ in period $i$ , with $c_1 < c_2 < p$ , where $p$ is the retail price. Salvage values and goodwill costs are zero.

The supply chain's period-2 objective is

\Omega_2(q_2\,|\,q_1,\xi) = pS(q_2\,|\,\xi) - c_2 q_2 + c_2 q_1 ,

and $q_2(q_1,\xi)$ maximizes it over $q_2 \ge q_1$ . The supply chain's expected profit is $\Omega_1(q_1) = -c_1 q_1 + E[\Omega_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ .

Under the buy back contract $\{w_1, w_2, b\}$ the retailer pays $w_i$ per unit ordered in period $i$ , and the supplier refunds $b$ per unsold unit. The retailer's period-2 profit is $\pi_2(q_2\,|\,q_1,\xi) = (p-b)S(q_2\,|\,\xi) - (w_2-b)q_2 + w_2 q_1$ , and his period-1 profit is $\pi_1(q_1) = -w_1 q_1 + E[\pi_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ . The supplier's period-2 profit $\Pi_2$ and her period-1 profit $\Pi_1(x\,|\,q_1)$ , as functions of the stock $x$ she holds, are given in the mission's Profits definition.

Formalization targets

Goal: the buy back contract coordinates

For $\lambda \in [0,1]$ with

p - b = \lambda p,\qquad w_2 - b = \lambda c_2,\qquad w_1 - w_2 + \lambda c_2 = \lambda c_1,

the identities

\pi_2(q_2\,|\,q_1,\xi) = \lambda\big(\Omega_2(q_2\,|\,q_1,\xi) - c_2 q_1\big) + w_2 q_1,\qquad \pi_1(q_1) = \lambda\,\Omega_1(q_1)

hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for $\lambda > 0$ ). In addition,

w_2 - c_2 = w_1 - \big(\lambda c_1 + (1-\lambda)c_2\big) < w_1 - c_1 \quad (\lambda < 1).

Milestones

The structure of the period-2 problem, Eqs. (25)–(26): $q_2(\xi)$ solves $F(q_2(\xi)\,|\,\xi) = (p-c_2)/p$ and increases in $\xi$ , and the threshold $\xi(q_1)$ splits the signals into those that trigger a period-2 order and those that do not.
The retailer's period-2 identity (p. 65).
The supplier fills any period-2 order up to $q_2(q_1,\xi)$ , and for $\lambda < 1$ she does not fill a larger one (p. 65).
The retailer's period-1 identity (p. 66).
The first-order condition (27) for $q_1^o$ .
The supplier's period-2 profit increases in her stock below $q_1$ , so she produces at least the period-1 order (p. 66).
The supplier produces exactly the period-1 order (p. 67).
The margin comparison (p. 67).

Significance

The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through $\lambda$ . Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.

These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold $\xi(x)$ .

Difficulty

The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and $\partial \Pi_1(x\,|\,q_1)/\partial x = -c_1 + c_2(1 - G(\xi(x)))$ . The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum $\max(q_1, q_2(\xi))$ has a kink at $\xi = \xi(q_1)$ . The integrand switches between two regimes, and the switch point moves with $q_1$ . The supplier's period-1 profit is not differentiable at $x = q_1$ ; only its right derivative is negative at $q_1^o$ . Turning the page's derivative statements into the global claim that $x = q_1^o$ is her unique optimum needs a monotonicity argument on both sides of $q_1^o$ .

Formalization scope

The conditional law is a measurable family $\xi \mapsto D_\xi$ of probability measures on $\mathbb R$ supported on $[0,\infty)$ , each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on $[0,\infty)$ . The signal has a measurable density $g \ge 0$ with $\int_0^\infty g = 1$ , and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. $0 < c_2 < p$ makes the critical ratio lie in $(0,1)$ . Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).

The optimum $q_2(q_1,\xi)$ is a hypothesis-carried selection maximizing $\Omega_2$ over $q_2 \ge q_1$ . It is never an arbitrary function: a formalization that let $q_2(q_1,\xi)$ be unconstrained would make $\pi_1 = \lambda\Omega_1$ a statement about meaningless orders. The thresholds $\xi(q_1)$ enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over $q_1 \ge 0$ and $q_2 \ge q_1$ . Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).

Three corrections of the print are disclosed in the item notes:

the strict margin inequality fails at $\lambda = 1$ ;
the p. 66 identity for $\Pi_2(x, q_1, q_2, \xi)$ is off by the constant $(1-\lambda)c_2q_1$ ;
"retailer optimal equals chain optimal" needs $\lambda > 0$ in the converse direction.

Contributions are welcome on all milestones. A lemma that differentiates $q \mapsto E[\max_{q_2 \ge q} \Omega_2]$ with a density-driven threshold would be reusable beyond this mission.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. https://doi.org/10.1016/S0927-0507(03)11006-7
K. L. Donohue, Efficient Supply Contracts for Fashion Goods with Forecast Updating and Two Production Modes, Management Science 46(11), 1397–1411, 2000. https://doi.org/10.1287/mnsc.46.11.1397.12088
M. Fisher and A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 87–99, 1996. https://doi.org/10.1287/opre.44.1.87

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VIII: In the Two-Location Base-Stock Model the Linear Transfers (39)–(41) Make the Optimal Base Stocks the Unique Nash EquilibriumTextbook

Motivation

In a supply chain with stock at two locations, a supplier holds inventory that replenishes a retailer, and the retailer serves customers. Each firm sets its own inventory level to minimize its own cost. The retailer bears only part of the cost of customer backorders, and the supplier bears none of the retailer's holding cost, so their incentives differ. The resulting equilibrium generally differs from the policy that minimizes total cost. Cachon and Zipkin (Management Science 45(7), 1999) studied this game and proposed linear transfer payments that align the firms' incentives. In the chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003, doi:10.1016/S0927-0507(03)11006-7), Cachon re-derives that analysis, adds a parameter $\lambda$ that divides the retail-level costs between the firms, and answers two questions the original paper left open: whether the contracts allow an arbitrary division of cost, and whether the optimal policy is the unique equilibrium under the contracts. This mission formalizes the second answer, together with the analysis of the decentralized game and of the optimal policy that it rests on (§6.8 of the 2003 chapter, read in the author's January 2003 draft).

Setting

Two firms, a retailer $r$ and a supplier $s$ , each use a base stock policy: firm $i$ keeps its inventory position equal to its base stock level $s_i \in \mathbb R$ . A negative supplier base stock means planned backorders. Let $D_r$ and $D_s$ be the demands during the retailer's and the supplier's lead times. They are nonnegative with finite means $\mu_r$ , $\mu_s$ , and their distribution functions $F_r$ , $F_s$ are continuous, zero at $0$ , strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$ . Holding costs are $h_r$ and $h_s$ , with $0 < h_s < h_r$ . Each backorder at the retailer costs the retailer $\beta_r > 0$ and the supplier $\beta_s > 0$ per unit time. Write $\beta = \beta_r + \beta_s$ .

At retailer inventory level $y$ the expected on-hand stock is $I_r(y) = E[(y-D_r)^+]$ and the expected backorders are $B_r(y) = E[(D_r-y)^+]$ . The retail-level cost rates are $c_r(y) = h_rI_r(y) + \beta_rB_r(y)$ , $c_s(y) = \beta_sB_r(y)$ and $c(y) = c_r(y) + c_s(y)$ . Because the supplier may stock out, the retailer's actual inventory level is $s_r - (D_s - s_s)^+$ , and every retail-level quantity is averaged accordingly:

g(s_r,s_s) = E\big[g(s_r - (D_s-s_s)^+)\big] = F_s(s_s)g(s_r) + \int_{s_s}^\infty g(s_r+s_s-x)f_s(x)\,dx .

With the supplier's inventory $I_s(y) = E[(y-D_s)^+]$ and backorders $B_s(y) = \mu_s - y + I_s(y)$ , the firms' costs and the chain's cost are

\pi_r(s_r,s_s) = c_r(s_r,s_s), \qquad \pi_s(s_r,s_s) = h_sI_s(s_s) + c_s(s_r,s_s), \qquad \Pi = \pi_r + \pi_s .

A pair $\{s_r^o, s_s^o\}$ minimizing $\Pi$ is an optimal policy. A Nash equilibrium is a pair from which neither firm can lower its own cost by a unilateral change of its base stock.

Under a linear transfer the supplier pays the retailer $t_II_r(s_r,s_s) + t_B^rB_r(s_r,s_s) + t_B^sB_s(s_s)$ (a negative amount is a payment the other way). The Cachon–Zipkin contracts with parameter $\lambda \in (0,1]$ are

t_I = (1-\lambda)h_r, \qquad t_B^r = \beta_r - \lambda\beta, \qquad t_B^s = \lambda h_s\frac{F_s(s_s^o)}{1-F_s(s_s^o)} .

Formalization targets

Goal: the contracts coordinate, uniquely

If $\{s_r^o, s_s^o\}$ is optimal with $s_s^o > 0$ and $\lambda \in (0,1]$ , then under the contracts

\pi_r = \lambda c(s_r,s_s) - t_B^sB_s(s_s), \qquad \pi_s = (h_s+t_B^s)I_s(s_s) + (1-\lambda)c(s_r,s_s) + t_B^s(\mu_s - s_s),

$\{s_r^o, s_s^o\}$ is a Nash equilibrium, and it is the only one. The goal contains no numerical constants. It holds for every demand distribution in the class and every $\lambda$ in the range.

Milestones

In the uncontracted game, every retailer best response exceeds $\hat s_r > 0$ , where $F_r(\hat s_r) = \beta_r/(h_r+\beta_r)$ , and every supplier best response is positive (pp. 79–80).
In the uncontracted game, for every $s_s$ the retailer's optimal base stock is below the chain's; consequently the competition penalty $(\Pi(s^*) - \Pi(s^o))/\Pi(s^o)$ is positive at every equilibrium $s^*$ (pp. 80–81).
The partial derivatives (35)–(36) of $\Pi$ , and every optimum with $s_s > 0$ satisfies $c'(s_r) = h_s$ , i.e. $F_r(s_r) = (h_s+\beta)/(h_r+\beta)$ (37) (p. 83).
Optima with $s_s \le 0$ have $s_r + s_s = \bar s$ , where $\Pr(D_r + D_s \le \bar s) = \beta/(h_r+\beta)$ (38) (p. 83).
The cost identities (42)–(43) under the contracts (p. 84).
Under the contracts the retailer's best response decreases in $s_s$ , and the supplier's marginal cost along it has the closed form printed on p. 84.

Significance

The goal says that a contract built from quantities both firms can measure, namely the retailer's inventory and backorders and the supplier's backorders, makes the system-optimal policy the only equilibrium. The firms therefore reach the optimum without coordinating on an equilibrium. The parameter $\lambda$ splits the retail-level costs between the firms in any proportion up to $\lambda = 1$ . Milestone 2 shows the contract is needed: without transfers, decentralization is always strictly suboptimal when the supplier is charged for retail backorders. The transfers $t_I$ and $t_B^r$ are those of the single-location model (§6.7), even though the retailer's target fractile changes from $\beta/(\beta+h_r)$ to $(\beta+h_s)/(\beta+h_r)$ .

The results are proved in the source and in Cachon and Zipkin (1999), with informal derivative arguments. No machine-checked version is known. Formalizing them requires differentiating expectations of piecewise-linear convex functions of a random lead-time shortfall. The page's argument also assumes densities, which the formal statements avoid, and contains several printing slips (see below). These would be settled by a complete development.

Difficulty

The firms' costs are compositions: a convex single-location cost evaluated at the random level $s_r - (D_s - s_s)^+$ , which is concave in $s_s$ . The supplier's cost is therefore not obviously convex in $s_s$ ; its convexity at $s_r = s_r^o$ depends on the value of $t_B^s$ and on $c'(s_r^o) = h_s$ . Uniqueness is the hard part. Under the contracts the retailer's best response $s_r(s_s)$ decreases, but the supplier's marginal cost along that best response, $F_s(s_s)(h_s - (1-\lambda)c'(s_r(s_s)) + t_B^s) - t_B^s$ , is not monotone in general when $\lambda$ is small, contrary to a literal reading of p. 84. A uniqueness argument has to show that it has at most one zero, not that it increases.

Formalization scope

Demand laws are probability measures on $\mathbb R$ with no mass below $0$ , finite means, and continuous distribution functions, zero at $0$ , strictly increasing on $[0,\infty)$ and differentiable on $(0,\infty)$ . These are the section's standing assumptions, together with $0 < h_s < h_r$ and $\beta_r, \beta_s > 0$ (footnote 34 excludes the zero cases). Expectations are Lebesgue integrals: $I_r$ , $B_r$ , $I_s$ and the two-location averages are defined by expectation, and the page's integral forms are consequences. Integrals against $f_s(x)\,dx$ are written against the law of $D_s$ , so no density hypothesis is made. Base stocks range over all of $\mathbb R$ , and "optimal" means minimizing $\Pi$ over $\mathbb R^2$ ; the existence of an optimum is a hypothesis, as on p. 77. Derivatives are stated with HasDerivAt. Independence of $D_r$ and $D_s$ , implicit on the page, enters only through the convolution of their laws in (38).

The contracted costs are defined from the firms' original costs and the transfer payment. Defining them by the closed forms (42)–(43) would make the identities trivial and is ruled out.

Corrected slips: (42) is stated with $\lambda c(s_r,s_s)$ where the page prints $\lambda\Pi(s_r,s_s)$ (the difference $\lambda h_sI_s(s_s)$ does not depend on $s_r$ ). The retailer's single-location fractile on p. 79 is stated as $\beta_r/(h_r+\beta_r)$ , not the printed $\beta/(h_r+\beta)$ . The garbled display after (43) and the $f_s$ / $F_s$ slip in the best-response derivative are not reproduced. Not included: the contraction condition (34), the case split for the optimal policy (p. 84), the case $s_s^o \le 0$ , and the alternative schemes of §6.8.5 (Lee–Whang, Chen). Contributions of those, or of a reusable library for derivatives of $E[g(s - (D-t)^+)]$ , are welcome. The platform's Clark–Scarf items (InventoryControl_clarkScarf, ClarkScarf.Serial.*) concern periodic-review echelon policies and are not reused.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003, §6.8. https://doi.org/10.1016/S0927-0507(03)11006-7
G. P. Cachon and P. H. Zipkin, Competitive and cooperative inventory policies in a two-stage supply chain, Management Science 45(7), 936–953, 1999. https://doi.org/10.1287/mnsc.45.7.936
F. Chen and Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426
A. Federgruen and P. Zipkin, Computational issues in an infinite-horizon, multiechelon inventory model, Operations Research 32(4), 818–836, 1984. https://doi.org/10.1287/opre.32.4.818

10 thms2 active usersReviewed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Wait-and-Judge Scenario Optimization 1: For Convex Programs, Seeing s_N Support Constraints Gives P^N{V(x_N) > ε(s_N)} ≤ γ, the Value of the Variational Problem (10)Research Paper

Motivation

Many decision problems in control, finance and engineering must hold against an uncertain parameter $\delta$ whose distribution is unknown, while samples of $\delta$ (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the $N$ observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen $\delta$ violate it?

The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on $N$ and the dimension $d$ , and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than $d$ samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.

Timeline:

2005–2006, Calafiore and Campi: a convex scenario program in $\mathbb R^d$ has at most $d$ support constraints; first sample-size bounds.
2008, Campi and Garatti: the exact bound $\mathbb P^N\{V(x^*_N)>\epsilon\}\le\sum_{i=0}^{d-1}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ , with equality for fully-supported problems.
2018, Campi and Garatti: the wait-and-judge bound, Theorem 1 below, with the 2008 bound as a corollary.

Setting

The decision variable is $x\in\mathbb R^d$ . A problem consists of a cost vector $c\in\mathbb R^d$ , a convex domain $\mathcal X\subseteq\mathbb R^d$ , convex constraint sets $\mathcal X_\delta\subseteq\mathbb R^d$ indexed by $\delta$ in a probability space $(\Delta,\mathcal F,\mathbb P)$ , and convex tie-break functions $t_1,\dots,t_p$ . Given an i.i.d. sample $\delta^{(1)},\dots,\delta^{(N)}$ with $N>d$ , the scenario program is

\min_{x\in\mathcal X}\ c^{\mathsf T}x\quad\text{subject to}\quad x\in\bigcap_{i=1}^N\mathcal X_{\delta^{(i)}}.

Ties are broken by minimising $t_1$ among the minimisers, then $t_2$ , and so on; the resulting solution is $x^*_N$ .

The violation of a point is $V(x)=\mathbb P\{\delta\in\Delta: x\notin\mathcal X_\delta\}$ .
A constraint is a support constraint if removing it changes the solution; $s^*_N$ is their number.
Assumption 1: for every $m$ and every sample of size $m$ , the program with those $m$ constraints has a unique tie-broken solution.
Assumption 2 (non-degeneracy): for every $m$ , with probability one, keeping only the support constraints does not change the solution.

The variational problem (10) is: for a function $\epsilon:\{0,\dots,d\}\to[0,1]$ ,

\gamma^*=\inf_{\xi\in C^d[0,1]}\xi(1)\quad\text{s.t.}\quad\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}\xi(t)\ge\binom Nk t^{N-k}\,\mathbf 1_{[0,1-\epsilon(k))}(t),\ \ t\in[0,1],\ k=0,\dots,d.

Formalization targets

Goal: Theorem 1 (p. 10)

For every $[0,1]$ -valued $\epsilon(k)$ , under Assumptions 1 and 2,

\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}\ \le\ \gamma^*.

The level $\epsilon$ is evaluated at the observed number of support constraints. The goal fixes no particular $\epsilon$ , which keeps it stable under any later choice of levels.

Milestones (the proof of Theorem 1, Sect. 5.1)

$s^*_m\le d$ for every sample (quoted from [7]).
(14): $\mathbb P^N\{V(x^*_N)>\epsilon(k)\wedge s^*_N=k\}=\binom Nk\,\mathbb P^N\{A\}$ , where $A$ adds "the first $k$ constraints are of support".
$A=B$ up to a null set, where $B$ concerns the program on the first $k$ samples.
(16): $\mathbb P^N\{A\}=\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$ , with $F_k(v)=\mathbb P^k\{V(x^*_k)\le v\wedge s^*_k=k\}$ .
(17): $\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}=\sum_{k=0}^d\binom Nk\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$ .
(18): $\sum_{k=0}^{\min\{m,d\}}\binom mk\int_{[0,1]}(1-v)^{m-k}\,\mathrm dF_k(v)=1$ for every $m$ .
Weak duality between the truncated moment problem (20) and its dual (21), giving (22).
(23): $\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}t^m=\binom mk t^{m-k}$ for $m\ge k$ , and $0$ otherwise.
(24): the infimum of $p(1)$ over polynomials feasible for (10) equals $\gamma^*$ .

Companions

Theorem 2 (p. 11): for $\beta\in(0,1)$ and $\epsilon(k)=1-t(k)$ , with $t(k)$ the unique root in $(0,1)$ of $\frac{\beta}{N+1}\sum_{m=k}^N\binom mk t^{m-k}-\binom Nk t^{N-k}=0$ , the probability is at most $\beta$ .
The root lemma of Sect. 5.3, including its sign and divergence claims.
$\gamma^*\le\sum_{i<d}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ for constant $\epsilon$ (Sect. 5.2).
Corollary 1, the 2008 bound.

Significance

Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of $\epsilon(k)$ , a user who finds $k\ll d$ support constraints obtains a level $\epsilon(k)$ comparable to that of a $k$ -dimensional problem, which is far below the a-priori level for dimension $d$ . The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.

The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:

a formal account of scenario programs with lexicographic tie-break and of support constraints in the "changes the solution" sense;
the exchangeability argument (14) on product measures;
the representation (17) of a tail probability through generalized distribution functions;
a weak-duality argument for a generalized moment problem. The 2008 bound itself is posed on the platform as an open problem under other hypotheses; Corollary 1 states it under this paper's assumptions.

Difficulty

The obvious approach bounds the probability for each value of $s^*_N$ separately by a binomial tail, then sums. This fails: the event $s^*_N=k$ is not known in advance, and summing the individual bounds over $k$ loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the $(d+1)$ -tuple $(F_0,\dots,F_d)$ . It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in $d+1$ measures, and solves it by duality.

Two steps carry most of the work. One is the almost-sure identity $A=B$ , which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in $C^d[0,1]$ . The bound $s^*_N\le d$ itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.

Formalization scope

Spaces. The decision space is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from $0$ . $\mathbb P$ is a probability measure and $\mathbb P^N$ is the product measure.
Tie-break. The tie-broken solution is the lexicographic minimiser of $(c^{\mathsf T}x,t_1(x),\dots,t_p(x))$ and depends only on the feasible set, which is what makes the exchangeability step valid. A support constraint is one whose removal changes this solution; this is not the platform's earlier "removal lowers the cost" notion.
Assumptions. Assumption 1 is required for every sample, Assumption 2 almost surely.
Measurability. The paper takes measurability for granted (footnote 1). Here it is two explicit hypotheses: the relation $\{(x,\delta):x\in\mathcal X_\delta\}$ is measurable, and every solution map $\omega\mapsto x^*_m(\omega)$ is measurable. No event is assumed measurable directly.
$F_k$ . $F_k$ is the finite measure on $\mathbb R$ given by the law of $V(x^*_k)$ on the event $\{s^*_k=k\}$ ; it is not normalised.
Problem (10). $C^d[0,1]$ is ContDiffOn ℝ d on $[0,1]$ , with derivatives taken within $[0,1]$ . $\gamma^*$ is a real infimum over a set that is nonempty ( $\xi(t)=t^N$ ) and bounded below by $0$ .
Probabilities are compared with real quantities through ENNReal.ofReal.
Theorem 2 is stated for every $\epsilon$ whose values $1-\epsilon(k)$ are roots of (11) in $(0,1)$ , which by its first part is the paper's $\epsilon$ .
Added hypothesis. The constant- $\epsilon$ companion assumes $d\ge1$ : at $d=0$ , $\epsilon=0$ its inequality is false.

Ruled-out trivializations:

The solution is never a free function of the sample.
The goal does not mention $F_k$ , moments or polynomials.
Assumption 1 is not weakened to almost surely.
$N>d$ is kept on Theorems 1, 2 and Corollary 1.
The indicators keep the paper's open and closed ends: $[0,1-\epsilon(k))$ in (10), $(\epsilon(k),1]$ in (16)–(21).

Contributions welcome:

the support-constraint bound under lexicographic tie-break, which is reusable for any convex scenario result;
the exchangeability lemma on Measure.pi;
the duality and density lemmas, which are pure analysis.

Selected references

M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming 167 (2018). https://doi.org/10.1007/s10107-016-1056-9
G. C. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102 (2005). https://doi.org/10.1007/s10107-003-0499-y
G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51 (2006). https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19 (2008). https://doi.org/10.1137/07069821X

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Supply Chain Coordination with Contracts IX: An Internal Market at the Shadow Price w(α, Q) Allocates Output Optimally, and Paying Its Expectation per Unit Induces the Optimal Effort e°Textbook

Motivation

In most contracts of the supply chain coordination literature the transfer payments are fixed when the contract is signed: a wholesale price $w$ , a buy-back rate $b$ , a revenue share $\phi$ . Some settings need payments that respond to information arriving after signing, such as realized demand at several retailers and realized production output. Fixing the per-unit price in advance then fails twice: for some output realizations the retailers do not buy everything that was produced, and for others they want more than exists, so the supplier must ration, which invites strategic ordering and misallocation (Cachon and Lariviere, 1999).

Section 6.9 of Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) studies an alternative after Kouvelis and Lariviere (2000): the supplier commits to hold an internal market for output after demand is observed, and pays her own production manager a fixed amount per unit of realized output. The model is a variant of Porteus and Whang (1991), who studied incentives between manufacturing and marketing managers in a firm. The section shows that this pair of mechanisms coordinates both the production decision and the allocation decision without the supplier observing either the demand shocks or the manager's effort.

This mission is part IX of a series formalizing the capstone results of that chapter.

Setting

One supplier employs a production manager and sells to two independent retailers. The constant demand elasticity is $\eta>1$ .

The manager chooses a production input level $e\ge0$ . The output is $Q=Ye$ , where $Y\in[0,1]$ is a random variable. The manager incurs the cost $c(e)$ , strictly convex and increasing, with derivative $c'$ .
Retailer $i\in\{1,2\}$ observes the realization $\alpha_i$ of a random variable $A_i>0$ .
The supplier allocates $q_i$ units to retailer $i$ with $q_1+q_2\le Q$ . Retailer $i$ earns revenue $q_ip_i(q_i)$ with the inverse demand $p_i(q_i)=\alpha_iq_i^{-1/\eta}$ , that is, $\alpha_iq_i^{(\eta-1)/\eta}$ .

If retailer one receives the share $\gamma$ of $Q$ , total retailer revenue is

\pi(\gamma,\alpha,Q)=\big(\alpha_1\gamma^{(\eta-1)/\eta}+\alpha_2(1-\gamma)^{(\eta-1)/\eta}\big)Q^{(\eta-1)/\eta}.

The optimal share is $\gamma^o(\alpha)=\alpha_1^\eta/(\alpha_1^\eta+\alpha_2^\eta)$ (Eq. (44)), and $\pi(\alpha,Q)=\pi(\gamma^o(\alpha),\alpha,Q)$ is revenue under it. The expected supply chain profit is $\Pi(e)=E[\pi(A,Ye)]-c(e)$ , and the optimal effort $e^o$ solves the first-order condition (45).

In the decentralized system, if the per-unit price is $w$ , retailer $i$ 's profit is $\pi_i(q_i,w)=\alpha_iq_i^{(\eta-1)/\eta}-wq_i$ . The contingent price is

w(\alpha,Q)=\Big(\frac{\eta-1}{\eta}\Big)(\alpha_1^\eta+\alpha_2^\eta)^{1/\eta}Q^{-1/\eta}.

The manager is paid a fixed amount per unit of realized output. With $K=E\big[(A_1^\eta+A_2^\eta)^{1/\eta}Y^{(\eta-1)/\eta}\big]$ , the payment is

\Big(\frac{\eta-1}{\eta}\Big)(e^o)^{-1/\eta}K/E[Y]\qquad(46),

and his expected utility is $u(e)=(\text{payment})\cdot E[Ye]-c(e)$ .

Formalization targets

Goal

The goal has two parts.

For every realization $\alpha_1,\alpha_2>0$ and output $Q>0$ , at the price $w(\alpha,Q)$ retailer one's unique optimal order is $\gamma^o(\alpha)Q$ and retailer two's is $(1-\gamma^o(\alpha))Q$ . So the retailers order exactly $Q$ , the allocation maximizes revenue over all feasible allocations, and

\frac{\partial\pi(\alpha,Q)}{\partial Q}=w(\alpha,Q).

If $e^o>0$ satisfies (45), then under the payment (46) the manager's unique optimal effort is $e^o$ . The payment equals $E[Qw(A,Q)\mid e^o]/E[Q\mid e^o]$ , and the supplier's expected profit from the market is zero.

Milestones

(44): revenue is strictly concave in $\gamma$ , and $\gamma^o(\alpha)$ is the unique optimal share.
The closed form $\pi(\alpha,Q)=(\alpha_1^\eta+\alpha_2^\eta)^{1/\eta}Q^{(\eta-1)/\eta}$ .
(45): $\Pi(e)=Ke^{(\eta-1)/\eta}-c(e)$ is strictly concave, and an interior $e^o$ is optimal if and only if $((\eta-1)/\eta)(e^o)^{-1/\eta}K-c'(e^o)=0$ .
The retailers' first-order condition, and the market allocation at $w(\alpha,Q)$ .
$\partial\pi(\alpha,Q)/\partial Q=w(\alpha,Q)$ .
The identity (46).
The manager's optimal effort and the supplier's zero expected profit.

Significance

The result shows that one mechanism handles two separate information problems. The market price $w(\alpha,Q)$ is the shadow price of output. Charging it makes the retailers' independent orders add up to exactly the output and split it as the integrated firm would, and the supplier never needs to observe $A$ . Paying the manager the output-weighted expectation of that shadow price, a single number fixed in advance, aligns his marginal incentive with the supply chain's, and the supplier does not need to observe $e$ . The supplier breaks even on the market. Kouvelis and Lariviere (2000) show that in more general settings she breaks even or loses money, so any profit must come from fixed fees. The section therefore illustrates a general design principle: market-based transfer prices inside a firm, combined with linear output-based pay.

The derivations are short calculus on the page. Formalizing them pins down what the page leaves implicit: the range of efforts and allocations; the role of $E[Y]>0$ and of the integrability of the shock; the fact that each retailer's problem has a unique interior optimum only at a positive price; and how the realized output $Q=0$ enters the expectation $E[Qw(A,Q)]$ . To our knowledge none of these statements has been machine-checked before.

Difficulty

The deterministic part requires real-power calculus with a non-integer exponent $(\eta-1)/\eta\in(0,1)$ . Strict concavity of $\gamma\mapsto\gamma^{(\eta-1)/\eta}$ has to be used on the closed interval $[0,1]$ , where the derivative blows up at the endpoints. The retailer's optimum has to be shown to be interior even though the profit at $q=0$ is defined.

The stochastic part requires pulling the effort out of the expectation, $E[\pi(A,Ye)]=Ke^{(\eta-1)/\eta}$ , pointwise in the shock, including at realizations with $Y=0$ . The natural first idea, to differentiate under the expectation sign, is unnecessary but tempting. The obstacle it hides is that $w(\alpha,Ye)$ is undefined where $Y=0$ , so the identity (46) only holds once $Qw(A,Q)$ is read as its limit $0$ at $Q=0$ . Uniqueness of the manager's optimum depends on strict convexity of $c$ alone, since his payment is linear in $e$ .

Formalization scope

All objects live in the namespace CachonCoord.InternalMarket. The deterministic file Revenue defines $\pi(\gamma,\alpha,Q)$ , $\gamma^o(\alpha)$ (as the printed formula, not as an argmax), $\pi(\alpha,Q)$ , $\pi_i(q_i,w)$ and $w(\alpha,Q)$ with real powers (Real.rpow). The file Model bundles a probability space with measurable $A_1,A_2>0$ and $Y\in[0,1]$ , the elasticity $\eta>1$ , and the cost $c$ . The cost is strictly convex and increasing on $[0,\infty)$ and has derivative $c'$ at every $e>0$ . On top of these, Model defines $\Pi$ , $K$ , the payment (46) (by its printed left side, not as the ratio it is claimed to equal), expected output and market revenue, and the manager's utility (from the payment scheme, not by the printed formula). Derivatives are HasDerivAt statements and optima are IsMaxOn over $[0,1]$ or $[0,\infty)$ .

The standing assumptions are those of the model paragraph on p. 92: risk neutrality and the distributional assumptions above. Added hypotheses, each disclosed in the item's Formalization Note:

$E[Y]>0$ , because (46) divides by it.
Integrability of $(A_1^\eta+A_2^\eta)^{1/\eta}Y^{(\eta-1)/\eta}$ .
A positive price in the retailer's first-order condition.
Differentiability of $c$ only on $(0,\infty)$ .

The existence of an effort satisfying (45) is a hypothesis, as on the page. Clauses 1 of the goal are stated for fixed realizations, not as random variables.

A trivializing formalization would define $\gamma^o(\alpha)$ as an argmax, or define the payment (46) as $E[Qw]/E[Q]$ ; neither is done here. Outside $\gamma\in[0,1]$ and $Q>0$ , Lean's real power returns junk values, and every statement restricts to that range. The companion claim that $w(\alpha,Q)$ is the unique market-clearing price is not posed.

The formalization needs no infrastructure beyond Mathlib's real powers, convexity and Bochner integral. The concavity and first-order-condition lemmas for $x\mapsto ax^{r}-bx$ with $0<r<1$ may be reused for other constant-elasticity models. Contributions are welcome at any milestone; each is independent of the others except through the closed forms.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6, §6.9. https://doi.org/10.1016/S0927-0507(03)11006-7 (formalized from the author's 3rd draft, January 2003).
P. Kouvelis and M. A. Lariviere, Decentralizing cross-functional decisions: Coordination through internal markets, Management Science 46(8), 2000, 1049–1058. https://doi.org/10.1287/mnsc.46.8.1049.12025
E. L. Porteus and S. Whang, On manufacturing/marketing incentives, Management Science 37(9), 1991, 1166–1181. https://doi.org/10.1287/mnsc.37.9.1166
G. P. Cachon and M. A. Lariviere, Capacity choice and allocation: strategic behavior and supply chain performance, Management Science 45(8), 1999, 1091–1108. https://doi.org/10.1287/mnsc.45.8.1091

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts X: Under Forced Compliance, Options Contracts with Shares λ_l and min{λ_h, λ̂_h} Separate the Two Demand Types and Coordinate CapacityTextbook

Motivation

A manufacturer launching a new product often depends on a single supplier for a critical component, and the supplier must build capacity before demand is known. The manufacturer usually knows more about demand than the supplier does: her sales force, market research and order history give her a forecast the supplier cannot verify, and she has a reason to inflate it, since more capacity costs her nothing if the supplier pays for it. Whether contracts can make forecast sharing credible, and at what cost to the supply chain, is the subject of Cachon and Lariviere, "Contracting to assure supply: how to share demand forecasts in a supply chain" (Management Science 47(5), 2001, doi:10.1287/mnsc.47.5.629.10486). Section 6.10 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents a simplified version of that model, and this mission formalizes it from the author's January 2003 draft.

The section separates two regimes. Under forced compliance the supplier must build exactly the capacity the contract specifies; under voluntary compliance he may build less. The section's conclusion is that forced compliance allows both coordination and credible forecast sharing, while voluntary compliance allows forecast sharing only at the price of under-investment in capacity.

Setting

Demand $D_\theta$ has one of two types $\theta \in \{h, l\}$ with distribution function $F_\theta(x) = F(x\mid\theta)$ . The page assumes $F_\theta(x) = 0$ for $x < 0$ , $F_\theta(x) > 0$ for $x \ge 0$ (so demand has an atom at $0$ ), $F_\theta$ increasing and differentiable, and stochastic dominance $F_h(x) < F_l(x)$ for all $x \ge 0$ . The supplier $S$ builds capacity $k$ at cost $c_k > 0$ per unit; after demand is observed he produces $\min\{D_\theta, k\}$ at cost $c_p > 0$ per unit; the manufacturer $M$ earns $r > c_p + c_k$ per unit of demand satisfied; unused capacity is worth nothing.

Expected sales with $x$ units of capacity are $S_\theta(x) = x - E[(x - D_\theta)^+]$ , and the supply chain's expected profit is

\Omega_\theta(k) = (r - c_p)S_\theta(k) - c_k k .

An optimal capacity $k_\theta^o$ maximizes $\Omega_\theta$ over $k \ge 0$ , and $\Omega_\theta^o = \Omega_\theta(k_\theta^o)$ .

In an options contract $M$ buys $q_i$ options at $w_o$ each and pays $w_e$ for each option exercised. With $k = q_i$ her profit is $\Pi_\theta(q_i) = (r - w_e)S_\theta(q_i) - w_o q_i$ and the supplier's is $(w_e - c_p)S_\theta(q_i) + w_o q_i - c_k q_i$ . The contract with share $\lambda$ sets $r - w_e = \lambda(r - c_p)$ and $w_o = \lambda c_k$ . Under a wholesale price contract with price $w$ the supplier earns $\pi_\theta(k) = (w - c_p)S_\theta(k) - c_k k$ ; the price inducing capacity $k$ is $w_\theta(k) = c_k/\bar F_\theta(k) + c_p$ with $\bar F_\theta = 1 - F_\theta$ , and the manufacturer then earns $\Pi_\theta(k) = (r - w_\theta(k))S_\theta(k)$ .

With asymmetric information only $M$ observes $\theta$ . Let $\hat\pi$ be the supplier's minimum acceptable profit, and define the shares

\lambda_l = 1 - \frac{\hat\pi}{\Omega_l^o},\qquad \lambda_h = 1 - \frac{\hat\pi}{\Omega_h^o},\qquad \hat\lambda_h = \frac{\Omega_l^o - \hat\pi}{\Omega_l(k_h^o)},\qquad \lambda_H = \min\{\lambda_h, \hat\lambda_h\}.

Formalization targets

Goal: forced-compliance separating contracts (§6.10.3, pp. 103–104)

The low type offers the options contract with share $\lambda_l$ and initial order $k_l^o$ , the high type the one with share $\lambda_H$ and initial order $k_h^o$ . Assuming $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$ :

0 < \lambda_l < \lambda_H < 1,\qquad \lambda_l\,\Omega_h(k_l^o) < \lambda_H\,\Omega_h^o,\qquad \lambda_H\,\Omega_l(k_h^o) \le \Omega_l^o - \hat\pi,

the supplier earns $\hat\pi$ from the low type and at least $\hat\pi$ from the high type, and each initial order $k_\theta^o$ maximizes both firms' profits. The profit comparisons are stated between the contract profit functions, not between shares.

Milestones

$S_\theta(x) = x - \int_0^x F_\theta$ (p. 98).
$\Omega_\theta$ is concave, and $k > 0$ is optimal iff $\bar F_\theta(k) = c_k/(r - c_p)$ (p. 99).
$\Omega_l(k) < \Omega_h(k)$ for $k > 0$ , hence $\Omega_l^o < \Omega_h^o$ (implicit on p. 104).
The options contract with share $\lambda \in [0,1]$ gives $\Pi_\theta = \lambda\Omega_\theta$ and the supplier $(1-\lambda)\Omega_\theta$ , so it coordinates (pp. 99–100).
Under voluntary compliance, $\partial\pi(k_\theta^o, k_\theta^o, \theta)/\partial k < 0$ (p. 100).
A capacity $k > 0$ is optimal for the supplier under a wholesale price $w$ iff $w = w_\theta(k)$ (p. 101).
A stationary point $k^*$ of $\Pi_\theta$ satisfies $\bar F_\theta(k^*) = \bar F_\theta(k_\theta^o)\bigl(1 + f_\theta(k^*)S_\theta(k^*)/\bar F_\theta(k^*)^2\bigr)$ , so $k^* < k_\theta^o$ (p. 102).

Significance

The goal shows that with forced compliance a high-demand manufacturer can share her forecast credibly through the terms of a coordinating contract rather than its form: both types use the same contract family, the supply chain is coordinated in every state, and the only cost of asymmetric information is that the high type may be unable to push the supplier down to his reservation profit. The voluntary-compliance milestones show the other side: once the supplier may under-build, only the wholesale price affects his capacity, and the resulting capacity is strictly below the integrated optimum. Together they explain why compliance regimes matter in capacity contracting.

The results are established on the page with short arguments; none has a machine-checked proof. Formalizing them requires the derivative of expected sales for a distribution with an atom, the first-order characterization of a concave maximizer on a half-line, and careful bookkeeping of the incentive constraints. The demand and profit definitions are reusable for other capacity-procurement and newsvendor-type models.

Difficulty

The incentive constraints look like arithmetic on shares, but the strict inequality $\lambda_l < \hat\lambda_h$ needs $\Omega_l(k_h^o) < \Omega_l^o$ : the low type's chain profit at the high type's capacity must be strictly below its optimum. The obvious argument via uniqueness of the maximizer is not available, because the page does not assume $F_\theta$ strictly increasing, so $\Omega_l$ need not be strictly concave and may have a whole interval of maximizers. Likewise $\Omega_l^o < \Omega_h^o$ needs a strict comparison of integrals of distribution functions. In the voluntary-compliance part, the derivative of $w_\theta(k)$ needs the density at $k^*$ , and $k^* < k_\theta^o$ fails when that density is $0$ .

Formalization scope

Each demand law is a probability measure on $\mathbb R$ and $F_\theta$ is Mathlib's cdf. $F_\theta$ is required to be differentiable only on $(0,\infty)$ , because the page's $F_\theta(0) > 0$ makes it jump at $0$ . $S_\theta$ is defined by the expectation $x - E[(x - D_\theta)^+]$ , whose integrand is integrable because $D_\theta \ge 0$ almost surely. Optimal capacities are passed as arguments characterized as maximizers over $[0,\infty)$ , never chosen; $k_\theta^o > 0$ is footnote 46's assumption. Derivatives are HasDerivAt statements.

Hypotheses added relative to the page, all disclosed in the items: $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$ in the goal (the page divides by $\Omega_l(k_h^o)$ and needs $\lambda_l \in (0,1)$ ); $\lambda > 0$ for the voluntary-compliance derivative (at $\lambda = 0$ it vanishes); $\bar F_\theta(k^*) > 0$ and $f_\theta(k^*) > 0$ for the non-coordination result. The page's assumption $w''_\theta > 0$ is not needed and not imposed; its strict-concavity claim on p. 101 is not stated, because it would need $F_\theta$ strictly increasing. The prior $\Pr(\theta = h) = \rho$ does not enter any statement. The page's "separating equilibrium" is formalized by its defining incentive and participation conditions, not by a general signalling-game solution concept; a predicate that holds by construction of $\hat\lambda_h$ (for example $\lambda_H \le \hat\lambda_h$ ) is not an acceptable substitute for the profit inequalities. The fixed-fee condition of p. 105 is pure algebra on four numbers and is not included.

All definitions are local to the namespace CachonCoord.CapacityForecast. No platform theorem formalizes this model; the Snyder–Shen newsvendor definitions (SupplyChainTheory_contracts) and the revenue-sharing model of Cachon–Lariviere 2005 (RevShareCoord.*) concern different games and are not reused. Proofs of any milestone, and a sanity instance showing the model's hypotheses are satisfiable (for example demand with an atom $p_\theta$ at $0$ and an exponential tail, $p_h < p_l$ ), are welcome.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. doi:10.1016/S0927-0507(03)11006-7 (formalized from the author's 3rd draft, January 2003).
G. P. Cachon and M. A. Lariviere, Contracting to assure supply: how to share demand forecasts in a supply chain, Management Science 47(5), 629–646, 2001. doi:10.1287/mnsc.47.5.629.10486
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (increasing failure rate distributions, cited on p. 102).

10 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Wait-and-Judge Scenario Optimization 2: Over Generic Sets, P^N{V(x_N) > ε(s_N)} ≤ γ*, the Least ξ(1) over Degree-N Polynomials Feasible for (31)Research Paper

Motivation

A solution of a scenario optimization program is chosen after observing finitely many uncertain constraints. Its future reliability depends on constraints that were not sampled. The usual advance question asks how many samples are needed to make every output reliable. Campi and Garatti instead ask what can be certified after solving the program, when the number of sampled constraints that actually determined its solution is visible. Their wait-and-judge result uses that observed number to set a violation threshold. This mission concerns their extension from convex programs in finite-dimensional spaces to programs over an arbitrary decision set, with no convexity requirement.

The generic extension matters when a dimension bound on the number of influential constraints is unavailable. A decision may be a combinatorial object, a function, or an element of an infinite-dimensional space. The paper allows the support count to range from zero to the full sample size $N$ , and its threshold includes the case of $N$ support constraints. The paper's Section 6 gives the model and its two probability guarantees.

Setting

Let $S$ be a set of decisions. A subset $X\subseteq S$ is the domain; a real function $f:S\to\mathbb R$ is the cost. An uncertain outcome $\delta$ belongs to a measurable space $\Delta$ with probability measure $P$ , and imposes a constraint set $X_\delta\subseteq S$ . For a sample $\omega=(\delta^{(1)},\ldots,\delta^{(N)})$ of $N$ independent outcomes, the program minimizes $f(x)$ over $x\in X$ that belongs to every sampled $X_{\delta^{(i)}}$ . The sample law is $P^N$ . There is no algebraic or topological condition on the feasible sets or on $f$ .

A fixed finite sequence of real tie-break functions is minimized lexicographically after the original cost. This selects one solution $x_N^*(\omega)$ whenever the program has a selected minimizer. Assumption 1 requires existence and uniqueness for every finite sample, including the empty one. A sampled constraint is a support constraint if removing it changes this selected solution. The number of support constraints is $s_N^*(\omega)$ . Assumption 2 says that, with probability one, keeping only the support constraints gives the same selected solution. Both assumptions are part of the source's generic setting; they are substantive restrictions even though the sets and cost are otherwise arbitrary.

The violation of a decision is $V(x)=P\{\delta:x\notin X_\delta\}$ . Thus $V(x_N^*)$ is the probability that a fresh constraint rejects the computed solution. Since the solution and support count depend on the sample, the wait-and-judge event uses a threshold function $\varepsilon$ evaluated at the observed count, $\{V(x_N^*)>\varepsilon(s_N^*)\}$ . For each $k\ge0$ , the paper also uses a generalized distribution function $F_k(v)=P^k\{V(x_k^*)\le v,\ s_k^*=k\}$ . It need not have total mass one.

Formalization targets

Variational bound, Theorem 3

For any $N\ge1$ and any $[0,1]$ -valued $\varepsilon$ on $\{0,\ldots,N\}$ , let $\gamma^*$ be the infimum of feasible values $q(1)$ over real polynomials of degree at most $N$ satisfying

\frac{q^{(k)}(t)}{k!}\ge {N\choose k}t^{N-k}{\bf1}_{[0,1-\varepsilon(k))}(t),\qquad 0\le k\le N,\quad 0\le t\le1.

The goal is the paper's Theorem 3:

P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\gamma^*.

The polynomial value retains the full dependence on the chosen threshold function. The source prints an extraneous $d$ in Theorem 3's range for $k$ ; its generic setting and variational problem use $0\le k\le N$ .

Explicit confidence bound, Theorem 4

For $0<\beta<1$ , the paper's Theorem 4 defines $t(k)\in(0,1)$ as the unique root of

\frac{\beta}{N+1}\sum_{m=k}^{N}{m\choose k}t^{m-k}-{N\choose k}t^{N-k}=0\qquad(0\le k<N).

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

P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\beta.

The terminal value $\varepsilon(N)=1$ is essential because the paper gives examples with $s_N^*=N$ and $V(x_N^*)=1$ .

Significance

Theorem 3 makes the observed support count a usable statistic for assessing the solution's future constraint violation without a dimension bound. Theorem 4 turns it into a certificate at any chosen confidence parameter $\beta$ . The confidence threshold depends on the count seen after the program is solved. These statements do not claim that every generic program satisfies Assumptions 1–2; they say what follows for programs that do.

A formal development must make the statistical objects and the analytic value agree exactly: the solution must come from the feasible set and the fixed tie-break rule, the support count must record changes of solution, and $\gamma^*$ must be the value of the derivative-constrained polynomial problem. The reusable outputs include the generic scenario model, its generalized violation distributions, and the finite moment and dual formulations. The statements are known results of Campi and Garatti; this mission asks for machine-checked proofs of those results and their selected intermediate claims.

Difficulty

The observed support count is data-dependent. Conditioning on $s_N^*=k$ therefore cannot be treated as conditioning on a fixed subset of $k$ sample coordinates. Symmetry across possible support subsets must agree with the selected solution under removal of nonsupport constraints. Assumption 2 is what rules out a degenerate change of solution when only support constraints remain. In the generic setting the possible count grows with $N$ , so the distributional characterization has one measure $F_k$ for every $k\ge0$ and moment equations for every sample size. The resulting infinite family must still be related to the finite degree- $N$ polynomial value in (31). No convexity or finite-dimensional geometry is available to supply a fixed support bound.

Formalization scope

Lean represents the decision set by an arbitrary type $S$ , with a measurable structure only to state the paper's implicit measurability convention. Samples are functions Fin N → Δ with zero-based indices and product law Measure.pi. The published generic violation definition is reused. The domain, constraint family, cost, finite lexicographic tie-break, selected solution, support set, and $F_k$ are defined locally. A Nonempty S instance provides an unused fallback value to the total solution selector; Assumption 1 already implies that $S$ is nonempty.

The source takes measurability for granted in a footnote. Here the constraint relation is jointly measurable, every solution map is measurable, and each support event is measurable. These pins assign probabilities to the events the paper uses. The $F_k$ are finite measures on $\mathbb R$ , so the paper's Stieltjes integrals are represented as integrals over $(\varepsilon(k),1]$ or $[0,1]$ against those measures. The polynomial class $\mathcal P_N$ means degree at most $N$ , matching the $N+1$ coefficients in (36). The value $\gamma^*$ is a real infimum; a separate sanity proof gives a feasible polynomial and a zero lower bound on all feasible values.

The goal retains Assumptions 1–2 and states the actual tail bound. It does not assume the moment equations or a favorable value of $\gamma^*$ , and no support count is fixed in advance. Contributions toward the distributional decomposition, the moment equations, the finite weak-duality inequality, the polynomial identity, and the explicit-root theorem are within scope.

Selected references

M. C. Campi and S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. DOI: 10.1007/s10107-016-1056-9. The mission uses the authors' accepted manuscript, especially Sections 6–7 and Theorems 3–4.

7 thms1 active userReviewed

Combinatorics Operations Research Probability+1·Captain: mikedeng1

An Optimal Algorithm for On-line Bipartite Matching 2: No Randomized On-line Algorithm Guarantees an Expected Matching Larger Than n(1 − 1/e) + o(n)Research Paper

Motivation

An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of $1-1/e$ for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).

The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.

Setting

There are $n$ boys, represented by rows, and $n$ girls, represented by columns. A bipartite graph $G\subseteq[n]\times[n]$ records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of $G$ . This assumption supplies an offline benchmark of $n$ matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.

Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order $n,n-1,\ldots,1$ . A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance $p(A)$ is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).

The paper's hard family begins with the complete upper-triangular graph $T_n$ , where row $i$ is adjacent to column $j$ exactly when $i\le j$ . Its columns arrive from largest to smallest. Relabeling the rows by a permutation $\pi$ gives an instance $T_\pi$ that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write $V_{T_n}(n,\varnothing)$ for RANDOM's expected number of matches on $T_n$ , beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).

Formalization targets

Main theorem

For every $\varepsilon>0$ , there is one threshold $N$ such that, for every $n\ge N$ and every randomized online algorithm $A$ on $n$ rows and columns, a graph $G$ with a perfect matching satisfies

\mathbb E_A[|M(G)|]\le (1-e^{-1}+\varepsilon)n.

The threshold is uniform over algorithms. The graph may depend on $A$ . This is the quantified upper-bound reading of Theorem 2's $p(A)\le n(1-1/e)+o(n)$ (Karp, Vazirani, and Vazirani, 1990, Theorem 2).

Milestone statements

Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted $T_n$ with RANDOM's expected size on $T_n$ . Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit

\lim_{n\to\infty}\frac{V_{T_n}(n,\varnothing)}{n}=1-e^{-1}.

Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).

Significance

Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from $n$ is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.

Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.

Difficulty

For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the $o(n)$ claim in Lemma 16.

Formalization scope

Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order $n,\ldots,1$ is represented by zero-based order $n-1,\ldots,0$ ; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.

RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For $n=0$ , the matching and RANDOM value are zero; the main theorem is eventual in $n$ and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's $o(n)$ in Theorem 2 is stated as $\forall\varepsilon>0,\exists N,\forall n\ge N$ with $N$ before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.

Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.

Selected references

Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, pp. 352–358, 1990. DOI: 10.1145/100216.100262.

9 thms2 active usersReviewed

Complexity Theory Graph Theory Operations Research+1·Captain: mikedeng1

Complexity of Machine Scheduling Problems 6: DIRECTED HAMILTON PATH Reduces to No-Wait Flow Shop Makespan and Total Completion TimeResearch Paper

Motivation

In a no-wait flow shop every job passes through the machines $M_1,\dots,M_m$ in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of Hall and Sriskandarajah (doi:10.1287/opre.44.3.510). The question of how hard it is to schedule such a shop well is the question this mission formalizes.

Brucker, Lenstra and Rinnooy Kan settled it for the case in which the number of machines is part of the input. In their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977, doi:10.1016/S0167-5060(08)70743-X), Theorem 5 reduces DIRECTED HAMILTON PATH to the no-wait flow shop. Both minimizing the makespan $C_{\max}$ and minimizing the total completion time $\sum C_j$ are thereby NP-complete.

Timeline.

1964: Gilmore and Gomory solve the two-machine no-wait flow shop with makespan in polynomial time (doi:10.1287/opre.12.5.655).
1972: Wismer (doi:10.1287/opre.20.3.689) and Reddi and Ramamoorthy (doi:10.1057/jors.1972.52) show that no-wait makespan minimization is a travelling-salesman problem with arc weights computed from the processing times.
1972: Karp proves DIRECTED HAMILTON CIRCUIT NP-complete (doi:10.1007/978-1-4684-2001-2_9).
1975: Brucker, Lenstra and Rinnooy Kan reduce DIRECTED HAMILTON CIRCUIT to DIRECTED HAMILTON PATH (their Theorem 2(d)), and DIRECTED HAMILTON PATH to $n|m|F,\textit{no wait}|C_{\max}$ and to $n|m|F,\textit{no wait},w_j=1|\sum w_jC_j$ (Theorem 5).
1984: Röck shows that the problem stays NP-hard for three machines (doi:10.1145/62.65).

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines. Job $J_\ell$ needs processing time $p_{\ell i}\in\mathbb N$ on machine $M_i$ . Write

q_{\ell i}=\sum_{r=1}^{i}p_{\ell r},\qquad q_{\ell 0}=0,

for the time job $J_\ell$ spends on its first $i$ machines. Because a job never waits, a schedule is determined by the start times $B_\ell\in\mathbb N$ . The operation of $J_\ell$ on $M_i$ occupies $[B_\ell+q_{\ell,i-1},\,B_\ell+q_{\ell i})$ , and job $J_\ell$ completes at $C_\ell=B_\ell+q_{\ell m}$ . A schedule is feasible when no two distinct jobs occupy the same machine at the same time. The delay

c_{jk}=\max_{1\le i\le m}\{q_{ji}-q_{k,i-1}\}

is the least gap $B_k-B_j$ that lets $J_k$ follow $J_j$ on every machine.

A directed graph $G=(V,A)$ on $V=\{0,\dots,n-1\}$ has a Hamilton path if its vertices can be ordered $\sigma(0),\dots,\sigma(n-1)$ with every $(\sigma(i),\sigma(i+1))\in A$ .

From $G$ the paper builds an instance with $n$ jobs and $m=n(n-1)+2$ machines. Each ordered pair $(j,k)$ of distinct jobs is assigned a middle machine $\iota(j,k)\in\{2,\dots,m-1\}$ , and the partial sums $q_{\ell i}$ are perturbed from $i\mu$ by $\pm\lambda$ or $\pm(\lambda+1)$ on the machines $\iota(\ell,\cdot)$ and just before the machines $\iota(\cdot,\ell)$ , depending on whether the pair is an arc. The parameters satisfy $\lambda\ge1$ and $\mu\ge2\lambda+3$ .

Formalization targets

Goal (Theorem 5)

\text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait}|C_{\max}\quad\text{and}\quad \text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait},w_j=1|\textstyle\sum w_jC_j,

where $\propto$ is polynomial-time many-one reducibility between the binary-coded recognition languages.

Milestones, in the order the proof uses them

Eq. (9): $c_{jk}$ is the least gap between $B_j$ and $B_k$ for which $J_k$ follows $J_j$ on every machine.
The travelling-salesman reformulation: if all processing times are positive, a feasible schedule with $C_{\max}\le y$ (resp. $\sum C_\ell\le y$ ) exists iff some job order has path length (resp. summed completion times along the path) at most $y$ .
An admissible ordering $\iota$ exists for every $n\ne2$ .
All processing times of the construction are at least $1$ .
The delays of the construction: $c_{jk}=\mu+2\lambda$ if $(j,k)\in A$ , and $\mu+2\lambda+2$ otherwise.
Theorem 5(a), the equivalence: $G$ has a Hamilton path $\iff$ $C_{\max}\le(n-1)(\mu+2\lambda)+m\mu$ .
Theorem 5(b), the equivalence: $G$ has a Hamilton path $\iff$ $\sum_jC_j\le\tfrac12n(n-1)(\mu+2\lambda)+nm\mu$ .
Theorem 2(d), off the goal's path: $G'$ has a Hamilton circuit iff the graph obtained by splitting a vertex $v'$ into $v'$ and a new sink $v''$ has a Hamilton path.

Significance

The result. Theorem 5, together with the NP-completeness of DIRECTED HAMILTON PATH, places both no-wait criteria among the NP-complete problems once $m$ is part of the input. The Gilmore–Gomory algorithm for two machines therefore cannot be extended to arbitrary $m$ unless P = NP, and heuristics and exact exponential methods for no-wait shops are justified. The reduction also gives a structural fact of independent use: every directed graph can be realized, up to two arc-weight values, as the delay matrix of a no-wait flow shop.

Formalizing it. The result has been proved for fifty years; to our knowledge no machine-checked version exists. This mission produces a checked no-wait flow shop model, a checked travelling-salesman reformulation of it, the correctness of the paper's construction, and a polynomial-time reduction in an explicit Turing-machine model. It also records a gap in the printed proof: the ordering $\iota$ the paper calls easy to construct does not exist for $n=2$ .

Difficulty

Three steps are not routine.

The passage from schedules to job orders assumes that the order in which jobs start is the order in which they visit every machine. With zero processing times this fails, so the reformulation needs the positivity milestone.
Computing the delays requires a case analysis over all machines and all pairs of perturbations. The property of $\iota$ is exactly what keeps the " $+$ " and " $-$ " cases from colliding, and the constants $\lambda\ge1$ , $\mu\ge2\lambda+3$ are tight enough that the comparison must be done carefully.
The goal asks for an actual Turing machine with a polynomial step bound. It has to build $\iota$ for every $n\ne2$ and handle $n\le2$ separately. The equivalences alone do not give this.

Formalization scope

Jobs and machines are $0$ -based (Fin n, Fin m); cum p ℓ i is the paper's $q_{\ell i}$ , and the machine indices $\iota(j,k)$ are the paper's $1$ -based indices. Start times are natural numbers, and release dates are $0$ . Section 3 computes times from processing orders on integer data, and every criterion is regular, so real start times would not change the yes-instances. A zero-length operation occupies the empty interval. $C_{\max}\le y$ is stated as $C_\ell\le y$ for every job. The delays, the partial sums of the construction and its processing times are computed in $\mathbb Z$ . The instance uses their conversion to $\mathbb N$ , which is exact by milestone 4. The threshold of Theorem 5(b) is compared in $\mathbb Q$ , as printed.

The paper's loose phrases are made explicit as follows:

"scheduled directly after" means "precedes on every machine";
"equivalent to solving the TRAVELLING SALESMAN problem" means the two threshold equivalences of milestone 2, with the $\sum C_j$ version as the reading of "constructed as in (a)";
"such an ordering can easily be constructed" is stated for $n\ne2$ , the only case in which it is true.

Directed graphs are Boolean adjacency matrices. A graph with $0$ or $1$ vertices has a Hamilton path, and a one-vertex graph has a Hamilton circuit iff it has a loop.

The goal is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs, with polynomial time measured on Cook's one-tape Turing machines. Instances are coded with the alphabet BSym and binary code encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). A graph is coded as $n$ followed by its adjacency matrix; a flow-shop instance as $n$ , $m$ , the matrix $(p_{\ell i})$ and the threshold $y$ .

Stating only the equivalences 6–7 and calling the result "reducible" would drop polynomiality; the goal therefore asserts PolyReducible. The target languages contain exactly the no-wait flow-shop instances, with no waiting allowed, so the reduction cannot land in a looser problem. The parameters $\lambda,\mu$ always carry $\lambda\ge1$ , $\mu\ge2\lambda+3$ .

Contributions are welcome at every level:

the general travelling-salesman reformulation, which is reusable for any no-wait flow-shop result;
the combinatorial existence of $\iota$ ;
the arithmetic of the construction;
Turing-machine infrastructure for computing arithmetic list transformations in polynomial time, which every reduction in this series needs.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9
P. C. Gilmore, R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12 (1964) 655–679. doi:10.1287/opre.12.5.655
D. A. Wismer, Solution of the flowshop-scheduling problem with no intermediate queues, Operations Research 20 (1972) 689–697. doi:10.1287/opre.20.3.689
S. S. Reddi, C. V. Ramamoorthy, On the flow-shop sequencing problem with no wait in process, Operational Research Quarterly 23 (1972) 323–331. doi:10.1057/jors.1972.52
H. Röck, The three-machine no-wait flow shop is NP-complete, Journal of the ACM 31 (1984) 336–345. doi:10.1145/62.65
N. G. Hall, C. Sriskandarajah, A survey of machine scheduling problems with blocking and no-wait in process, Operations Research 44 (1996) 510–525. doi:10.1287/opre.44.3.510
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047

14 thms3 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 7: Makespan Reduces to Total Completion Time on Identical Machines with Precedence ConstraintsResearch Paper

Motivation

Scheduling jobs on parallel machines under precedence constraints is the core model of project and parallel-processing scheduling: a job may start only after its predecessors have finished. Two criteria dominate the literature, the makespan $C_{\max}$ (when does the last job finish?) and the total completion time $\sum_j C_j$ (how long do jobs wait on average?). Knowing that one criterion is at least as hard as the other lets a hardness proof for one transfer to the other without a new reduction from a combinatorial problem.

Brucker, Lenstra and Rinnooy Kan's report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; later in Annals of Discrete Mathematics 1, 1977) collected the complexity status of the standard scheduling problems and stated a set of elementary reductions among them as Theorem 1. Part (l) reduces makespan to total completion time for identical machines with precedence constraints and bounded processing times.

Timeline.

1971–1972: Cook (doi:10.1145/800157.805047) and Karp (doi:10.1007/978-1-4684-2001-2_9) introduce NP-completeness and polynomial reducibility.
1975: Ullman (doi:10.1016/S0022-0000(75)80008-0) proves that the makespan problems $n|2|I,\mathit{prec},1\le p_{j1}\le 2|C_{\max}$ and $n|m|I,\mathit{prec},p_{j1}=1|C_{\max}$ are NP-complete, by reductions from 3-SATISFIABILITY.
1975: Brucker, Lenstra and Rinnooy Kan state Theorem 1(l); their Table III (p. 13) applies it to Ullman's two problems and concludes that the corresponding total completion time problems are NP-complete.

Setting

An instance has $n$ jobs $J_1,\dots,J_n$ , a number $m \ge 1$ of identical machines, a processing time $p_j$ for each job, and a precedence relation $<$ on the jobs: $J_j < J_k$ means that $J_k$ may start only after $J_j$ has completed. Each job is one operation, processed without interruption on any one machine. For a constant $p_*$ , the class $n|m|I,\mathit{prec},1\le p_{j1}\le p_*$ requires $1 \le p_j \le p_*$ for every job and an acyclic precedence relation.

A schedule assigns to every job a machine and a starting time $B_j \in \mathbb N$ ; the completion time is $C_j = B_j + p_j$ . It is feasible if two jobs on the same machine never overlap and $J_j < J_k$ implies $C_j \le B_k$ .

Following the paper, each optimization problem is replaced by its recognition version. Problem $P'$ asks, for an instance and a threshold $y'$ , whether some feasible schedule has $C_{\max} = \max_j C_j \le y'$ . Problem $P$ asks, for an instance of the same class and a threshold $y$ , whether some feasible schedule has $\sum_j C_j \le y$ (all weights $w_j = 1$ ).

$P'$ is reducible to $P$ , written $P' \propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 1(l)

For every constant $p_* \ge 1$ ,

n'|m|I,\mathit{prec},1\le p_{j1}\le p_*|C_{\max} \;\propto\; n|m|I,\mathit{prec},1\le p_{j1}\le p_*,w_j=1|\textstyle\sum w_jC_j .

Milestones

A trivial upper bound. Every instance of $P'$ with $n'$ jobs has a feasible schedule with $C_{\max} \le n'p_*$ .
The construction and the forward direction. For $0 \le y' \le n'p_*$ let $n'' = (n'-1)y'$ , $n = n'+n''$ and $y = ny' + \tfrac12 n''(n''+1)$ , and add $n''$ unit-time jobs $J_{n'+k}$ , each required to follow every original job and every earlier added job. If $P'$ has a schedule with $C_{\max} \le y'$ , the new instance has a feasible schedule with $\sum_j C_j \le y$ .
The backward direction. If every feasible schedule of $P'$ has $C_{\max} > y'$ , every feasible schedule of the new instance has $\sum_j C_j > y$ .

Significance

The result. Theorem 1(l) makes the total completion time problem at least as hard as the makespan problem in the same class. Combined with Ullman's NP-completeness results and Theorem 1(b) (reducibility transfers NP-completeness), it shows that minimizing $\sum_j C_j$ on identical machines with precedence constraints is NP-complete, already for two machines with $p_j \in \{1, 2\}$ and for unit processing times on $m$ machines. These are two rows of the paper's Table III.

Formalizing it. The result is proved on one page of a typewritten report; no machine-checked version exists. The mission produces a scheduling model for identical machines with precedence constraints, binary languages for the two recognition problems, and the reduction in Cook's Turing-machine model. The proof's displayed bounds contain a misprinted index range, which the formal statements correct.

Difficulty

The two criteria are not monotonically related: a schedule with a smaller makespan can have a larger total completion time than one with a larger makespan. So the obvious reduction, keeping the instance and asking for $\sum_j C_j \le n'y'$ , is not an equivalence: a no-instance of $P'$ can have a schedule with small total completion time. The instance has to be changed so that the total completion time is governed by the makespan, and the comparison of the two thresholds must be exact, including the strict inequality on the "no" side, which depends on integral completion times and positive processing times.

The main formal difficulty lies in the reduction itself. A polynomial-time Turing machine must decode the binary instance, check that it belongs to the class (including acyclicity of the precedence relation), compare $y'$ with $n'p_*$ , and write out an instance with $n'' = (n'-1)y'$ additional jobs and a quadratic-size precedence matrix. The size of that output is polynomial only because $p_*$ is a constant: a version with $p_*$ part of the input would make $n''$ exponential in the input length.

Formalization scope

Jobs and machines are indexed from $0$ (Fin n, Fin m). Starting times are natural numbers; Section 3 derives all times from processing orders on nonnegative integer data, and both criteria are regular. " $C_{\max} \le y$ " is written as " $C_j \le y$ for every $j$ ".
The precedence relation is a Boolean matrix. Its acyclicity and $m \ge 1$ are part of the problem class; the paper leaves both implicit, and the claim "any instance has a solution with $C_{\max} \le n'p_*$ " fails without them.
$p_*$ is a constant of the class and a parameter of both languages, not part of the input. All weights in the target problem equal $1$ and are not written.
The threshold $y = ny' + \tfrac12 n''(n''+1)$ is stated in $\mathbb Q$ exactly as printed in the milestones; it is an integer, and the reduction uses its natural-number value.
The paper's displayed bounds $n'y' + \sum_{k=n'+1}^{n}(y'+k) = y$ and $y' + \sum_{k=n'+1}^{n}(y'+1+k) = y$ have a misprinted index range (the sums must run over $k = 1,\dots,n''$ ). The milestones state the end-to-end bounds $\sum_j C_j \le y$ and $\sum_j C_j > y$ .
" $C_{\max} > y'$ " in the backward direction is read as the negation of the forward hypothesis: no feasible schedule of $P'$ has $C_{\max} \le y'$ .
"Reducible" is Cook's polynomial-time many-one reducibility from the published definition CookPvsNP_defs; numbers are written in binary with the alphabet and code encNats of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). The unit-time model ResourceScheduling.Chain.Model (Błażewicz, Lenstra and Rinnooy Kan) has the same feasibility conditions but unit processing times and real start times, so the model here is defined anew.
A trivializing formalization is ruled out: the goal asserts a polynomial-time computable map, not the bare equivalence, and codes of instances outside the class are excluded from both languages, so the reduction cannot exploit malformed inputs.
Contributions welcome: proofs of the three milestones, a Turing-machine library for arithmetic on binary codes (reusable across this series), and a proof of the goal from the milestones.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; published in Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
J. D. Ullman, NP-complete scheduling problems, Journal of Computer and System Sciences 10 (1975) 384–393. doi:10.1016/S0022-0000(75)80008-0
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9

9 thms3 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 4: With Times in {p, q} and gcd(p, q) = 1, a q-Dimensional Matching Exists Iff a Schedule Has Makespan ≤ pqResearch Paper

Motivation

Minimum makespan scheduling on unrelated parallel machines asks for an assignment of $n$ jobs to $m$ machines, where job $j$ takes $p_{ij}$ time units on machine $i$ , so that the largest machine load is as small as possible. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) it is $R\,\|\,C_{\max}$ . It models load balancing across heterogeneous processors, workers or production lines, and it is a standard test case for linear-programming rounding.

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714; Mathematical Programming 46, 1990) gave a polynomial 2-approximation algorithm for $R\,\|\,C_{\max}$ and showed that no polynomial algorithm achieves a ratio below $3/2$ unless P = NP. They also asked which restrictions on the processing times keep the problem hard. Their Section 5 answers this when only two distinct processing times occur:

all $p_{ij}=1$ : trivial;
all $p_{ij}\in\{1,\infty\}$ : bipartite cardinality matching;
all $p_{ij}\in\{1,2\}$ : polynomial by matching techniques (Theorem 6);
all $p_{ij}\in\{p,q\}$ with $p<q$ , $2p\ne q$ : NP-hard (Theorem 7).

Theorem 7 is the paper's last result and closes this classification. Its proof generalizes the reduction of Theorem 4, which handles the case $\{1,3\}$ , from 3-dimensional matching to $q$ -dimensional matching.

Setting

Machines are indexed by $i\in\{1,\dots,m\}$ and jobs by $j$ . A schedule $\sigma$ assigns every job to exactly one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$ , and the makespan $C_{\max}(\sigma)$ is the largest load.

$q$ -dimensional matching. An instance is a ground set $U$ of $qn$ elements and a family $S_1,\dots,S_m$ of $q$ -element subsets of $U$ . A matching is a subfamily $F'\subseteq\{1,\dots,m\}$ with $|F'|=n$ and $\bigcup_{i\in F'}S_i=U$ ; its members are then pairwise disjoint.

The instance of Theorem 7. Fix natural numbers $0<p<q$ that are relatively prime. Build a scheduling instance with $m$ machines, machine $i$ corresponding to $S_i$ , and two kinds of jobs:

$qn$ element jobs, one per $u\in U$ , with $p_{iu}=p$ if $u\in S_i$ and $p_{iu}=q$ otherwise;
$p(m-n)$ dummy jobs, each taking $q$ time units on every machine.

Every processing time lies in $\{p,q\}$ .

The instance of Theorem 4. For disjoint sets $A=\{a_1,\dots,a_n\}$ , $B$ , $C$ of the same size and triples $T_i=(a_j,b_k,c_l)$ , $i=1,\dots,m$ , there are $3n$ element jobs, one per element of $A\cup B\cup C$ , and $m-n$ dummy jobs. Machine $i$ processes the element jobs of $a_j$ , $b_k$ , $c_l$ in one time unit and every other job in three time units. A 3-dimensional matching is a subfamily of $n$ triples covering $A\cup B\cup C$ .

Formalization targets

Goal: Theorem 7 (p. 8; proof pp. 8–9)

For relatively prime $0<p<q$ and a family of $q$ -subsets $S_1,\dots,S_m$ of a $qn$ -element set, the instance above has all processing times in $\{p,q\}$ , and

\exists\,\sigma:\ C_{\max}(\sigma)\le pq \quad\Longleftrightarrow\quad \exists\,F'\subseteq\{1,\dots,m\}:\ |F'|=n,\ \bigcup_{i\in F'}S_i=U .

Milestones

Theorem 4 (p. 7): on the 3-dimensional matching instance with times in $\{1,3\}$ , a schedule with makespan at most $3$ exists iff a matching exists.
Matching gives a schedule (pp. 8–9): if $S$ has a matching, some schedule has $C_{\max}\le pq$ .
No idle time, two kinds of machine (p. 9): in every schedule with $C_{\max}\le pq$ , three things hold. Every load equals $pq$ . Every element job runs at length $p$ , on a machine whose tuple contains it. Each machine processes either exactly $q$ element jobs and no dummy job, or exactly $p$ dummy jobs and no element job.

Significance

The result. Theorems 6 and 7 together say exactly which two-valued restrictions of $R\,\|\,C_{\max}$ are tractable. Up to scaling, the polynomial case is $\{1,2\}$ , and every other pair $\{p,q\}$ with $p<q$ is NP-hard. Theorem 4 is the base case. It also yields Corollary 1 of the paper: no polynomial $\rho$ -approximation with $\rho<4/3$ exists unless P = NP. Reductions of this "no idle time" kind are a standard template for hardness of restricted-assignment and two-value scheduling, a line still active in the study of the restricted assignment problem and of the "graph balancing" special case.

Formalizing it. The result is proved, in two short paragraphs. The proof leaves to the reader the construction of the schedule from a matching and the "easy number theoretic argument" behind the converse, and both become explicit here. The development also produces reusable pieces: a $q$ -dimensional matching definition over an arbitrary family of $q$ -sets, and two reduction instances built on the published load and makespan of MatousekLP.Scheduling.Schedule. To our knowledge no machine-checked proof of these reductions exists.

Difficulty

The forward direction is a direct construction. The converse is where care is needed. A schedule with makespan at most $pq$ may a priori place an element job on a machine whose tuple does not contain it, at length $q$ , and may mix element and dummy jobs on one machine. Looking at one machine at a time does not exclude either: a single machine can carry such a mixed load below $pq$ . What excludes them is a property of the whole schedule together with the arithmetic of $p$ and $q$ . The hypotheses are sharp for this step: for $p>q$ element jobs are cheaper on foreign machines, and for $\gcd(p,q)>1$ a load $ap+bq=pq$ with $a,b>0$ becomes possible.

Formalization scope

Model. Machines are Fin m. Schedules are maps from jobs to machines. Load and makespan are those of the published MatousekLP.Scheduling.Schedule, with natural-number processing times cast to $\mathbb R$ . The jobs are enumerated as Fin (q * n + p * (m - n)) (Theorem 7) and Fin (3 * n + (m - n)) (Theorem 4), element jobs first, through finSumFinEquiv.
Ground set and family. The ground set is Fin (q * n) and the family is indexed by machines, so repeated tuples are allowed. The $q$ -partite structure of $q$ -dimensional matching is not imposed: the reduction does not use it, and statements over all families of $q$ -sets contain the $q$ -partite case. Theorem 4 keeps the tripartite structure, with triples of indices in Fin n × Fin n × Fin n.
Threshold. The thresholds are exactly $pq$ and $3$ , with "makespan at most".
Complexity wording not formalized. "NP-hard" (Theorem 7) and "NP-complete" (Theorem 4) are not formalized: membership in NP, polynomial size of the reductions, and the hardness of the matching problems are not stated. What is stated is the equivalence each reduction establishes.
Hypotheses. Theorem 7's goal assumes $0<p<q$ , $\gcd(p,q)=1$ and $|S_i|=q$ . The paper's general case $\gcd(p,q)=g>1$ is its stated "without loss of generality": divide all times by $g$ , which divides every makespan by $g$ . It is not part of the formal statement. The paper's hypothesis $2p\ne q$ is dropped because the reduction does not use it. With coprime $p<q$ it excludes only $(p,q)=(1,2)$ , where the equivalence still holds but the source problem is bipartite matching. The formal goal is therefore stronger than the paper's.
Edge cases. For $m<n$ , natural-number subtraction gives no dummy jobs; both sides of each equivalence are false when $n\ge1$ . This stands in for the paper's "trivial 'no' instance". For $n=0$ the empty family is a matching and the dummy jobs fill the machines exactly.
No trivialization. The goal is an equivalence about a constructed instance whose processing times are given by explicit definitions. Neither side is assumed, the schedule is quantified over all maps from jobs to machines, and the instance is not a free parameter pinned by hypotheses.
Welcome contributions. Besides the milestones: counting lemmas relating a machine's load to the numbers of jobs of each length on it, and lemmas on the makespan of MatousekLP.Scheduling.Schedule (it bounds every load; it is attained when $m\ge1$ ), which are reusable across scheduling reductions.

Selected references

J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Amsterdam, 1987 (the version formalized here); journal version in Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem SP1).
R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3 (the schedule, load and makespan definitions reused here). https://doi.org/10.1007/978-3-540-30717-4

7 thms1 active userReviewed

Linear Optimization Operations Research Statistics·Captain: mikedeng1

Optimal Estimation of Executive Compensation by Linear Programming I: Least Absolute Deviations under Ranking Constraints Equal a Linear ProgramResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Equivalence of the two programs

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

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

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

Supporting claims and numerical result

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

5 thms1 active userReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Assortment Optimization under Variants of the Nested Logit Model 6: For δ > 1, the Powers-of-δ LP Optimum Scaled by (δ^(2γ̄+1), δ^(γ̄+1)) Is Feasible for the Full LPResearch Paper

Motivation

Assortment optimization asks which products a retailer should offer when customers choose among the offered products according to a probabilistic choice model, so as to maximize expected revenue. Under the nested logit model the products are grouped into nests: a customer first picks a nest, then a product inside it. The model is the standard relaxation of the independence of irrelevant alternatives property of the multinomial logit, and it is used throughout revenue management and transportation demand modelling.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) classify the complexity of the assortment problem under four variants of the nested logit model, according to whether the dissimilarity parameters are at most one and whether a customer who picks a nest always buys there. The problem is NP-hard as soon as some dissimilarity parameter exceeds one (their Theorem 5), and also when the nests have positive no-purchase weights (Theorem 8), so for the general variant approximation is the realistic aim. §6.2 of the paper gives an approximation scheme for the most general variant: for any $\delta > 1$ it restricts each nest to a short list of candidate assortments indexed by the powers of $\delta$ , solves a small linear program, and loses at most a factor $\delta^{2\bar\gamma+1}$ of the optimal revenue. This mission formalizes the guarantee behind that scheme, Theorem 12.

Setting

There are nests $M$ and products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$ ; the products are ordered so that $r_{i1} \ge \dots \ge r_{in}$ . Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$ , and $v_0 \ge 0$ is the weight of leaving without choosing a nest. Offering $S_i \subseteq N$ in nest $i$ gives

V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j \in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \qquad \Pi(S_1, \dots, S_m) = \frac{\sum_i V_i(S_i)^{\gamma_i} R_i(S_i)}{v_0 + \sum_i V_i(S_i)^{\gamma_i}}.

The optimal expected revenue $Z^* = \max \Pi$ is the optimal value of the linear program (3): minimize $x$ subject to $v_0 x \ge \sum_i y_i$ and $y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - x)$ for every nest $i$ and every $S_i \subseteq N$ . Problem (4) keeps the second family of constraints only for a candidate collection of assortments in each nest.

Let $\bar\gamma = \max_i \gamma_i$ , assumed $> 1$ throughout §6, and fix $\delta > 1$ . Put $v^L_i = v_{i0} + \min_j v_{ij}$ , $v^U_i = v_{i0} + \sum_j v_{ij}$ , and let $l^L_i$ , $l^U_i$ be the least integers with $\delta^{l} \ge v^L_i$ , $\delta^l \ge v^U_i$ . For each level $l = l^L_i, \dots, l^U_i$ , problem (15) maximizes $\sum_{j \in S} r_{ij} v_{ij}$ over the assortments with $\delta^{l-1} \le V_i(S) \le \delta^l$ ; its value is $\hat G_{il}$ . An assortment $\hat S_{il}$ is feasible for (15) and satisfies $\delta \sum_{j \in \hat S_{il}} r_{ij} v_{ij} \ge \hat G_{il}$ . The candidate collection of nest $i$ is $\{\hat S_{il} : l = l^L_i, \dots, l^U_i\} \cup \{\emptyset\}$ .

Formalization targets

Goal: Theorem 12 (p. 28)

If $(\hat x, \hat y)$ is an optimal solution of problem (4) over the candidate collections $\{\hat S_{il}\} \cup \{\emptyset\}$ , then

\big(\delta^{2\bar\gamma+1}\hat x,\ \delta^{\bar\gamma+1}\hat y\big) \text{ is feasible for problem (3).}

Milestones (Appendix A.6, pp. 53–54)

$\hat x \ge 0$ .
Every nonempty assortment of nest $i$ lies in some level $l^L_i \le l \le l^U_i$ .
If $\delta^{l-1} \le a \le \delta^l$ , then $a^{\gamma-1} \ge (\delta^l)^{\gamma-1}\delta^{-[\gamma-1]^+}$ .
Under the same hypothesis, $(\delta^l)^{\gamma-1} \ge \delta^{-[1-\gamma]^+} a^{\gamma-1}$ .
$\delta^{\bar\gamma}\delta^{-[\gamma_i-1]^+}\delta^{-[1-\gamma_i]^+} \ge 1$ and $\delta^{\bar\gamma+\gamma_i+1} \le \delta^{2\bar\gamma+1}$ .
The scaled pair satisfies $\delta^{\bar\gamma+1}\hat y_i \ge V_i(S_i)^{\gamma_i}(R_i(S_i) - \delta^{2\bar\gamma+1}\hat x)$ for every nonempty $S_i$ .
The same inequality for $S_i = \emptyset$ .

Companions

The guarantee stated after Theorem 12: with $v_0 > 0$ , the assortment assembled from the candidates solving problem (5) earns at least $Z^*/\delta^{2\bar\gamma+1}$ .
Proposition 15 (p. 51): when (15) is feasible, one of the explicit assortments $\hat S(J_L, J_S)$ , built from at most $q = \lceil \delta/(\delta-1)\rceil$ large and at most $q$ small products by a greedy continuous knapsack, is feasible for (15) and within a factor $\delta$ of $\hat G_{il}$ .
The count $l^U_i - l^L_i \le 1 + \log_\delta(v^U_i/v^L_i)$ (p. 28).

Significance

Theorem 12 is the analytical half of the approximation scheme. Together with the paper's Theorem 1 it shows that a linear program with $1 + m$ variables and at most $1 + m(2 + \log_\delta(v^U_i/v^L_i))$ constraints yields an assortment within a factor $\delta^{2\bar\gamma+1}$ of the optimum, for the most general variant, which is NP-hard, and Proposition 15 makes the candidate assortments computable. Letting $\delta \downarrow 1$ trades accuracy for running time, so the result is the paper's answer to how well the general problem can be approximated by this LP approach.

The result is proved in the paper; the work here is to formalize the known proof. To the best of a search of the Prove2Me library (local index and platform mirror, October 2026), no nested logit approximation result, and no knapsack lemma matching Proposition 15, has a machine-checked statement or proof. The definitions of the shared model (the instance, $V_i$ , $R_i$ , $\Pi$ , the linear programs (3) and (4)) are common to the six missions of this series.

Difficulty

The obvious argument compares an arbitrary assortment $S_i$ with the candidate of its level and uses the candidate's constraint in (4). This fails as a direct comparison because the nest weight $V_i(\cdot)^{\gamma_i}$ enters twice with different exponents, $\gamma_i - 1$ in front of the revenue and $\gamma_i$ in front of $\hat x$ , and within one level $V_i$ may vary by a factor $\delta$ . When $\gamma_i > 1$ and when $\gamma_i \le 1$ the monotonicity of $t \mapsto t^{\gamma_i - 1}$ goes in opposite directions, so the losses must be tracked separately by $[\gamma_i - 1]^+$ and $[1 - \gamma_i]^+$ , and they are absorbed by the common factor $\delta^{\bar\gamma}$ only because $\bar\gamma > 1$ . The other half, Proposition 15, concerns a knapsack with both a lower and an upper bound on the total weight, where a feasible solution must be produced as well as a good objective value.

Formalization scope

Products are Fin n ( $0, \dots, n-1$ for $1, \dots, n$ ), nests a finite type, powers $V^{\gamma}$ real powers, and $x/0 = 0$ , which gives $R_i(\emptyset) = 0$ . The shared model carries the standing assumptions of §1 with the disclosed pins $v_{ij} > 0$ , $r_{ij} \ge 0$ and $\gamma_i > 0$ (the page allows $\gamma_i = 0$ and zero-weight padding products, under which its convention $0^{\gamma_i} = 0$ and its proofs fail). Every statement of the mission also assumes $n \ge 1$ (for $v^L_i$ ), $\bar\gamma$ is the greatest of the $\gamma_i$ (so at least one nest exists) with $\bar\gamma > 1$ , and $\delta > 1$ . Integer powers $\delta^l$ are zpow, and $l^L_i$ , $l^U_i$ are written $\lceil \log_\delta v^L_i\rceil$ , $\lceil \log_\delta v^U_i\rceil$ , which equal the minima of the paper. An optimal solution of (4) is a feasible pair whose $x$ is minimal among feasible pairs. The companion guarantee adds $v_0 > 0$ , the pin of Theorem 1. In Proposition 15 the capacity row of (33) includes $v_0$ , correcting a printed slip, and the running-time claim is not stated.

The assortments $\hat S_{il}$ enter Theorem 12 as an arbitrary family with the two properties of p. 28; the theorem is stated for every such family. A level at which (15) has no feasible assortment imposes nothing on $\hat S_{il}$ , as on the page. Requiring $\hat S_{il}$ to lie in its level unconditionally would make the hypothesis unsatisfiable for most instances and the goal vacuous; that encoding, and any goal that assumes displays (34)–(36) or the exponent bounds, is ruled out.

Contributions welcome: proofs of the real-power milestones (3)–(5), which are self-contained, of the two cases (6)–(7), and of Proposition 15, whose fractional knapsack lemma (the greedy solution of a continuous knapsack sorted by ratio is optimal) is reusable beyond this mission.

Selected references

J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014; cited from the revised manuscript of June 18, 2013. https://doi.org/10.1287/opre.2014.1256
A. M. Frieze, M. R. B. Clarke, Approximation algorithms for the m-dimensional 0–1 knapsack problem: worst-case and probabilistic analyses, European Journal of Operational Research 15(1), 1984. (cited on p. 50 of the paper for the continuous knapsack (33); link not verified here)
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

The Bargaining Problem: The Nash Product Maximizer Is the Unique Solution Satisfying Invariance, Symmetry, IIA and Pareto EfficiencyResearch Paper

Motivation

Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).

Timeline:

1944. von Neumann and Morgenstern axiomatize expected utility. A utility is determined up to a positive affine transformation $au+b$ . Nash quotes this on p. 157.
1950. Nash introduces the two-person bargaining problem and the axioms of Pareto efficiency, independence of irrelevant alternatives and symmetry, the solution being invariant under the choice of utility scales. He proves that they force the maximizer of the product $u_1u_2$ (doi:10.2307/1907266).
1953. Nash's Two-Person Cooperative Games adds the threat game that fixes the disagreement point.
1975. Kalai and Smorodinsky replace independence of irrelevant alternatives by monotonicity and obtain a different solution.
1986. Binmore, Rubinstein and Wolinsky show that the Nash solution is the limit of equilibria of alternating-offers bargaining as the time between offers vanishes.

Setting

A bargaining problem is a pair $\langle S,d\rangle$ . Here $S\subseteq\mathbb R^2$ is the set of utility pairs $u=(u_1,u_2)$ the two players can reach by agreement, including lotteries over agreements. $d\in S$ is the disagreement point, the utilities of no cooperation. As in the platform goal, $S$ is compact and convex, and some $s\in S$ has $s_1>d_1$ and $s_2>d_2$ (both individuals could gain). Write $\mathcal B$ for the set of such pairs.

A bargaining solution is a map $g$ from $\mathcal B$ to $\mathbb R^2$ . Nash requires:

Selection. $g(S,d)\in S$ .
PAR (Nash's assumption 6). If $s,t\in S$ and $t$ is strictly better than $s$ for both players, then $g(S,d)\neq s$ .
IIA (assumption 7). If $S\subseteq T$ and $g(T,d)\in S$ , then $g(S,d)=g(T,d)$ .
SYM (assumption 8). If $d_1=d_2$ and $S$ is symmetric in the line $u_1=u_2$ , then $g(S,d)$ lies on that line.
INV. For $L(s)=(\alpha_1s_1+\beta_1,\ \alpha_2s_2+\beta_2)$ with $\alpha_1,\alpha_2>0$ , $g(L(S),L(d))=L(g(S,d))$ .

The paper has no separate INV axiom. It normalizes the disagreement utility to $0$ and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.

Formalization targets

Goal

The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by Nickrobbins95 and currently Open. This mission references it and does not restate it. It asserts that there is a solution $f$ such that a solution $g$ satisfies selection, INV, SYM, IIA and PAR if and only if $g=f$ , and that for every $\langle S,d\rangle\in\mathcal B$

f(S,d)\ge d,\qquad (s_1-d_1)(s_2-d_2)<(f_1-d_1)(f_2-d_2)\ \text{ for all } s\in S,\ s\ge d,\ s\neq f(S,d).

Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.

Milestones

On a compact convex $S\ni(0,0)$ that contains a point where both players gain, $u_1u_2$ has exactly one strict maximizer $p$ in the closed first quadrant, and $p_1,p_2>0$ .
Multiplying the utilities by positive constants maps the maximizer to the maximizer, so $p$ may be moved to $(1,1)$ .
If $S$ is convex and $(1,1)$ maximizes $u_1u_2$ , then $u_1+u_2\le2$ on all of $S$ .
A compact $S$ under that line lies in a square $Q_h=\{2-2h\le u_1+u_2\le2,\ |u_1-u_2|\le h\}$ .
$(1,1)$ is the only point of $Q_h$ on the diagonal that no point of $Q_h$ strictly dominates.
Necessity. Under the five conditions, $g(S,d)$ is the strict maximizer of $(s_1-d_1)(s_2-d_2)$ over $S\cap\{s\ge d\}$ .

Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex $(12,5)$ reached by exactly one exchange, and trade with money, where the solution gives equal money profits.

Significance

The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.

The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.

Difficulty

Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class $\mathcal B$ , and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of $S$ under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality $d=0$ and $p=(1,1)$ ". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of $d$ inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.

Formalization scope

Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work at $d=(0,0)$ , the paper's normalization. Milestone 6 has a general $d$ and the goal's encoding. Milestones 1–5 make the following readings explicit:

"First quadrant" is the closed quadrant $u_1\ge0,\ u_2\ge0$ .
"The point where $u_1u_2$ is maximized" is the strict maximizer over $S$ in that quadrant, in the goal's form. Milestone 1 also states $p_1,p_2>0$ , which follows from the point where both gain (p. 158).
Milestone 3's hypothesis is the weak maximum $s_1s_2\le1$ . Its conclusion covers every point of $S$ , not only first-quadrant points.
The square is the explicit set $Q_h$ . Its compactness, convexity and literal symmetry $(a,b)\in Q_h\iff(b,a)\in Q_h$ are part of milestone 4's conclusion.
"Satisfying assumptions (6) and (8)" in the square means lying on $u_1=u_2$ and being strictly dominated by no point of the square.

Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given $g$ . It does not restate the goal: it has no existence claim and no "if and only if".

Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of $u_1u_2=0$ . The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class $\mathcal B$ , which is nonempty.

The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.

Related platform work treats other bargaining models. These are Rubinstein's alternating-offers game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction (ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.

Selected references

J. F. Nash, Jr., The Bargaining Problem, Econometrica 18(2), 155–162, 1950. doi:10.2307/1907266
J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
J. F. Nash, Jr., Two-Person Cooperative Games, Econometrica 21(1), 128–140, 1953. doi:10.2307/1906951
E. Kalai, M. Smorodinsky, Other Solutions to Nash's Bargaining Problem, Econometrica 43(3), 513–518, 1975. doi:10.2307/1914280
K. Binmore, A. Rubinstein, A. Wolinsky, The Nash Bargaining Solution in Economic Modelling, RAND Journal of Economics 17(2), 176–188, 1986. doi:10.2307/2555382
M. J. Osborne, A. Rubinstein, Bargaining and Markets, Academic Press, 1990, Theorem 2.3.

10 thms3 active usersReviewed

The OR Formalization Drive

Missions

Supply Chain Coordination with Contracts IV: Competing Newsvendors with Proportional Allocation Have a Unique Equilibrium, and a Coordinating Buy-Back Gives the Supplier ((p(n − 1) + b)/(pn))Π(q°)Textbook

Why competing retailers change the contracting problem

The proportional allocation model

Formalization targets

Goal: the coordinating buy-back contract (pp. 51–53)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

Milestones: the four yes-instance equivalences

Significance

Difficulty

Formalization scope

Selected references

An Optimal Algorithm for On-line Bipartite Matching 1: RANKING Finds a Matching of Expected Size at Least n(1 − 1/e) − o(n) on Every Graph with a Perfect MatchingResearch Paper

Motivation

Setting

Formalization targets

RANKING guarantee

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts V: With Market-Clearing Prices the Best Wholesale Price Earns θ/(2(1 + θ)) or θ/8, Below the (1 + θ)/8 a Full-Refund Buy-Back AttainsTextbook

Motivation

Setting

Formalization targets

Goal (pp. 55, 57)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts VII: In the Single-Location Base-Stock Model the Transfers t_I = (1 − λ)h_r, t_B = β_r − λβ Make the Retailer's Cost λc(s_r)Textbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Integer Programming with a Fixed Number of Variables 1: If B(p,r) ⊂ τK ⊂ B(p,R) with R/r ≤ c₁ and τK Misses the Lattice, Fewer Than 1 + c₁c₂√n Lattice Hyperplanes H + kbₙ Meet B(p,R)Research Paper

Motivation

Setting

Formalization targets

Goal (§1, p. 541)

Milestones, in the order the paper uses them

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4(d)

The equivalence and its claims

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts VI: With a Forecast Update, Buy-Back Terms with w₁ − w₂ + λc₂ = λc₁ Give the Retailer λΩ₁(q₁) and a Lower Period-2 Margin w₂ − c₂ < w₁ − c₁Textbook

Motivation

Setting

Formalization targets

Goal: the buy back contract coordinates

Milestones

Significance

Difficulty

Formalization scope

Selected references

Supply Chain Coordination with Contracts VIII: In the Two-Location Base-Stock Model the Linear Transfers (39)–(41) Make the Optimal Base Stocks the Unique Nash EquilibriumTextbook