All missions

Motivation

Minimizing a submodular set function is one of the central tractable problems of combinatorial optimization. Minimum cuts in graphs and hypergraphs, matroid intersection and partition, the rank of a matroid union, and many problems in facility location, image segmentation and machine learning are special cases or subroutines of it. The question is algorithmic: given only a value oracle for $f$, find a set $U$ with $f(U) = \min_W f(W)$ using a number of operations bounded by a polynomial in $|V|$ alone, independent of the size of the values of $f$ (strongly polynomial).

Timeline.

• 1981. Grötschel, Lovász and Schrijver showed with the ellipsoid method that submodular functions can be minimized in strongly polynomial time (Combinatorica 1, 1981). The method is not combinatorial.
• 1985. Cunningham gave a combinatorial pseudo-polynomial algorithm for submodular function minimization (Combinatorica 5, 1985).
• 1999–2000. Two combinatorial strongly polynomial algorithms appeared independently: Iwata, Fleischer and Fujishige (J. ACM 48, 2001), and Schrijver, the paper of this mission (J. Combin. Theory Ser. B 80, 2000).

Schrijver's algorithm is the one usually taught. Its proof uses only the greedy vectors of $f$, a reachability digraph and a lexicographic potential.

Setting

Let $V = \{1,\dots,n\}$ and let $f$ be a real function on all subsets of $V$ that is submodular:

normalized so that $f(\emptyset)=0$. For $x \in \mathbb R^V$ and $U \subseteq V$ write $x(U) = \sum_{v\in U} x(v)$. The base polytope is $B_f = \{x \in \mathbb R^V : x(U) \le f(U)\ \forall U,\ x(V) = f(V)\}$.

For a total order $\prec$ on $V$ let $v_\prec = \{u : u \prec v\}$. The greedy vector of $\prec$ is $h^\prec(v) = f(v_\prec\cup\{v\}) - f(v_\prec)$. A lower ideal of $\prec$ is a set closed under taking $\prec$-smaller elements. The interval $(s,t]_\prec$ is $\{v : s \prec v \preceq t\}$. For $s \prec u$, the order $\prec^{s,u}$ is obtained from $\prec$ by moving $u$ to the position just before $s$. The vector $\chi^u$ is the incidence vector of $u$.

The algorithm keeps a point $x = \lambda_1 h^{\prec_1} + \dots + \lambda_k h^{\prec_k}$ with $\lambda_i > 0$ and $\sum_i \lambda_i = 1$; initially $x = h^\prec$ for an arbitrary order. It forms the digraph $D = (V, A)$, where $A = \{(u,v) : u \prec_i v \text{ for some } i\}$, and the sets $P = \{x > 0\}$ and $N = \{x < 0\}$.

• Case 1: $D$ has no path from $P$ to $N$. The algorithm returns the set $U$ of vertices that can reach $N$.
• Case 2: there is such a path. Let $d(v)$ be the distance from $P$ to $v$ in $D$. The algorithm picks $t \in N$ maximizing $(d(t), t)$, then the largest $s$ with $(s,t)\in A$ and $d(s) = d(t)-1$, then an order $\prec_1$ maximizing $|(s,t]_{\prec_1}|$.
  • It finds $\delta \ge 0$ with $h^{\prec_1} + \delta(\chi^t - \chi^s)$ a convex combination of the $h^{\prec_1^{s,u}}$, $u \in (s,t]_{\prec_1}$.
  • It moves $x$ toward $y = x + \lambda_1\delta(\chi^t-\chi^s)$ as far as $x(t) \le 0$ allows.
  • It reduces the new convex decomposition to at most $|V|$ terms, dropping $\prec_1$ if $x'(t) < 0$.

Formalization targets

Goal: correctness, well-definedness and the iteration bound

For every submodular $f$ with $f(\emptyset)=0$:

Part (iii) is the opening claim of §5 (p. 352), and part (i) is display (16) (p. 351). Part (ii) states that the description of §4 can always be carried out, and it keeps (iii) from holding vacuously.

Milestones

In order: the diminishing-returns inequality (9); $h^\prec(U) = f(U)$ on lower ideals and $h^\prec \in B_f$ (§2); the comparison (8) of $h^{\prec^{s,u}}$ with $h^\prec$; the subroutine (12); the Case 1 certificate (16); existence of a Case 2 iteration (§4, p. 352); the location (22) of new arcs; monotonicity (20) of distances; and the lexicographic decrease (21) of $(d(t), t, s, \alpha, \beta)$ while $d$ stays fixed.

Significance

The result. The theorem gives a submodular minimizer after a number of iterations bounded by a polynomial in $|V|$. Each iteration makes polynomially many oracle calls and arithmetic operations, so the algorithm is strongly polynomial. The same exchange-and-potential scheme underlies later improvements (Fleischer–Iwata's push-relabel variant, Iwata–Orlin, Orlin's $O(n^5)$ bound). Section 6 of the paper, the companion mission, transfers the result to submodular functions on ring families.

