Motivation

Set cover asks for the fewest sets from a family $\mathcal S$ of $m$ subsets of a ground set $X$ of $n$ elements whose union contains $X$. It is NP-hard, and the best ratio achievable in polynomial time is $\Theta(\log n)$ (Feige 1998, doi:10.1145/285055.285059).

Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance $(X,\mathcal S)$ is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set $X'\subseteq X$ of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.

The question is how much an algorithm loses against an offline adversary who knows $X'$ and covers it with a family $\mathcal C_{OPT}$. This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor $O(\log m\log n)$ of $|\mathcal C_{OPT}|$. Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.

Setting

An instance consists of a finite ground set $X$ with $n=|X|$ elements and a finite family $\mathcal S$ of $m=|\mathcal S|$ sets. For an element $j$, $\mathcal S_j$ is the collection of sets containing $j$. Every set has cost $1$, so the cost of a family is its number of members.

The adversary gives a sequence $\sigma$ of elements (the given elements form $X'$). A family $\mathcal C_{OPT}\subseteq\mathcal S$ covers $\sigma$ if each element of $\sigma$ lies in some member of it.

The algorithm keeps a weight $w_S>0$ for every set, initially $w_S=1/(2m)$, and a cover $\mathcal C$, initially empty. The weight of an element is $w_j=\sum_{S\in\mathcal S_j}w_S$, and $C$ is the set of elements covered by members of $\mathcal C$. The potential is

$$\Phi=\sum_{j\notin C}n^{2w_j}.$$

When the adversary gives an element $j$:

1. if $w_j\ge1$, nothing changes;
2. otherwise a weight augmentation is performed: (a) $k$ is the minimal integer with $2^k w_j>1$; (b) every $S\in\mathcal S_j$ gets the weight $2^k w_S$; (c) at most $4\log n$ sets from $\mathcal S_j$ are added to $\mathcal C$, so that $\Phi$ does not exceed its value before the augmentation.

Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on $\sigma$ is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.

Formalization targets

Goal: Theorem 2.3

For $n\ge2$, every arrival sequence $\sigma$, and every family $\mathcal C_{OPT}$ covering $\sigma$: a run of the algorithm on $\sigma$ exists, and every run ends with a cover $\mathcal C$ that covers every element of $\sigma$ and satisfies

$$|\mathcal C|\;\le\;\lceil 4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2).$$

The paper states $|\mathcal C|=O(|\mathcal C_{OPT}|\log m\log n)$; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.

Milestones

Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most

$$|\mathcal C_{OPT}|\cdot(\log_2 m+2).$$

Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family $F\subseteq\mathcal S_j$ with $|F|\le\lceil4\ln n\rceil$ such that

$$\Phi_e\le\Phi_s,$$

where $\Phi_s$ is the potential before the iteration and $\Phi_e$ the potential after it, computed with the augmented weights and the cover $\mathcal C\cup F$.

Significance

The theorem shows that online set cover over a known instance admits a deterministic $O(\log m\log n)$-competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves $o\!\left(\frac{\log m\log n}{\log\log m+\log\log n}\right)$ over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.

The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.

Difficulty

The central step is Lemma 2.2: a family of at most $\lceil4\ln n\rceil$ sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of $\mathcal S_j$ can exceed the cardinality bound, since $\mathcal S_j$ may contain up to $m$ sets. Adding nothing, or a single set, can increase $\Phi$: every uncovered element sharing a set with $j$ has its weight raised, and its term $n^{2w}$ grows by a factor up to $n^{2\delta}$. The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of $n$.

The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs $n\ge2$ and a careful treatment of the initial potential, which is at most $n^2$ and equals $n^2$ when every element lies in every set.

Formalization scope

The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight ($w_j$) and coveredBy ($j\in C$). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. $n=|E|$ and $m=|T|$. Weights are real numbers; $n^{2w_j}$ is the real power.

The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.

Explicit forms of the paper's asymptotic and unspecified quantities:

• the paper's "$4\log n$" sets per augmentation is $\lceil 4\ln n\rceil$ (natural logarithm, rounded up: the proof repeats a random choice that many times and needs $(1-\delta/2)^{4\log n}\le n^{-2\delta}$);
• Lemma 2.1's $\log m+2$ is $\log_2 m+2=\log_2(4m)$ (weights grow from $1/(2m)$ to at most $2$ by factors at least $2$);
• Theorem 2.3's $O(|\mathcal C_{OPT}|\log m\log n)$ is $\lceil4\ln n\rceil\cdot|\mathcal C_{OPT}|\cdot(\log_2 m+2)$;
• $k$ ranges over natural numbers; for $w_j<1$ the minimal integer with $2^kw_j>1$ is one;
• the paper's remark "(Clearly, $2^k\cdot w_j<2$.)" is not encoded; the correct bound is $\le2$ ($w_j=1/2$ gives $k=2$) and is not a hypothesis anywhere.