Formalizing it. The result is proved and has been in textbooks for twenty years. It has no machine-checked proof that we know of, in Lean or elsewhere, and Mathlib has no submodular minimization. A complete development yields a verified correctness and termination proof for a nontrivial combinatorial algorithm on the base polytope. It also yields reusable facts about greedy vectors and lower ideals, and a worked example of a lexicographic-potential termination argument.

Difficulty

Correctness (16) is short once $h^\prec(U) = f(U)$ on lower ideals is available. The difficulty is termination. A single iteration can increase $x$ at $t$ and decrease it at $s$, and it adds new orders and so new arcs. Neither $|N|$ nor $x(N)$ need improve monotonically, and the obvious potentials fail. The argument needs the precise structure of the new arcs (22): every new arc lies inside the interval $[s,t]$ of $\prec_1$, and that gives both the monotonicity of distances (20) and the strict lexicographic decrease (21). The choice rule for $t$ and $s$ ("largest") is what makes (21) hold. An arbitrary choice can cycle. Well-definedness also takes work: it combines (12) with a Carathéodory reduction over the hyperplane $x(V) = f(V)$.

Formalization scope

• Ground set and values. $V$ is Fin n and subsets are Finset (Fin n). Values are real; the paper allows any ordered field. "Largest" in the choice of $t$ and $s$ is the order of Fin n.
• Orders and states. A total order is a permutation $\sigma$ read as a position map: $u \prec v$ iff $\sigma(u) < \sigma(v)$. The order $\prec^{s,u}$ is characterized relationally (IsMoved). A state is a list of (order, weight) pairs.
• Distances. Distances take values in $\mathbb N \cup \{\infty\}$, with $\infty$ for unreachable vertices.
• Standing assumptions. Submodularity (the platform definition NonmonotoneSubmod.Shared.Submodular) and $f(\emptyset) = 0$ are the paper's standing assumptions of §2 and §4. Milestones that do not need $f(\emptyset)=0$ omit it.
• Iterations as a relation. An iteration is a relation Step that admits every choice the paper leaves open: any subroutine output $\delta$, any maximizing index, and any Carathéodory reduction. The reduced decomposition may only use orders $\prec_i$ ($i \ne 1$), each $\prec_1^{s,u}$ at most once, and $\prec_1$ only when $x'(t) = 0$.
• Not formalized. The value oracle, "strongly polynomial time" and the number of oracle calls are not formalized, because there is no machine model. Only the iteration count is.
• No trivial reading. A Step relation that is never satisfiable would make the bound vacuous. Part (ii) of the goal rules this out, and the goal does not mention $d$, $\alpha$, $\beta$ or the matrix of §3.
• Contributions welcome. Proofs of the milestones, general lemmas on greedy vectors and lower ideals (reusable for any base-polytope development), and a Carathéodory lemma for convex combinations in an affine hyperplane.

Selected references

• A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000) 346–355. https://doi.org/10.1006/jctb.2000.1989
• S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001) 761–777. https://doi.org/10.1145/502090.502096
• M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
• W. H. Cunningham, On submodular function minimization, Combinatorica 5 (1985) 185–192. https://doi.org/10.1007/BF02579361
• J. B. Orlin, A faster strongly polynomial time algorithm for submodular function minimization, Math. Program. 118 (2009) 237–251. https://doi.org/10.1007/s10107-007-0189-2

Motivation

Most stochastic programs cannot be solved as stated, because the objective is an expectation over a distribution that is high-dimensional, continuous or known only through a simulator. The standard remedy is the sample average approximation (SAA), also called the Monte Carlo or sample-path method: draw an i.i.d. sample, replace the expectation by the sample mean, and solve the resulting deterministic problem. The method is the workhorse of two-stage stochastic programming, and its statistical behaviour decides how large a sample a practitioner must draw.

For smooth problems with a unique optimum, the classical theory says the SAA solution converges at rate $N^{-1/2}$ and is asymptotically normal. Shapiro and Homem-de-Mello (SIAM J. Optim. 11 (2000)) observed that two-stage linear programs with finitely many scenarios behave quite differently: their optimal solutions are typically sharp, the objective grows linearly away from the minimizer, and then the SAA problem does not just approach the true solution but returns it exactly once the sample is large enough. This mission formalizes that first observation, Theorem 2.1 of the paper. Its sequels in the same series show that the probability of failure decays exponentially in $N$ (mission 2) and extend the picture to multiple optimal solutions in the finite polyhedral case (mission 3).

Setting

Let $P$ be a probability measure on a sample space $(\Omega,\mathcal F)$, let $\Theta\subseteq\mathbb R^m$ be a set of feasible decisions, and let $h:\mathbb R^m\times\Omega\to\mathbb R$ be a cost function. The true problem (1.1) is

Let $\omega^1,\omega^2,\dots$ be an i.i.d. sequence of random elements of $\Omega$ with law $P$, defined on some probability space $(S,Q)$. The approximating problem (1.2) uses the first $N$ of them:

For a function $g$ on $\mathbb R^m$ write $\operatorname{argmin}_\Theta g = \{x\in\Theta : g(x)\le g(y)\ \forall y\in\Theta\}$; the optimal set of the true problem is $A=\operatorname{argmin}_\Theta f$. The directional derivative of $g$ at $x$ in direction $d$ is $g'(x,d)=\lim_{t\downarrow0}(g(x+td)-g(x))/t$; for the cost of a single scenario it is written $h'_\omega(x,d)$. The tangent cone $T_\Theta(\bar x)$ to a convex set $\Theta$ at $\bar x\in\Theta$ is the closure of $\{t(x-\bar x): t\ge0,\ x\in\Theta\}$.

Assumption (A). The true problem has a unique optimal solution $\bar x$, i.e. $A=\{\bar x\}$, and there is $c>0$ with

An optimal solution with this linear growth is a sharp minimum.

A statement holds w.p.1 for $N$ large enough if for $Q$-almost every sample path there is $N^*$, depending on the path, such that it holds for every $N\ge N^*$.

Formalization targets

Goal: Theorem 2.1 (p. 5)

Suppose (i) $h(\cdot,\omega)$ is convex for every $\omega$; (ii) $f$ is well defined and finite valued; (iii) $\Theta$ is closed and convex; (iv) Assumption (A) holds. Then w.p.1 for $N$ large enough

that is, the approximating problem has a unique optimal solution $\hat x_N$ and $\hat x_N=\bar x$.

Milestones

1. (A) ⇔ (2.3) (p. 4): for a convex problem, $\bar x$ is a sharp unique minimum iff $f'(\bar x,d)>0$ for all $d\in T_\Theta(\bar x)\setminus\{0\}$.
2. Uniform positivity (p. 4): (2.3) implies $f'(\bar x,d)\ge\varepsilon\|d\|$ for some $\varepsilon>0$ and all $d\in T_\Theta(\bar x)$.
3. Proposition 2.2 (2.5) (p. 5): $f'(x,d)=\mathbb E_P\{h'_\omega(x,d)\}$.
4. (2.10) (p. 5): $\hat f'_N(x,d)=N^{-1}\sum_{j=1}^N h'_{\omega^j}(x,d)$.
5. Proposition 2.2 (2.6) (p. 5): $\lim_N \sup_{\|d\|\le1}|f'(x,d)-\hat f'_N(x,d)|=0$ w.p.1.
6. Proposition 2.2 (2.7) (p. 5): $\lim_N\mathcal H(\partial\hat f_N(x),\partial f(x))=0$ w.p.1, with $\mathcal H$ the Hausdorff distance.
7. (2.11) (p. 6): w.p.1 for $N$ large enough, $\hat f'_N(\bar x,d)>0$ for all $d\in T_\Theta(\bar x)\cap S^{m-1}$.

Significance

The result. Theorem 2.1 says that for convex stochastic programs with a sharp optimum, SAA is not an estimator with sampling error in the usual sense: almost every sample path eventually produces the true solution itself. This is the qualitative statement behind the paper's main quantitative result (Theorem 3.1, mission 2 of this series), that the probability of not obtaining the exact solution decays like $e^{-\beta N}$. Together they explain why, in two-stage linear programs with finitely many scenarios, modest sample sizes often recover the optimal first-stage decision exactly, a phenomenon the paper documents numerically. The proposition on directional derivatives (Proposition 2.2) is of independent use: it is the almost-sure uniform convergence of first-order information of a sample average, which recurs in the asymptotic analysis of SAA estimators.

Formalizing it. The theorem is proved in the paper; nothing here is open. Machine-checked SAA theory is thin: the existing platform material treats uniform convergence of the objective on compact sets, not directional derivatives or exactness at sharp minima. A complete development supplies, on top of Mathlib, the strong law of large numbers applied to directional derivatives of convex integrands, the passage from pointwise to uniform convergence for convex functions, and the characterization of sharp minima by directional derivatives on the tangent cone. Each of these is reusable well beyond this paper.

Difficulty

The obvious argument fails at the step from convergence to exactness. Strong consistency of SAA ($\hat x_N\to\bar x$ w.p.1) says nothing about $\hat x_N$ equalling $\bar x$; for a smooth objective it never does. Exactness has to come from a first-order condition at $\bar x$ that holds with a margin, and that margin must be transferred to $\hat f_N$ uniformly over all tangent directions at once, not one direction at a time, since there are uncountably many directions and each carries its own null set. The second difficulty is that $\hat f_N$ and $f$ are typically nonsmooth (piecewise linear in the motivating examples), so the first-order objects are one-sided directional derivatives, and differentiation under the integral sign, in its usual smooth form, does not apply to them.