The goal adds the hypothesis $n\ge2$, which the paper's $\log n$ assumes tacitly: for $n=1$ no set may be added and the element is never covered.

Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.

A complete development needs elementary real analysis (Real.rpow, Real.log, $1-x\le e^{-x}$), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM J. Comput. 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• U. Feige, A Threshold of ln n for Approximating Set Cover, J. ACM 45(4):634–652, 1998. https://doi.org/10.1145/285055.285059
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$. Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$, a randomized local search achieving $2/5$, and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$.
• Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$-approximation (this mission) and a randomized linear-time $1/2$-approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$, and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$. In iteration $i = 1, \dots, n$ it computes

$$a_i = f(X_{i-1} \cup \{u_i\}) - f(X_{i-1}), \qquad b_i = f(Y_{i-1} \setminus \{u_i\}) - f(Y_{i-1}).$$

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$, $Y_i = Y_{i-1}$; otherwise $X_i = X_{i-1}$, $Y_i = Y_{i-1} \setminus \{u_i\}$. A tie adds $u_i$. After $n$ iterations $X_n = Y_n$, which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$, which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$. In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$,

$$X_n = Y_n \qquad\text{and}\qquad f(OPT) \le 3\, f(X_n).$$

Milestones

1. Lemma II.1. For every $1 \le i \le n$, $a_i + b_i \ge 0$.
2. The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$.
3. Lemma II.2. For every $1 \le i \le n$,

$$f(OPT_{i-1}) - f(OPT_i) \le [f(X_i) - f(X_{i-1})] + [f(Y_i) - f(Y_{i-1})].$$

4. The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$.
5. Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$.

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$, is the template the paper then refines into the randomized $1/2$-approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$, which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$, not against $OPT$. For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

• The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
• Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
• The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$.
• The tie rule is line 5's $a_i \ge b_i$: ties add $u_i$.
• Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
• The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$, because $f(OPT)$ may be $0$.
• Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$-approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$, without which $f \equiv 0$ would satisfy it.
• Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$. A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$" would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.

Selected references

• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205)
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
• S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
• M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011. https://doi.org/10.1007/978-3-642-22006-7_29

Motivation

Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.

The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.

Setting

A directed network has $n$ numbered points. Its length matrix $w$ assigns a real number $w(i,j)$ to a direct link from $i$ to $j$. The value $\infty$ means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries $w(i,i)$ are unrestricted. The paper's matrix index range is $1,\ldots,n$; the Lean development uses $0,\ldots,n-1$ in the same order.

A path from $i$ to $j$ is a sequence $p_0=i,p_1,\ldots,p_L=j$ with $L\ge1$ links. The points $p_0,\ldots,p_{L-1}$ are distinct, as are $p_1,\ldots,p_L$. Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is $\ell_w(p)=\sum_{t=0}^{L-1}w(p_t,p_{t+1})$; a missing link gives length $\infty$. Write $d_w(i,j)$ for the minimum length among these paths, taking $d_w(i,j)=\infty$ when there is no finite-length path. Since $L\le n$, this is a minimum over a finite family.

The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.

Algorithm 97 scans a pivot $i$, then row $j$, then column $k$, each in increasing order. It enters the column scan when the current $m(j,i)$ is finite; if the current $m(i,k)$ is also finite, it computes $s=m(j,i)+m(i,k)$ and replaces $m(j,k)$ when $s<m(j,k)$. Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when $m(j,i)$ and $m(i,k)$ are true, it sets $m(j,k)$ to true.

Formalization targets

Reachability and missing paths

For Algorithm 96, let $b^+$ be the transitive closure of the initial parent relation $b$, using chains of one or more links. Its comment asserts

$$\operatorname{ancestor}(b)(i,j)=\mathrm{true}\quad\Longleftrightarrow\quad i\mathrel{b^+}j.$$

For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from $i$ to $j$,

$$\operatorname{shortestPath}(w)(i,j)=\infty.$$

This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.

Complete shortest-path matrix

The goal is the whole output claim of Algorithm 97. For every $n$, every matrix $w$ with no negative cycle, and all points $i,j$,

$$\operatorname{shortestPath}(w)(i,j)=d_w(i,j).$$

The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.

Significance

The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.

Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.

Difficulty

The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on $m(j,i)$ is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.

Formalization scope

Points are Fin n, including the empty network at $n=0$ and the single-point network at $n=1$. Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is $10^{10}$; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.

The initial diagonal is not normalized. Therefore a path from $i$ to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.

The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length $-1$, the procedure changes that entry to $-2$, although the shortest simple closed path has length $-1$. No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark $d_w$ is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.

Selected references

• Robert W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6), 1962, p. 345. DOI 10.1145/367766.368168.
• Robert W. Floyd, Algorithm 96: Ancestor, Communications of the ACM 5(6), 1962, pp. 344–345, in the same published Algorithms department scan.

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.

Timeline of the setting:

• Dynkin (1963) introduced the classical problem; the rule "observe a $1/e$ fraction, then accept the first record" selects the best candidate with probability tending to $1/e$.
• Rasmussen and Pliska (1975/76) and Mahdian, McAfee and Pennock (2008, personal communication cited by the paper) studied secretary problems with specific "well-behaved" discount functions such as $d(t)=\beta^t$.
• Babaioff et al. (2009) treat an arbitrary discount function $d$. Without prior knowledge, no algorithm is better than $\Omega(\log n/\log\log n)$-competitive (their Theorem 4.3), and $O(\log n)$ is achievable (Theorem 4.4). If the algorithm knows a good estimate $Z$ of the expected offline optimum, a single threshold rule recovers a constant fraction (Theorem 4.7, headlined as Theorem 1.2). This mission formalizes that last result.

Setting

There are $n\ge1$ elements, indexed by $\mathrm{Fin}\,n$. Element $e$ has a value $v(e)\ge0$, and each time $t\in\{1,\dots,n\}$ has a discount $d(t)\ge0$. The elements arrive in a uniformly random order $\pi$, a bijection from times to elements: element $\pi(t)$ arrives at time $t$. Selecting the element that arrives at time $i$ earns $d(i)\,v(\pi(i))$, and an algorithm selects at most one element.

The offline optimum on the order $\pi$ is $\mathrm{OPT}(\pi)=\max_{i=1}^n d(i)\,v(\pi(i))$. It is a random variable, and the benchmark is its expectation

$$\mathbf E[\mathrm{OPT}]=\sum_{\pi\in S_n}\frac1{n!}\max_{i=1}^n\{d(i)\,v(\pi(i))\}.$$

For a real parameter $Z$, algorithm $\mathcal A$ selects the first time $j$ at which $d(j)\,v(\pi(j))\ge Z/2$ and earns that product; if no time qualifies, it selects nothing and earns $0$. It knows $Z$ and $d$, sees the values one at a time, and never sees the future of $\pi$. Its expected value is $\mathbf E[\mathcal A]=\sum_{\pi\in S_n}\frac1{n!}\,\mathcal A(\pi)$.

The proof uses three derived objects:

• the accepting permutations $S_{acc}=\{\pi:\max_i d(i)v(\pi(i))\ge Z/2\}$, on which $\mathcal A$ selects something;
• their contribution $L=\sum_{\pi\in S_{acc}}\frac1{n!}\max_i d(i)v(\pi(i))$ to $\mathbf E[\mathrm{OPT}]$;
• for a time $i$ and an element $j$, the set $G_{ij}$ of orders on which $\mathcal A$ selects $j$ at time $i$. These are the orders with $\pi(i)=j$ and $d(k)v(\pi(k))<Z/2$ for every $k<i$.

Formalization targets

Goal: Theorem 4.7

For every $n\ge1$, all discounts $d\ge0$, all values $v\ge0$ and every real $Z$,

$$Z\le\mathbf E[\mathrm{OPT}]\ \Longrightarrow\ \mathbf E[\mathcal A]\ \ge\ \frac Z4.$$

Taking $Z=\mathbf E[\mathrm{OPT}]$ gives $\mathbf E[\mathrm{OPT}]\le4\,\mathbf E[\mathcal A]$, a $4$-competitive algorithm when the expected optimum is known.

Milestones (in the order of the paper's proof, p. 8)

1. Eq. (4.1). If $Z\le\mathbf E[\mathrm{OPT}]$ then $L\ge Z/2$.
2. Eq. (4.3). If $Z\le\mathbf E[\mathrm{OPT}]$ then

$$\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}\frac1n\,d(i)v(j)\ \ge\ \frac Z2.$$

3. Eq. (4.4). $\displaystyle\mathbf E[\mathcal A]=\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}d(i)v(j)\,\frac{|G_{ij}|}{|S_n|}$.
4. Claim 4.8. For every $i,j$ with $d(i)v(j)\ge Z/2$, $n|G_{ij}|\ge|S_n\setminus S_{acc}|$; and if $2|S_{acc}|\le n!$ then $2n|G_{ij}|\ge n!$.

Significance

The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number $\mathbf E[\mathrm{OPT}]$, or of any lower estimate $Z$ of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, $\mathbf E[\mathrm{OPT}]$ can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than $\sqrt2$.

Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over $S_n$ as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.

Difficulty

The obvious argument fails when $\mathcal A$ rarely selects. $\mathcal A$ earns at least $Z/2$ whenever it selects anything, so $\mathbf E[\mathcal A]\ge\frac Z2\Pr[\mathcal A\text{ selects}]$. That settles the case $\Pr[\mathcal A\text{ selects}]\ge1/2$ and nothing else: the probability of selecting can be tiny while $\mathbf E[\mathrm{OPT}]$ is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair $(i,j)$ with $d(i)v(j)\ge Z/2$ must be realized by $\mathcal A$ on a positive fraction of the orders.

Two points need care in a formal proof:

• Eq. (4.2) rewrites $L$ as a sum over pairs weighted by the conditional probability that $d(i)v(j)$ is the highest product. It relies on a consistent tie-breaking rule, which the paper leaves implicit.
• Claim 4.8 is a counting argument on $S_n$. A map from the rejecting orders into $G_{ij}$ swaps element $j$ into position $i$, and must be shown to be at most $n$-to-$1$ and to land in $G_{ij}$.

Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.

Formalization scope

• Types. Times and elements are Fin n; the paper's time $t$ is the index $t-1$. An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes $n\ge1$, so the maximum over times is a genuine maximum (Finset.sup').
• Expectations. Expectations over the uniform order are finite averages $\frac1{n!}\sum_\pi$. No measure theory is used.
• Values and constants. Values, discounts and $Z$ are real numbers, and the hypotheses $d\ge0$, $v\ge0$ are explicit. The constant $1/4$ is the paper's. The bound is stated multiplicatively, $Z/4\le\mathbf E[\mathcal A]$, never as a ratio.
• Thresholds and ties. Every threshold is non-strict ($\ge Z/2$), exactly as on pp. 7–8. $\mathcal A$ selects the first qualifying time, so it needs no tie-breaking. The tie-breaking remark at Eq. (4.2) concerns only the paper's intermediate identity (4.2), which is not a milestone.
• Claim 4.8. Both inequalities are stated with cleared denominators. The second carries the proof's case hypothesis $2|S_{acc}|\le n!$, which the paper uses in the same place ("at most half the permutations are in $S_{acc}$").
• What is not this theorem. $\mathcal A$ is the online threshold rule with threshold $Z/2$ applied to $\pi$ as it unfolds. An algorithm that inspects the whole order, or that chooses its threshold after seeing the values, would make the bound trivial and is not this theorem.
• Contributions welcome. Proofs of each milestone, including the counting argument of Claim 4.8. Lemmas on averages over Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009.
• E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR 150:238–240, 1963.
• W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3):279–289, 1975/76.
• M. Mahdian, P. McAfee, D. Pennock, The secretary problem with durable employment, personal communication, 2008 (cited as [MMP08]).
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443.

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least $1/e$, so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time $t$ is worth $d(t)\,v(e)$ for a known discount function $d$. Discounts model settings where a sale is worth more at some times than at others. The case $d(t)=\beta^t$ had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary $d$. Its answer has two sides: an $O(\log n)$-competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than $\Omega(\log n/\log\log n)$-competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.

Setting

There are $n$ elements $e\in\{0,\dots,n-1\}$ with values $v(e)\ge 0$, and a discount function $d$ on the times. The elements arrive in a uniformly random order $\pi$: element $\pi(t)$ arrives at time $t$. A randomized online stopping rule $A$ specifies, for each time $t$ and each sequence of values seen so far $h=(v(\pi(0)),\dots,v(\pi(t)))$, a probability $p_t(h)\in[0,1]$ of stopping at $t$ if it has not stopped yet. Stopping at $t$ selects $\pi(t)$ and earns $d(t)\,v(\pi(t))$; the rule selects at most one element and may select none. The rule knows $n$ and $d$, but it sees only values, only as they arrive, and it is not told which instance it is facing.

The expected value of $A$ is

$$\mathbb E[A]=\mathbb E_\pi\Bigl[\sum_t d(t)\,v(\pi(t))\,p_t(h_t)\prod_{s<t}\bigl(1-p_s(h_s)\bigr)\Bigr],$$

and the benchmark is the expected offline optimum

$$\mathbb E[\mathrm{OPT}]=\mathbb E_\pi\Bigl[\max_t d(t)\,v(\pi(t))\Bigr],$$

which is itself a random variable averaged over the order. $A$ is $\alpha$-competitive on an instance when $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$.

The hard family (§4.1.1 of the paper): fix an integer $c\ge1$ and put $L=c$, $n=L^{4c}$, $n_t=L^{2t}$ for $t\le 2c$, and $K=n^2$. The step discount is $d(j)=L^{-1}$ on the times $1\le j\le n_1$ and $d(j)=L^{-t}$ on $n_{t-1}<j\le n_t$. The instance $\mathcal I_1$ has $n/n_1$ elements of value $K$ and the rest $0$; $\mathcal I_{t+1}$ is obtained from $\mathcal I_t$ by raising $n/n_{t+1}$ of its values $K^t$ to $K^{t+1}$, so $\mathcal I_t$ has $n/n_t$ elements of value $K^t$.

Formalization targets

Goal: Theorem 4.3 in the form its proof establishes

For every integer $c\ge1$ and every randomized online stopping rule $A$ for horizon $n=c^{4c}$ and the step discount,

$$\exists\,t\in\{1,\dots,2c\}:\qquad c\cdot\mathbb E[A(\mathcal I_t)]\ <\ 10\cdot\mathbb E[\mathrm{OPT}(\mathcal I_t)].$$

That is, no online rule is $c/10$-competitive on all of $\mathcal I_1,\dots,\mathcal I_{2c}$.