Formalization scope

• $\mathbb R^m$ is EuclideanSpace ℝ (Fin m). The sample is one infinite i.i.d. sequence on a separate probability space $(S,Q)$: each $\omega^j$ is measurable with law $P$, and the family is mutually independent. $\hat f_N$ uses the first $N$ terms (0-based in Lean). "W.p.1 for $N$ large enough" is ∀ᵐ s ∂Q, ∀ᶠ N in atTop, …; a fresh sample for each $N$ is not used.
• Hypothesis (ii), "$f$ well defined and finite valued", is encoded as integrability of $h(x,\cdot)$ for every $x$ (a disclosed pin, which includes measurability).
• $f$ is the Bochner integral; directional derivatives are one-sided limits (limUnder along $t\downarrow0$), used only for convex finite functions, where the limits exist. Optimal sets are defined directly as argmin sets, without infima.
• The tangent cone is Mathlib's posTangentConeAt, the cone of limits of $c_n d_n$ with $c_n\ge0$; for convex $\Theta$ it is the closure of $\mathbb R_+(\Theta-\bar x)$. Mathlib's tangentConeAt ℝ, which allows negative scalings and is symmetric, is not the paper's cone and is not used.
• Supremum limits over the unit ball are stated as uniform convergence on the closed unit ball; the Hausdorff distance is the extended-valued Metric.hausdorffEDist. Subdifferentials use the published definition ShorNonsmooth.Subdiff.subdifferential.
• Uniqueness in the goal is the set equality $\operatorname{argmin}_\Theta\hat f_N=\{\bar x\}$; the weaker "$\bar x$ is optimal for (1.2)" is not the theorem. The goal's quantifier order is "almost surely, eventually in $N$"; "for each $N$, almost surely" is a different and false statement.
• Milestones 1 and 2 are stated for an arbitrary finite convex function, which covers both $f$ and $\hat f_N$.

Contributions welcome: proofs of any milestone; in particular the convex-analysis lemmas (milestones 1, 2 and 4) need no probability, and (2.5)–(2.6) need only Mathlib's strong law.

Selected references

• A. Shapiro and T. Homem-de-Mello, On the rate of convergence of optimal solutions of Monte Carlo approximations of stochastic programs, SIAM J. Optim. 11(1):70–86, 2000. https://doi.org/10.1137/S1052623498349541 (the mission cites the authors' preprint, Stochastic Programming E-Print Series).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorem 10.8, uniform convergence of convex functions). https://doi.org/10.1515/9781400873173
• J.-B. Hiriart-Urruty and C. Lemaréchal, Convex Analysis and Minimization Algorithms I, Springer, 1993 (Theorem V.3.3.8, support functions and Hausdorff distance). https://doi.org/10.1007/978-3-662-02796-7
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009 (Chapter 5, statistical inference for SAA). https://doi.org/10.1137/1.9780898718751

Motivation

The scheduling problem $R\,|\,r_j\,|\sum C_j$ asks for a nonpreemptive schedule of jobs on unrelated parallel machines, each job with a machine-dependent processing time and a release date, so that the total completion time is minimal. It is NP-hard, and the question that remains is how well it can be approximated in polynomial time. Positive results include the 2-approximation of Skutella (J. ACM 2001), based on a convex quadratic relaxation. This mission covers the negative side, from §7 of the same paper: the problem has no polynomial-time approximation scheme unless P = NP.

The standard route to such a statement is an L-reduction (Papadimitriou and Yannakakis 1991) from a problem already known to be MaxSNP-hard. MaxSNP-hard problems have no approximation scheme unless P = NP, by the PCP theorem (Arora et al. 1998).

Timeline.

• 1991: Papadimitriou and Yannakakis define MaxSNP and L-reductions, and show that MAX3SAT with a bounded number of occurrences per variable is MaxSNP-complete.
• 1998: Hoogeveen, Schuurman and Woeginger prove that $R\,|\,|\sum w_jC_j$ and $R\,|\,r_j\,|\sum C_j$ are MaxSNP-hard, by a reduction from a MaxSNP-hard variant of 3-dimensional matching.
• 2001: Skutella (§7, pp. 32–33) gives a shorter reduction from 3-OCCURRENCE MAX3SAT, the variant of MAX3SAT in which every variable occurs at most three times (MaxSNP-hard, see Ausiello et al. 1999, Corollary 8.15).

Setting