Milestones

1. Lemma 4.1: $\mathbb E[\mathrm{OPT}(\mathcal I_t)]\ge(1-1/e)K^tL^{-t}$ for $1\le t\le 2c$.
2. Coupling step of Lemma 4.2's proof: for every rule and $1\le t<2c$, the probability of stopping among the first $n_t$ arrivals drops by at most $1/L^2$ from $\mathcal I_t$ to $\mathcal I_{t+1}$.
3. Lemma 4.2: a rule that is $c/10$-competitive on $\mathcal I_1,\dots,\mathcal I_{2c}$ stops among the first $n_t$ arrivals of $\mathcal I_t$ with probability at least $t/c$.
4. Theorem 4.3, asymptotic form: for $c\ge2$ and $n=c^{4c}$, every rule has some $\mathcal I_t$ with

$$\frac1{40}\cdot\frac{\log n}{\log\log n}\cdot\mathbb E[A(\mathcal I_t)]<\mathbb E[\mathrm{OPT}(\mathcal I_t)].$$

Significance

The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the $e$-competitive classical rule). Together with the paper's $O(\log n)$ upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between $\log n/\log\log n$ and $\log n$ up to constants, and it motivates the paper's known-$\mathrm{OPT}$ model (§4.2), where an estimate of $\mathbb E[\mathrm{OPT}]$ restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.

The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the $O(\log n)$ upper bound, and the $\sqrt2$ lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.

Difficulty

The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the $2c$ instances against each other. A rule that does well on $\mathcal I_t$ must commit early, within the first $n_t$ steps, yet the rule cannot distinguish $\mathcal I_t$ from $\mathcal I_{t+1}$ during those steps except with probability $L^{-2}$. Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time $t$ depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on $\mathcal I_{t+1}$ and its late earnings are both small compared with $\mathbb E[\mathrm{OPT}(\mathcal I_{t+1})]$, which uses $L\ge 2$ and that $K=n^2$ dwarfs $L^{2c}$.

Formalization scope

• Elements and times are Fin n, 0-based: index $j$ is the paper's time $j+1$, so the paper's block $(n_{t-1},n_t]$ is the index range $[n_{t-1},n_t)$. The random order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and every expectation over it is the finite average $\frac1{n!}\sum_\pi$. Values and discounts are real.
• Algorithms are the structure StoppingRule n: stopping probabilities $p_t(h)\in[0,1]$ indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that $p_t(h)$ depends only on $h_0,\dots,h_t$. The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on $n$ and $d$ but not on the instance index.
• OPT is $\mathbb E_\pi[\max_t d(t)v(\pi(t))]$ (a supremum over the finite type Fin n), and competitiveness is multiplicative, $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$, never a quotient.
• Constants. The goal uses the paper's constant $10$ (from "if $A$ is $c/10$-competitive"); the asymptotic form uses $1/40$, from $\log n/\log\log n\le 4c$ for $c\ge2$, with the natural logarithm. $K=n^2$, the value the paper suggests.
• The construction ($n$, $n_t$, $d$, $K$, $\mathcal I_t$) is fixed by explicit formulas in the definition file. A solver cannot choose the discount or the instances, and the goal is not stated for a restricted class of algorithms; a formalization that let the rule see the instance index or future values, or quantified only over threshold rules, would be a different and trivial or weaker theorem. For $c<10$ the goal is immediate, since $\mathbb E[A]\le\mathbb E[\mathrm{OPT}]$ and $\mathbb E[\mathrm{OPT}(\mathcal I_t)]>0$; the content lies in $c\ge10$. The bound is stated only for the horizons $n=c^{4c}$ the paper constructs.
• Needed infrastructure: counting arguments over permutations of Fin n (the probability that a set of $m$ elements misses the first $k$ positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135 (authors' full version, the one cited here: https://www.cs.jhu.edu/~mdinitz/papers/secretary.pdf)
• E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR, 1963.
• W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3), 1976.
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

Motivation

The simplex method, introduced by G. B. Dantzig in 1947, is the standard algorithm for linear programming and remains the core of commercial solvers. It moves from one basic feasible solution to another by pivot steps, and at each step a pivot rule chooses which variable enters and which leaves the basis. For several natural rules, including Dantzig's original largest-coefficient rule, the method can cycle: on a degenerate linear program it can return to a basis it has already visited and repeat forever without improving the objective. Hoffman (1953) and Beale (1955) gave cycling examples.

R. G. Bland (New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2), 1977) showed that a simple combinatorial rule, choosing the smallest eligible index for both the entering and the leaving variable, never cycles. This makes the simplex method a finite algorithm on every linear program in equational form, and it gives an algorithmic proof of the duality theorem. Chapter 5 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), develops the general theory of simplex tableaus and proves Bland's theorem as Theorem 5.8.1. This mission is the third of a series formalizing that book.

Setting

A linear program in equational form is

$$\text{maximize } c^{T}x \quad\text{subject to}\quad Ax=b,\ x\ge 0,$$

with $A$ a real $m\times n$ matrix, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. Following §4.2 of the book, $A$ has $n\ge m$ columns and rank $m$. For an $m$-element set $B=\{k_1<\dots<k_m\}\subseteq\{1,\dots,n\}$ let $N=\{\ell_1<\dots<\ell_{n-m}\}$ be its complement, and $A_B$, $A_N$ the matrices of the columns of $A$ indexed by $B$ and $N$. $B$ is a feasible basis if $A_B$ is nonsingular and $A_B^{-1}b\ge0$; its basic feasible solution is the unique $x$ with $Ax=b$ and $x_j=0$ for $j\notin B$.

A simplex tableau $T(B)$ is a system

$$x_B=p+Q\,x_N,\qquad z=z_0+r^{T}x_N$$

in the variables $x_1,\dots,x_n,z$ with the same solutions as $Ax=b$, $z=c^Tx$. A nonbasic variable $x_v$, $v=\ell_\beta$, may enter if $r_\beta>0$; a basic variable $x_u$, $u=k_\alpha$, may then leave if

$$q_{\alpha\beta}<0\quad\text{and}\quad-\frac{p_\alpha}{q_{\alpha\beta}}=\min\Bigl\{-\frac{p_i}{q_{i\beta}}: q_{i\beta}<0\Bigr\}.\tag{5.3}$$

The pivot step replaces $B$ by $B'=(B\setminus\{u\})\cup\{v\}$. Bland's rule takes the entering variable of smallest index among those with $r_\beta>0$, and the leaving variable of smallest index among those satisfying (5.3).

Formalization targets

Goal: Theorem 5.8.1 (p. 73)

There is no infinite sequence of bases

$$B_0\to B_1\to B_2\to\cdots$$

in which each $B_{t+1}$ is obtained from the feasible basis $B_t$ by a pivot step obeying Bland's rule. Since there are finitely many bases and a Bland step is determined by its starting basis, this is the book's "always finite; i.e., cycling is impossible".

Milestones

1. Lemma 5.5.1 (p. 66): a feasible basis has exactly one simplex tableau, with $Q=-A_B^{-1}A_N$, $p=A_B^{-1}b$, $z_0=c_B^TA_B^{-1}b$, $r=c_N-(c_B^TA_B^{-1}A_N)^T$.
2. Optimality criterion (§5.6, p. 67): if $r\le0$, the basic feasible solution of $B$ is optimal.
3. Lemma 5.6.1 (p. 68): a pivot step leads to a feasible basis; if no leaving variable exists, the program is unbounded along an explicit ray.
4. Claim in the proof of Theorem 5.8.1 (p. 73): for any pivot rule, all bases of a cycle have the same basic feasible solution, and every variable that enters during the cycle is $0$ in it.

Significance

With the optimality criterion and Lemma 5.6.1, Theorem 5.8.1 turns the simplex method into an algorithm: started from any feasible basis, it stops after finitely many pivot steps at an optimal basic feasible solution or with a ray certifying unboundedness. Combined with the auxiliary program of §5.6 for finding a first feasible basis, this yields a constructive proof that every feasible, bounded linear program has an optimal basic feasible solution, and the book remarks that the duality theorem follows easily. Bland's rule is also the model for later combinatorial anticycling rules in oriented matroid programming.

The theorem is classical and fully proved in the book. What the mission adds is a machine-checked version stated in the book's own tableau notation. On Prove2Me the simplex method is formalized in the Bertsimas–Tsitsiklis series (Introduction to Linear Optimization IV), for minimization with reduced costs, with termination proved under nondegeneracy and for the lexicographic rule; Bland's rule is not formalized there.

Difficulty

The obvious termination argument is that the objective value strictly increases at each step, so no basis repeats. That argument fails exactly at degenerate pivot steps, where the minimum in (5.3) is $0$: the basis changes, the basic feasible solution and the objective value do not. Along a degenerate stretch the objective gives no progress measure, and for general pivot rules the method does cycle there. Any proof must therefore use the specific tie-breaking of Bland's rule, which is a statement about indices, not about values, and relate the tableaus of two different bases in the cycle to each other. Counting bases or tracking the objective value alone does not suffice.

Formalization scope

Vectors are Fin n → ℝ and the book's indices $1,\dots,n$ become $0,\dots,n-1$. Bases are Finset (Fin n); the sorted enumerations $k_1<\dots<k_m$ and $\ell_1<\dots<\ell_{n-m}$ are Finset.orderEmbOfFin, tableau rows are indexed by Fin m and nonbasic columns by Fin (n - m). Nonsingularity of $A_B$ is IsUnit A_B.det, so the Mathlib inverse is the true inverse wherever it appears. The tableau parameters used by the pivot rules are the explicit formulas of Lemma 5.5.1; the tableau itself is also defined as in the book (same solution set) so that Lemma 5.5.1 is a genuine statement. "Smallest index" compares variable indices, not row positions. Optimality and unboundedness are stated against feasible points, not through a supremum. Every theorem assumes $n\ge m$ and $\operatorname{rank}A=m$, the standing assumption of §4.2.