An instance $I$ of 3-OCCURRENCE MAX3SAT has $n$ variables and $m$ clauses. Each clause is a set of one to three literals (a variable $x$ or its negation $\neg x$), and each variable occurs at most three times in total. A truth assignment $t$ gives each variable the value true or false and satisfies a clause when one of the clause's literals is true. $\#(t)$ denotes the number of satisfied clauses, and $\mathrm{OPT}_{\mathrm{SAT}}(I)=\max_t \#(t)$.

The scheduling instance $R(I)$ has $n+m$ jobs and $2n$ machines.

• Every variable $x$ has a true machine and a false machine, and one v-job. The v-job is released at time $0$, has processing time $4$ on the two machines of $x$, and cannot run anywhere else.
• Every clause $c$ has one c-job, released at time $3$, with processing time $0$. It may run on the false machine of $x$ when $x$ occurs in $c$, on the true machine of $x$ when $\neg x$ occurs in $c$, and nowhere else.

A schedule $S$ gives every job $j$ a machine and a start time $S_j\ge r_j$, with no two jobs on one machine overlapping. Its value is the total completion time $\mathrm{VAL}(S)=\sum_j (S_j+p_j)$. The truth assignment $\mathrm{SAT}(S)$ sets $x$ true exactly when the v-job of $x$ runs on the true machine. $\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ is the minimum of $\mathrm{VAL}$ over feasible schedules.

Formalization targets

Goal: the L-reduction inequalities (Lemma 7.1 b) and the proof of Theorem 7.2, p. 33)

$R(I)$ has an optimal schedule $S_0$, and

for every feasible schedule $S$. These are the two conditions of an L-reduction, with constants $\alpha=32$ and $\beta=1$.

Milestones

1. Lemma 7.1 a) (p. 32): $\#(\mathrm{SAT}(S))\ge 4n+4m-\mathrm{VAL}(S)$ for every feasible $S$.
2. Lemma 7.1 b) (p. 33): $\mathrm{OPT}_{\mathrm{SCH}}(R(I))=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)$.
3. The two counting facts of the proof of Theorem 7.2: $\mathrm{OPT}_{\mathrm{SAT}}(I)\ge m/2$ and $n\le 3m$.
4. The first L-reduction condition: $\mathrm{OPT}_{\mathrm{SCH}}(R(I))\le 12m+4m\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I)$.
5. The second L-reduction condition: $\mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{OPT}_{\mathrm{SCH}}(R(I))$.

Significance

The result. The two inequalities are what an L-reduction requires. Combined with the MaxSNP-hardness of 3-OCCURRENCE MAX3SAT, they show that $R\,|\,r_j\,|\sum C_j$ is MaxSNP-hard (Theorem 7.2, due to Hoogeveen, Schuurman and Woeginger), and therefore has no polynomial-time approximation scheme unless P = NP. Together with the constant-factor algorithms of the earlier sections of the paper, this places the problem in APX but outside PTAS. The identity of Lemma 7.1 b) is exact, so the reduction transfers solutions in both directions with no loss beyond the affine shift $k\mapsto 4n+4m-k$.

Formalizing it. The result is proved, on paper, by both the 1998 and the 2001 reductions. As far as the platform's corpus shows, neither is machine-checked. This mission produces a checked version of the combinatorial core of Skutella's reduction: the exact relation between optimal schedules of $R(I)$ and optimal truth assignments of $I$, and the two L-reduction constants. A Lean model of 3-OCCURRENCE MAX3SAT and of nonpreemptive schedules with release dates and machine eligibility is a by-product.

Difficulty

The obvious argument is the paper's intuition: given a truth assignment, a c-job can start at time $3$ without conflicting with a v-job exactly when its clause is satisfied. That is not enough for Lemma 7.1 a), which concerns every feasible schedule. In an arbitrary schedule a v-job may be delayed so that c-jobs of unsatisfied clauses run before it on its machine, and v-jobs and c-jobs may start at arbitrary real times. To compare such a schedule with a normalized one, its total completion time has to be bounded from below by $4n+4m-\#(\mathrm{SAT}(S))$. The bound depends on the occurrence limit of three, which caps how many c-jobs can share a machine with a given v-job; without that limit Lemma 7.1 a) is false. Lemma 7.1 b) also needs the existence of an optimal schedule, which the paper takes for granted.

Formalization scope

Variables and clauses are Fin n and Fin m; here $n$ and $m$ count variables and clauses, not jobs and machines as in the rest of the paper. A literal is a pair (x, b) with b = true for $x$ and b = false for $\neg x$, and a clause is a Finset of literals. Jobs are Fin n ⊕ Fin m and machines Fin n × Bool. Infinite processing times are encoded by an eligibility relation. Start times are real numbers, and $\mathrm{VAL}$ is a real number; $\#$ and $\mathrm{OPT}_{\mathrm{SAT}}$ are natural numbers cast to the reals, so no natural-number subtraction occurs. $\mathrm{OPT}_{\mathrm{SCH}}$ is never a primitive: statements assert, or assume, a feasible schedule that is no worse than every feasible schedule.

Two conventions are fixed that the page leaves implicit:

• Every clause has between one and three literals. An empty clause would leave its c-job with no machine, so $R(I)$ would have no schedule, and "at least $m/2$" would fail.
• Every variable occurs at least once. The bound $n\le 3m$, and with it the constant $32$, needs this: a variable that occurs nowhere adds $4$ to $\mathrm{OPT}_{\mathrm{SCH}}$ and nothing to $\mathrm{OPT}_{\mathrm{SAT}}$.

Zero-length jobs need a precise non-overlap rule. Two distinct jobs on one machine must satisfy $S_j+p_j\le S_k$ or $S_k+p_k\le S_j$. Under this rule a c-job at time $3$ conflicts with a v-job running over $[0,4)$, but several c-jobs may share a start time. Reading jobs as half-open intervals $[S_j,S_j+p_j)$ would let a zero-length c-job sit inside a v-job, so every clause would count as satisfied: that formalization is ruled out.

Not formalized: MaxSNP, MaxSNP-hardness and Theorem 7.2's statement itself; the definition of an L-reduction as a pair of polynomial-time maps; the polynomial running time of $R$ and $\mathrm{SAT}$; the weighted variant for $R\,|\,|\sum w_jC_j$ in the last paragraph of §7, which the paper does not prove. Contributions are welcome on the counting facts, on a normal form for schedules of $R(I)$ (v-jobs at time $0$, c-jobs at time $3$ or $4$), and on the existence of optimal schedules.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2), 206–242, 2001. https://doi.org/10.1145/375827.375840
• J. A. Hoogeveen, P. Schuurman, G. J. Woeginger, Non-approximability results for scheduling problems with minsum criteria, IPCO 1998, LNCS 1412, 353–366. https://doi.org/10.1007/3-540-69346-7_27
• C. H. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
• G. Ausiello, P. Crescenzi, G. Gambosi, V. Kann, A. Marchetti-Spaccamela, M. Protasi, Complexity and Approximation, Springer, 1999. https://doi.org/10.1007/978-3-642-58412-1
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306

Motivation

A dispatcher assigns each arriving job to one of $n$ servers. Sending it to a uniformly random server is simple but produces long queues near capacity; sending it to the globally shortest queue requires full state information. The power of $d$ choices sits between the two: each job samples $d$ servers at random and joins the shortest of them. Mitzenmacher's analysis of this supermarket model (IEEE TPDS 12(10), 2001) together with the balls-into-bins result of Azar, Broder, Karlin and Upfal (SIAM J. Comput. 29(1), 1999), established that a second random choice changes the behaviour of the system qualitatively. The idea underlies load balancers, hashing schemes and distributed schedulers.

This mission formalizes the paper's quantitative statement of that improvement in heavy traffic, the regime where the arrival rate per server $\lambda$ approaches the service rate $1$.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$ with $0\le\lambda<1$, service times are exponential with mean $1$, and each customer joins the shortest of $d$ queues sampled uniformly with replacement. As $n\to\infty$ the fraction of queues with at least $i$ customers follows a deterministic limiting system with fixed point $\pi_i=\lambda^{(d^i-1)/(d-1)}$. Corollary 2 of the paper shows that, for $d\ge2$, the expected time a customer spends in that limiting system converges to

With a single choice the system is $n$ independent M/M/1 queues, and the expected time is

This mission takes these two formulas as its definitions; the limiting system itself and the convergence to $T_d(\lambda)$ are the subject of the companion mission (part I). The auxiliary function of Lemma 3 is

Throughout, $d\ge2$ is an integer and logarithms are natural.

Formalization targets

Goal: Theorem 4, limit clause (p. 1099)

Milestones, in the order the paper's argument uses them

1. The rewriting of $T_d$ (proof of Theorem 4): with $\lambda'=\lambda^{1/(d-1)}$ and $0<\lambda<1$,

2. The product identity (proof of Lemma 3): for $0\le\lambda<1$,

3. Lemma 3:

The goal is a statement about the shape of the growth, not a constant: it pins the leading behaviour $T_d(\lambda)\sim\log_d\frac{1}{1-\lambda}$.

Significance

Theorem 4 makes "exponential improvement" precise. With one choice the expected time grows like $\frac1{1-\lambda}$ as the load approaches capacity; with $d\ge2$ choices it grows like $\frac{\log\frac1{1-\lambda}}{\log d}$. It also quantifies the diminishing return of extra choices: going from $d=2$ to $d$ only divides the leading term by $\log_2 d$, while going from one choice to two changes its order. These constants are the benchmark against which later heavy-traffic analyses of join-the-shortest-of-$d$ policies are compared.