A formalization in which any improving variable may enter proves a different, false statement, since cycling examples exist for such rules; the step relation here fixes both choices by Bland's rule. The step relation is not empty: it holds whenever the current tableau has a positive last-row coefficient and a negative entry in the entering column, so the goal is not vacuous.

The development needs basic linear algebra over Matrix, the uniqueness of basic feasible solutions, and bookkeeping for sorted index enumerations. Lemma 5.5.1 and Lemma 5.6.1 are reusable for any later formalization of the simplex method in this notation. Contributions are welcome for each milestone, for the cycle-form corollary, and for a sorry-free proof of the goal.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 5. https://doi.org/10.1007/978-3-540-30717-4
• R. G. Bland, New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2):103–107, 1977. https://doi.org/10.1287/moor.2.2.103
• E. M. L. Beale, Cycling in the dual simplex algorithm, Naval Research Logistics Quarterly 2(4):269–275, 1955. https://doi.org/10.1002/nav.3800020407
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 3.

We formalize the equivalence between Turing machines and the WordRAM model of computation. Turing machines are the standard model for studying computability, but algorithms are rarely described in terms of tape operations. WordRAM is much closer to assembly, with memory accesses, arithmetic instructions, branches, and loops. The goal is to connect this familiar way of expressing algorithms to the foundations of computability. This will also bring us closer to one day formalizing Fine Grained Complexity.

The formal target is halting equivalence through simulations in both directions, with the stated memory bounds and a family of word widths, each fixed during a run.

References:

• Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
• Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

Motivation

Scheduling indivisible jobs on parallel machines to finish all of them as early as possible is a basic problem in operations research and in the theory of algorithms. In the unrelated machines model each job may take a different time on each machine, with no relation between the rows of the time table, as when machines of different types (black-and-white, duplex, colour copiers in the book's example) handle jobs of different kinds. Minimizing the makespan in this model is NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.

• 1990. Lenstra, Shmoys and Tardos (Math. Programming 46, 259–271) give a polynomial-time algorithm that rounds a basic optimal solution of a linear programming relaxation and returns a schedule of makespan at most $2\,t_{\mathrm{opt}}$. The same paper shows that approximating the optimum makespan within a factor less than $3/2$ is NP-hard.
• 2007. Matoušek and Gärtner present the algorithm in §8.3 of Understanding and Using Linear Programming in a simplified, somewhat less efficient form: minimize $t^*(T) + T$ over the thresholds $T$ rather than binary-searching for the smallest $T$ with $t^*(T) \le T$. This mission follows the book's presentation.

The gap between $3/2$ and $2$ for the general unrelated-machines problem has remained open since 1990; it is the standard example of LP rounding driven by the sparsity of basic solutions.

Setting

There are $m$ machines $M$ and $n$ jobs $J$; $d_{ij} > 0$ is the running time of job $j$ on machine $i$. A schedule is a map $\sigma : J \to M$ assigning each job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} d_{ij}$, the makespan of $\sigma$ is the largest load, and $t_{\mathrm{opt}}$ is the makespan of an optimal schedule, one whose makespan is at most that of every schedule.

For a real threshold $T$, the linear program $\mathrm{LPR}(T)$ in the variables $t$ and $x_{ij}$ is

$$\begin{aligned} \text{minimize } \ & t \\ \text{subject to } \ & \textstyle\sum_{i \in M} x_{ij} = 1 \ \ (j \in J), \qquad \textstyle\sum_{j \in J} d_{ij} x_{ij} \le t \ \ (i \in M),\\ & x_{ij} \ge 0, \qquad x_{ij} = 0 \ \text{ whenever } d_{ij} > T . \end{aligned}$$

Its optimal value is $t^*(T)$, with $t^*(T) = \infty$ when $\mathrm{LPR}(T)$ is infeasible. The constraint matrix $A$ has one row per machine, one per job and one per pair with $d_{ij} > T$; the column of $x_{ij}$ carries $d_{ij}$ in the row of machine $i$, $1$ in the row of job $j$, and $1$ in the row of the constraint $x_{ij} = 0$ if present. Assumption 8.3.1 on a solution $x^*$ is that the columns of $A$ belonging to its nonzero variables are linearly independent; basic feasible solutions satisfy it. The support graph of $x^*$ is the bipartite graph $G = (M \cup J, E)$ with $E = \{\{i,j\} : x^*_{ij} > 0\}$.

Formalization targets

Goal: Theorem 8.3.4

Let $T^*$ minimize $t^*(T) + T$ over all real $T$ and let $(t^*, x^*)$ be an optimal solution of $\mathrm{LPR}(T^*)$ satisfying Assumption 8.3.1. Then there is a schedule $\sigma$ with $x^*_{\sigma(j) j} > 0$ for every job $j$ and