The result is proved in the paper (the limit clause; see Difficulty for the other clause). No machine-checked version is known to exist. The formalization yields a self-contained Lean development of the lacunary series $\sum_i x^{d^i}$ near $x=1$ and of the base-$d$ product identity, both of which are classical analytic facts with uses outside queueing (lacunary power series, digit expansions).

Difficulty

The obvious approach compares $\sum_i\lambda^{d^i}$ with an integral, but the terms are not monotone images of a smooth function of a continuous index in a way that controls the error uniformly as $\lambda\to1^-$: the number of terms close to $1$ grows like $\log_d\frac{1}{1-\lambda}$ and each of them contributes nearly $1$, so the error terms are of the same order as the quantity being measured. The difficulty is to obtain matching upper and lower bounds with constants tending to $1/\log d$, uniformly as $\lambda\to1^-$. Passing from Lemma 3 to Theorem 4 additionally requires controlling the change of variable $\lambda\mapsto\lambda^{1/(d-1)}$ inside the logarithm.

Theorem 4 as printed also contains a first clause, $T_d(\lambda)\le c_d\log T_1(\lambda)$ for all $\lambda\in[0,1]$. It is false as printed near $\lambda=0$: $T_d(\lambda)\ge1$ while $\log T_1(\lambda)\to0$. The paper does not prove it, and this mission does not pose it.

Formalization scope

• Representation. $\lambda$ is a real number (lam), $d$ a natural number with the hypothesis $2\le d$ on every statement. $T_d$, $T_1$ and $F_d$ are real-valued definitions in one definition file.
• Exponents. $T_d$'s $i$-th term uses the natural-number exponent $\sum_{1\le k<i}d^k=\frac{d^i-d}{d-1}$, so its $i=1$ term is $\lambda^0=1$. The series runs over $i\in\mathbb N$ with the $i=0$ term equal to $0$. $\lambda'=\lambda^{1/(d-1)}$ and $\lambda^{d/(d-1)}$ are real powers.
• Series and junk values. All series are real tsums; they converge for $0\le\lambda<1$. Outside that range Lean's conventions (a divergent series sums to $0$, $x/0=0$, $\log x=0$ for $x\le0$) produce meaningless values, so every statement either restricts $\lambda$ to $[0,1)$ or $(0,1)$ or is a limit along $\lambda<1$.
• Limits. "$\lambda\to1^-$" is the one-sided filter 𝓝[<] 1; the limit $1/\log d$ uses Real.log.
• Infinite product. The product identity is stated with HasProd (unconditional convergence of finite subproducts), which for factors $\ge1$ is the same as convergence of the partial products.
• Not trivializable. Because every limit is one-sided at $1$ and the denominators $\log T_1(\lambda)$ and $\log\frac1{1-\lambda}$ are positive there, no statement can be satisfied by Lean's junk values at $\lambda\ge1$ or at $\lambda=0$; the summability of the rewritten series is asserted explicitly.
• Infrastructure. Useful general lemmas: asymptotics of $\sum_i x^{d^i}$ as $x\to1^-$, products of finite geometric sums, change of variables in one-sided limits. These are reusable beyond this mission. Contributions of any of the milestones, or of alternative proofs of Lemma 3, are welcome.

Selected references

• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
• Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490

Motivation

Boosting combines many weak classifiers into a strong one by refitting, round after round, to a reweighted version of the training data. Freund and Schapire's AdaBoost was introduced as a procedure, with guarantees on the training error, and for several years it was not clear what statistical model it fitted. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) answered this by showing that boosting is stagewise additive modelling: each round adds one term to an additive function $F(x) = \sum_m f_m(x)$ so as to improve a population criterion.

Section 4.3 of that paper takes the step from interpretation to design. If boosting is stagewise fitting of an additive logistic model, one can choose the criterion directly: the Bernoulli log-likelihood. The resulting procedure, LogitBoost (Algorithm 3), fits at each round a weighted least-squares regression to a working response, exactly as iteratively reweighted least squares fits a logistic regression. Result 3 states that this is no accident: in the population, LogitBoost's update is a Newton step on the expected log-likelihood. The same Newton reading reappears in gradient boosting with logistic loss, where each terminal node of a tree takes one Newton step (Friedman 2001).

Timeline:

• 1997: Freund and Schapire, AdaBoost (J. Comput. Syst. Sci. 55).
• 1999: Schapire and Singer, Real AdaBoost with confidence-rated predictions (Mach. Learn. 37).
• 2000: Friedman, Hastie and Tibshirani, the statistical view; LogitBoost and Result 3.
• 2001: Friedman, gradient boosting machines (Ann. Statist. 29).

Setting

Let $X$ be a measurable space of features and let $\nu$ be a probability measure on $X\times\{0,1\}$, the joint law of a feature $x$ and a 0/1 response $y^*$. Write $E(\cdot\mid x)$ for the conditional expectation given $x$, an integral against the regular conditional distribution of $y^*$ given $x$.

A current fit is a function $F : X\to\mathbb R$. The symmetric logistic model (30) represents $P(y^*=1\mid x)$ by

For an update $f(x)$, the expected log-likelihood (31) is

whose integrand is the Bernoulli log-likelihood $y^*\log p + (1-y^*)\log(1-p)$ of $y^*$ under the model.

For a positive weight $w$, the weighted conditional expectation is $E_w(g\mid x) = E(wg\mid x)/E(w\mid x)$. LogitBoost (Algorithm 3), population version, computes the working response and weight

fits $f(x) = E_w(z\mid x)$ (the population weighted least-squares regression of $z$ on $x$), and updates $F(x)\leftarrow F(x)+\tfrac12 f(x)$.

Formalization targets

Goal: Result 3

Fix $x$ and let $\ell_x(t) = E[\,2y^*(F(x)+t) - \log(1+e^{2(F(x)+t)})\mid x]$. Then $\ell_x$ has first derivative $s(x)$ and second derivative $H(x)$ at $t=0$,

$H(x)\neq0$, and the population LogitBoost update equals the Newton update:

Milestones

1. (31): the integrand of $E\,l(F+f)$ is the Bernoulli log-likelihood of the symmetric logistic model.
2. (32): the first derivative $s(x)$.
3. (33): the second derivative $H(x)$.
4. (34)–(35): $F(x) - H(x)^{-1}s(x) = F(x) + \frac12 \frac{E(y^*-p(x)\mid x)}{E(p(x)(1-p(x))\mid x)} = F(x)+\frac12E_w\big(\frac{y^*-p(x)}{p(x)(1-p(x))}\,\big|\,x\big)$.
5. (36): the Newton update solves $\min_{f(x)} E_{w(x)}\big(F(x)+\frac12 z - (F(x)+f(x))\big)^2$.

Significance

The result. Result 3 explains what LogitBoost computes: a stagewise Newton–Raphson ascent of the expected Bernoulli log-likelihood, one coordinate $F(x)$ at a time. It makes the working response and the weights of Algorithm 3 the score and curvature of the likelihood, and reduces each round to a weighted least-squares problem (36) that any regression method can solve.

Formalizing it. The result is proved on the page by a short calculation, and no machine-checked version exists. The mission produces a formal account of the population algorithm on an arbitrary joint law, with conditional expectations taken through a regular conditional distribution, the derivatives stated with differentiability, and the Newton step identified exactly, including the constants $2$, $-4$ and $\tfrac12$ that the symmetric parametrization forces.

Difficulty

The algebra is short; the formal content is in keeping every object honest. The derivatives are of a conditional expectation in a parameter, so differentiation must pass through the integral against the conditional law. The second derivative needs the first derivative as a function of $t$, not only its value at $0$. The Newton step divides by $H(x)$, which must be shown nonzero from $0<p(x)<1$ rather than assumed. A tempting shortcut, replacing the conditional expectation of the log-likelihood by its closed form in a free probability parameter, removes the joint law from the statement and is ruled out.

Formalization scope

• Labels are Bool, with $y^*(\texttt{true}) = 1$ and $y^*(\texttt{false})=0$. The joint law is a probability measure ν on X × Bool; $E(\cdot\mid x)$ is the integral against Mathlib's ν.condKernel x. Every statement is for every $x$, conditional on $x$ as in the Derivation; because the label space is finite, no integrability or measurability hypotheses are needed.
• The symmetric logistic is written exactly as (30), $e^{t}/(e^{t}+e^{-t})$, not as $1/(1+e^{-t})$, which differs by a factor $2$ in $t$ and would change every constant.
• The conditional log-likelihood is defined as an integral against the conditional law, not by its closed form with a free parameter.
• Derivatives are stated with HasDerivAt, never with deriv, which returns $0$ at non-differentiable points; $H(x)\neq0$ is a conclusion, so the division in the Newton step cannot silently return $0$.
• The weighted conditional expectation takes its weight as an explicit argument; here it is $p(x)(1-p(x))$.
• In (36) the page writes $E_{w(x)}$ without "$\mid x$"; it is read as the conditional weighted expectation, since the Derivation conditions on $x$ throughout.
• Out of scope: the data version of Algorithm 3 (regression trees, the $z_{\max}$ threshold and the weight floor of pp. 352–353), which are implementation choices, and the multiclass algorithm (§5).

Contributions welcome: differentiation of finite conditional expectations in a parameter, and derivative facts for the symmetric logistic, both reusable across the other missions of this series.

Selected references

• J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. Syst. Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
• R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Mach. Learn. 37(3):297–336, 1999. https://doi.org/10.1023/A:1007614523901
• J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5):1189–1232, 2001. https://doi.org/10.1214/aos/1013203451