$$\max_{i \in M} \sum_{j : \sigma(j) = i} d_{ij} \;\le\; 2\, t_{\mathrm{opt}} .$$

Milestones

1. Lemma 8.3.2. Every subgraph of the support graph $G$ has at most as many edges as vertices: $|E'| \le |M'| + |J'|$.
2. Lemma 8.3.3. For $T \ge 0$ and an optimal solution $(t^*, x^*)$ of $\mathrm{LPR}(T)$ satisfying Assumption 8.3.1, some schedule along the edges of $G$ has makespan at most $t^* + T$.
3. Proof of Theorem 8.3.4, first step. $\mathrm{LPR}(t_{\mathrm{opt}})$ is feasible and $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$.
4. Proof of Theorem 8.3.4, second step. $t^*(T^*) + T^* \le 2\,t_{\mathrm{opt}}$.

Significance

The theorem gives a polynomial-time 2-approximation for an NP-hard problem, and its proof isolates a reusable principle: a basic solution of an assignment-type LP has a support graph in which every subgraph has at most as many edges as vertices (a pseudoforest), so all but a matching's worth of the fractional assignment is already integral. The same sparsity argument underlies rounding results for the generalized assignment problem and for many later scheduling and allocation relaxations.

The result has been proved since 1990 and is textbook material. It is not formalized on Prove2Me or, to the maintainers' knowledge, in Mathlib. This mission produces a machine-checked version of the rounding theorem together with the counting lemma on basic solutions, the relaxation inequality $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$, and the bound on the chosen threshold, each stated on shared definitions of the scheduling LP.

Difficulty

The obvious approach, rounding every job to the machine carrying the largest fraction of it, can overload a machine by many jobs at once and gives no constant factor. The bound $t^* + T$ needs two facts that are not visible from the LP value alone: that the support of a basic solution is sparse in the precise sense of Lemma 8.3.2, which has to be read off the linear independence of columns of the constraint matrix after deleting rows; and that the jobs left fractional can be matched injectively to machines, which requires a Hall-type condition derived from that sparsity. Relating linear independence of real column vectors to an edge count in a bipartite graph, and then producing a matching, is where the formal work lies.

A second subtlety is the threshold $T$: the bound $t^* + T \le 2 t_{\mathrm{opt}}$ holds only because $T^*$ is chosen by minimizing over thresholds, and the relaxation at $T = t_{\mathrm{opt}}$ must be compared with the one at $T^*$ through optimal solutions of different linear programs.

Formalization scope

Machines are Fin m, jobs are Fin n (0-based; the book's machines $1,\dots,m$ and jobs $m+1,\dots,m+n$ are disjoint index sets), running times form d : Matrix (Fin m) (Fin n) ℝ, and the standing hypothesis $d_{ij} > 0$ of §8.3 appears in every theorem. A schedule is a function Fin n → Fin m; the makespan is the supremum of the loads over the finite type Fin m, which is the maximum for $m \ge 1$. The optimum $t_{\mathrm{opt}}$ is the makespan of a schedule assumed optimal, never an infimum.

Optimal values of $\mathrm{LPR}(T)$ are never written as sInf: statements quantify over optimal solutions, i.e. feasible $(t, x)$ with $t \le t'$ for every feasible $(t', x')$. The book's convention $t^*(T) = \infty$ for infeasible $\mathrm{LPR}(T)$ is encoded by letting thresholds without an optimal solution impose no condition in the minimality hypothesis on $T^*$, which reads $t^* + T^* \le t + T$ for every real $T$ and every optimal solution $(t, x)$ of $\mathrm{LPR}(T)$. The constraint matrix used in Assumption 8.3.1 has rows indexed by Fin m ⊕ Fin n ⊕ {(i, j) // T < d i j} and excludes the column of $t$, as on p. 151.

"Efficiently construct" in Lemma 8.3.3 and "computes" in Theorem 8.3.4 are formalized by the property of the constructed schedule, not by its running time: every job goes to a machine $i$ with $x^*_{ij} > 0$. This constraint is what rules out the trivializing formalization — "some schedule has makespan at most $2 t_{\mathrm{opt}}$" is true of the optimal schedule itself and says nothing about the rounding.

A complete development needs: finite linear algebra (a linearly independent family of vectors supported on $k$ coordinates has at most $k$ members), Hall's marriage theorem (available in Mathlib as Finset.all_card_le_biUnion_card_iff_exists_injective), and the existence of an optimal solution of a feasible, bounded linear program (used to apply the minimality of $T^*$ at $T = t_{\mathrm{opt}}$). The counting lemma for basic solutions and the definitions of $\mathrm{LPR}(T)$ are reusable for other assignment relaxations. Proofs of any milestone, and alternative proofs of Lemma 8.3.3 by the direct pseudoforest argument of p. 153–154, are welcome.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.3, pp. 148–156. https://doi.org/10.1007/978-3-540-30717-4
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990), 259–271. https://doi.org/10.1007/BF01585745