Motivation

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012

The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$. Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

$$f(A\cup B)+f(A\cap B)\le f(A)+f(B)\qquad(A,B\subseteq\mathcal N).$$

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$. The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2

Algorithm 2 visits the elements once in an arbitrary order $u_1,\ldots,u_n$. It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$. At step $i$, it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$. It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$. It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$. When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

$$\max_{S\subseteq\mathcal N}f(S)\le 2\,\mathbb E[f(X_n)].$$

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$, set $OPT_i=(O\cup X_i)\cap Y_i$. Lemma II.1 asserts $a_i+b_i\ge0$. The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$. Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$. The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2

A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities $f_1,f_2$, let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$. The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

$$3\max_{S\subseteq\mathcal N}g(S)\le4\,\mathbb E[g(X_n)].$$

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4

This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$. The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$. Buchbinder et al., proof of Lemma III.1

Formalization scope

The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles $0/0$ by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.

The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.

The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints $F$ for $f$ in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in $Y\setminus X$, a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.

Selected references

• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

We establish the polynomial simulation needed for WordRAM-based NP proofs. It reuses the same machines and Cook–Levin definitions, with uniform programs, logarithmic word widths, and standard bit input/output.

The targets cover function outputs and verifier verdicts, including loading and serialization costs.

This adapts Cook–Reckhow’s Theorem 2(a), pp. 361–363, to Hagerup’s bounded-word operations, including multiplication; no particular simulation exponent is prescribed.

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

Single-machine sequencing is the base case of deterministic scheduling theory. Many multi-machine and shop problems are analysed by reduction to it, and many bounds and approximation algorithms for harder models use it as a subroutine. A central objective class is the bottleneck or minmax objective. Each job carries a nondecreasing cost of its completion time, and the schedule is judged by its worst job. Maximum lateness, maximum tardiness and maximum weighted tardiness are all special cases.

Before 1973 the minmax problem was solved without precedence constraints. Jackson (1955) showed that ordering by due date minimizes maximum lateness. Moore (1968, Management Science 15(1)) gave a procedure for general nondecreasing deferral costs, and Lawler and Moore (1969) gave a related method. In Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, Lawler showed that arbitrary precedence constraints can be added at no loss of efficiency. Jobs are chosen from last to first, by a single comparison of costs at a known time. The resulting $O(n^2)$ procedure is the standard algorithm for the problem written $1\,|\,\mathrm{prec}\,|\,f_{\max}$ in the classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979). It is one of the first polynomial-time results for precedence-constrained scheduling that every survey of the field cites.

Setting

A finite, nonempty set $J$ of jobs is processed on a single machine, one job at a time and without interruption. Each job $j$ has a processing time $a_j \ge 0$ and a cost function $c_j : \mathbb{R} \to \mathbb{R}$ that is monotone nondecreasing. The value $c_j(t)$ is the cost incurred when $j$ is completed at time $t$.

The precedence constraints are an arbitrary relation $\prec$ on jobs: $i \prec j$ means that job $i$ is required to precede job $j$. A sequence $\pi = (\pi_1, \dots, \pi_n)$ lists every job of $J$ once. It observes the precedence constraints if $\pi_q \prec \pi_p$ never holds for positions $p < q$. The machine starts at time $0$ with no idle time, so the completion time of $\pi_m$ is $C_{\pi_m}(\pi) = a_{\pi_1} + \dots + a_{\pi_m}$. The maximum incurred cost of $\pi$ is

$$f_{\max}(\pi) = \max_{j \in J} c_j\bigl(C_j(\pi)\bigr),$$

and a feasible $\pi$ is minmax optimal if $f_{\max}(\pi) \le f_{\max}(\pi')$ for every feasible $\pi'$.

For a set $P$ of jobs, $S(P)$ is the set of jobs of $P$ that are not required to precede any other job of $P$, and $T_P = \sum_{j \in P} a_j$. Lawler's rule builds a sequence from the last position to the first. With $P$ the jobs not yet placed, it chooses $k \in S(P)$ with $c_k(T_P) = \min_{j \in S(P)} c_j(T_P)$, places $k$ in the latest open position and removes it from $P$. Ties are broken arbitrarily. In Lean the objects are IsFeasible, lastEligible ($S$), IsMinmaxOptimal and IsLawlerSequence, in namespace LawlerPrec.MinMax. They are built on the published MooreLateJobs.Shared.completionTime and MooreLateJobs.MaxDeferral.maxCost.

Formalization targets

Goal: the rule is optimal

Every sequence $\pi$ that Lawler's rule can produce, under any tie-breaking, observes the precedence constraints and satisfies

$$f_{\max}(\pi) \;\le\; f_{\max}(\pi') \qquad \text{for every sequence } \pi' \text{ of } J \text{ observing the precedence constraints.}$$

This is the statement of §3 (p. 545), "An efficient algorithm for finding a minmax optimal sequence follows immediately from the theorem above". It contains no constants.

Milestones

1. §2 proof, third paragraph. Moving a job of $S(J)$ to the end of a feasible sequence keeps it feasible.
2. §2 proof, fourth paragraph, first sentence. After that move, no job other than $k$ completes later, and $k$ completes at $T = \sum_{j \in J} a_j$.
3. §2 proof, fourth paragraph. If $c_k(T) \le c_{k'}(T)$, where $k'$ is the last job of the feasible sequence, the move does not raise $f_{\max}$.
4. THEOREM (§2), p. 544. If some feasible sequence exists and $k \in S(J)$ minimizes $c_j(T)$ over $S(J)$, then some minmax optimal sequence has $k$ last.
5. §3, the reduction. A minmax optimal sequence of $J \setminus \{k\}$, followed by $k$, is minmax optimal for $J$.
6. §3, the procedure never stalls. If a feasible sequence exists, the rule produces a complete sequence. This shows the goal is not vacuous.

Significance

The result shows that $1\,|\,\mathrm{prec}\,|\,f_{\max}$ is solvable in polynomial time for every family of nondecreasing costs. The ordering of an optimal sequence depends on the costs only through their values at the $n$ partial sums $T_P$ along the way. The deadline problem is a corollary (§5): sequencing from last to first by latest deadline among the currently available jobs avoids tardiness whenever any sequence does. The last-to-first scheme is reused in later backward rules for $f_{\max}$ objectives. A formal statement of the rule, its feasibility and its optimality makes these extensions available for formal reuse.

The result is classical and its proof is short. No machine-checked proof of it is known to be in Mathlib. The work this mission asks for is a formal proof of the known exchange argument and of the induction that turns the Theorem into the algorithm's correctness. The induction needs the reduced problem's sets $S(P)$ and times $T_P$ to be the correct ones at each stage, which the definitions fix.

Difficulty

The exchange argument of §2 is elementary. The difficulty lies in stating the algorithm faithfully and carrying the induction. At each stage the eligible set $S(P)$ and the time $T_P$ must be recomputed on the remaining jobs, with constraints into already placed jobs ignored. The induction must also show that the rule's sequence is feasible, which is a conclusion and not an assumption.

A first attempt often proves only the Theorem, that some optimal sequence has $k$ last. That statement says nothing about a sequence built entirely by the rule, because an optimal sequence of $J$ with $k$ last need not restrict to an optimal sequence of $J \setminus \{k\}$. Optimality of the rule's whole sequence is the target, and milestone 5 isolates the corresponding step of the page.

Formalization scope

• Jobs form a type ι with decidable equality, and the job set is J : Finset ι.
• Processing times are a : ι → ℝ, costs are c : ι → ℝ → ℝ, and the precedence constraints are prec : ι → ι → Prop.
• A sequence is a duplicate-free list whose elements are exactly J. Positions are 0-based, and completion times are prefix sums (MooreLateJobs.Shared.completionAt).
• The relation prec is arbitrary: it is not assumed transitive, irreflexive or acyclic. A cycle among distinct jobs leaves no feasible sequence. A self-loop constrains nothing, both in feasibility and in $S$ (the "others" of the page exclude the job itself).

The standing assumptions of §1 appear as hypotheses wherever they are used: monotone nondecreasing $c_j$ for $j \in J$, and $J$ nonempty where the maximum is taken. Two hypotheses are added relative to the page and disclosed in each statement. Processing times are non-negative ($a_j \ge 0$), since they are durations and the exchange argument fails without them. The Theorem also assumes the existence of a feasible sequence, which its conclusion presupposes.

The rule is the property IsLawlerSequence of a finished sequence. At each position $m$, the job there lies in $S$ of the jobs in positions $0..m$ and minimizes the cost at their total processing time. Every tie-break is covered. The rule is not a deterministic function, and it is not an arbitrary choice function. Feasibility of the rule's output is part of the goal's conclusion, so the goal cannot be obtained by assuming it. A statement that compares the rule only with some sequence, or that asserts only that an optimal sequence exists, is weaker and is ruled out by the goal's form. Milestone 6 shows the goal's hypotheses are satisfiable whenever a feasible sequence exists.

The $n^2$ operation count of §4, the first-to-last rule of §5 and the deadline corollaries of §5 are not part of this mission. A development needs only finite lists and finsets from Mathlib. Lemmas about moving an element to the end of a duplicate-free list, and about prefix sums under that move, are reusable for other exchange arguments in single-machine scheduling.

Selected references

• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5):544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• E. L. Lawler and J. M. Moore, A Functional Equation and its Application to Resource Allocation and Sequencing Problems, Management Science 16(1):77–84, 1969. https://doi.org/10.1287/mnsc.16.1.77
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• R. L. Graham, E. L. Lawler, J. K. Lenstra and A. H. G. Rinnooy Kan, Optimization and Approximation in Deterministic Sequencing and Scheduling: a Survey, Annals of Discrete Mathematics 5:287–326, 1979. https://doi.org/10.1016/S0167-5060(08)70356-X

Motivation

Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).

The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio $O(\log m \log n)$, where $n$ is the number of elements and $m$ the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).

This mission formalizes the core of the weighted result: the algorithm that is given a value $\alpha$ at least the optimal cost, and its guarantee (Theorem 3.4).

Setting

The ground set $X$ has $n = |X|$ elements and the family $\mathcal S$ has $m = |\mathcal S|$ sets; every set $S$ has a cost $c_S > 0$. Both are known to the algorithm in advance. For an element $j$, $\mathcal S_j$ denotes the sets containing $j$. Elements of an unknown subset of $X$ arrive one at a time in a sequence $\sigma$; on arrival each must be covered by a chosen set. The chosen family $\mathcal C$ can only grow. $\mathcal C_{OPT}$ is any family covering every arriving element, and $c(\mathcal C_{OPT}) = \sum_{S \in \mathcal C_{OPT}} c_S$.

The algorithm is given $\alpha \ge c(\mathcal C_{OPT})$. It discards sets costing more than $\alpha$, buys sets costing at most $\alpha/m$ outright, and rescales costs; on the resulting normalized instance $1 \le c_S \le m$ and $c_S \le \alpha$ for every set (p. 365).

The algorithm keeps a weight $w_S > 0$ for every set, initially $w_S = 1/m^2$; the weight of an element is $w_j = \sum_{S \in \mathcal S_j} w_S$. With $C$ the set of covered elements and $\chi_{\mathcal C}$ the indicator of $\mathcal C$, the potential is

$$\Phi = \sum_{j \notin C} n^{2 w_j} + n \cdot \exp\Big(\frac{1}{2\alpha} \sum_{S \in \mathcal S} \big(c_S \chi_{\mathcal C}(S) - 3 w_S c_S \log n\big)\Big),$$

with natural logarithms throughout. When $j$ arrives with $w_j \ge 1$ nothing happens; otherwise the algorithm performs weight augmentation steps while $w_j < 1$. In a step, for each $S \in \mathcal S_j$: (a) $w_S \leftarrow w_S (1 + \frac{1}{n c_S})$; (b) if $S \notin \mathcal C$, add $S$ to $\mathcal C$ when $\Phi$ does not exceed its value before (a); (c) if $\Phi$ has increased, return FAIL.

In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.

Formalization targets

Goal: Theorem 3.4

On the normalized instance, with $\mathcal C_{OPT}$ covering $\sigma$, $c(\mathcal C_{OPT}) \le \alpha$, and $n \cdot n^{2/m} + n < n^2$, every reachable configuration is a running state (never FAIL) in which (i) every $j \in X$ with $w_j \ge 1$ is covered, and (ii)

$$\sum_{S \in \mathcal C} c_S \le 3 \log n \Big(1 + \Big(1 + \frac1n\Big)\alpha \log\Big(m^2\Big(1+\frac1n\Big)\Big)\Big) + 2\alpha \log n = (6 + o(1))\,\alpha \log m \log n.$$

Milestones

• Lemma 3.1 (p. 365): the number $N$ of augmentation steps satisfies $N \le \sum_{S \in \mathcal C_{OPT}} (n c_S + 1)\log(m^2(1 + 1/n)) \le (n+1)\alpha\log(m^2(1+1/n))$.
• Lemma 3.2 (p. 366): throughout, $\sum_S w_S c_S \le 1 + N/n \le 1 + (1 + 1/n)\alpha\log(m^2(1+1/n))$.
• Lemma 3.3 (p. 366): a per-set step with $c_S \le \alpha$ never increases $\Phi$; in particular the algorithm never fails.

The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant $\Phi < n^2$ assumed) is included as a supporting reference.

Significance

Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of $\alpha$ described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic $O(\log m \log n)$-competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.

The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant $\Phi < n^2$ to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis $c_S \le \alpha$. Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the $o(1)$ terms replaced by explicit expressions.

Difficulty

The cost bound in the last step is short once two facts about the run are available: that $\Phi$ stays below $n^2$, and that the fractional cost $\sum_S w_S c_S$ stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add $S$ or not) does not increase $\Phi$; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most $\alpha$. The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers $n^{2 w_j}$, where the initial bound $\Phi < n^2$ is a genuine size condition on $n$ and $m$.

Formalization scope

The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits $\mathcal S_j$ is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by $\mathcal C_{OPT}$.

Conventions: costs, weights and $\alpha$ are real; $n$ and $m$ are the cardinalities of the finite types cast to $\mathbb R$; $\log$ is Real.log; $n^{2 w_j}$ and $n^{2/m}$ are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:

• Lemma 3.1: $(2 + o(1)) n\alpha\log m$ becomes $(n+1)\alpha\log(m^2(1+1/n))$;
• Lemma 3.2: $(2 + o(1))\alpha\log m$ becomes $1 + (1+1/n)\alpha\log(m^2(1+1/n))$, together with the intermediate bound $1 + N/n$;
• Theorem 3.4 (ii): $(6 + o(1))\alpha\log m\log n$ becomes $3\log n\,(1 + (1+1/n)\alpha\log(m^2(1+1/n))) + 2\alpha\log n$;
• "n and m large" becomes the hypothesis $n \cdot n^{2/m} + n < n^2$ used for the initial potential (it holds, for instance, when $n \ge 4$ and $m \ge 3$).

The goal is a statement about the configurations the algorithm actually reaches from $w_S = 1/m^2$ and the empty cover. Taking the invariant $\Phi < n^2$ or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown $\alpha$ is not part of this mission.

A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• 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

In the online set cover problem of Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009; preliminary version STOC 2003), a ground set and a family of subsets are known in advance, but the elements that actually need covering arrive one at a time, and each must be covered on arrival by sets chosen irrevocably. The paper's motivating example is a network of servers with activation costs: the set of potential clients is known, the clients that actually request service are not, and each request must be served on arrival.

The paper gives a deterministic online algorithm whose cost is within a factor $O(\log m \log n)$ of the offline optimum, where $n$ is the number of elements and $m$ the number of sets. Its Section 4 shows that this is close to optimal for deterministic algorithms: for all interesting values of $m$ and $n$, every deterministic online algorithm has competitive ratio $\Omega\big(\log n \log m / (\log\log m + \log\log n)\big)$. The lower bound is the reason the $\log m \log n$ product, rather than the $\ln n$ of offline approximation (Feige 1998), is the right target online. The online primal–dual framework that grew out of this paper (Buchbinder and Naor 2009) cites it as the benchmark for online covering problems.

This mission formalizes the exact, non-asymptotic statements behind that lower bound: Propositions 4.1 and 4.2 of the paper.

Setting

A ground set $X$ and a family $\mathcal F$ of distinct subsets of $X$ are fixed and known to the algorithm; $m = |\mathcal F|$. An adversary presents elements $x_1, x_2, \dots$ of $X$ one by one, choosing each after seeing the algorithm's previous responses. A deterministic online algorithm $A$, on the arrival of $x_t$, sees the earlier arrivals $(x_1, \dots, x_{t-1})$ and $x_t$, and adds a finite family $A\big((x_1,\dots,x_{t-1}), x_t\big) \subseteq \mathcal F$ of sets to its collection; sets are never removed. It is valid if after every arrival that lies in some member of $\mathcal F$, that element lies in a chosen set. After an arrival sequence $\sigma$ the chosen collection is $\mathcal C_A(\sigma)$, and since every set has unit cost, the cost is $|\mathcal C_A(\sigma)|$. The offline optimum $\mathrm{OPT}(\sigma)$ is the least number of members of $\mathcal F$ covering the elements of $\sigma$. The competitive ratio of $A$ is at least $\rho$ when some arrival sequence $\sigma$ has $\mathrm{OPT}(\sigma) \ge 1$ and $|\mathcal C_A(\sigma)| \ge \rho\,\mathrm{OPT}(\sigma)$.

Two families are used.

• The bit family: $X = \{0, \dots, 2^k - 1\}$ and $F_i = \{ j : \text{bit } i \text{ of } j \text{ is on}\}$ for $1 \le i \le k$.
• The block family: $k r^2$ disjoint blocks $X_1, \dots, X_{kr^2}$ of $2^k$ elements each; $X_b(t)$ is the set of elements of block $X_b$ whose $t$th bit is on. For an $r$-set $R = \{b_1 < \dots < b_r\}$ of blocks and bit locations $I = (i_1, \dots, i_r)$,

$$F_{R,I} = \bigcup_{t=1}^r X_{b_t}(i_t),$$

and the family consists of all $F_{R,I}$; it has $m = \binom{kr^2}{r} k^r$ members.

Formalization targets

Goal: Proposition 4.2

For all positive integers $k, r$ and all $n, m$ with

$$n \ge 2^{k+1} k r^2, \qquad 2^{2^k k r^2} \ge m \ge \binom{kr^2}{r} k^r,$$

there is a family $\mathcal F$ of exactly $m$ distinct subsets of an $n$-element set such that for every valid deterministic online algorithm $A$ there is a nonempty arrival sequence $\sigma$, covered by a single member of $\mathcal F$, with

$$|\mathcal C_A(\sigma)| \ge kr = kr \cdot \mathrm{OPT}(\sigma).$$

The goal leaves the instance existential, as the paper does, and keeps both bounds on $m$ and the bound on $n$ exactly as printed.

Milestones

1. Proposition 4.1. On the bit family, $|\mathcal F| = k$; every valid deterministic algorithm can be forced to cost $k$ on a sequence with $\mathrm{OPT} = 1$; and some valid algorithm has cost at most $k \cdot |C|$ for every offline cover $C$. So the best deterministic competitive ratio is exactly $k = \log_2 n$.
2. The adversary claim of Section 4 (p. 369). On the block family, every valid deterministic algorithm can be forced to choose $kr$ sets by at most $kr$ arrivals that a single set covers.

A supporting item (not a milestone) records the count $|\mathcal F| = \binom{kr^2}{r} k^r$ of the block family.

Significance

The result. Proposition 4.2 is the exact statement behind the paper's lower bound: choosing $r$ of order $\log m / (\log\log m + \log\log n)$ and $k$ of order $\log n$ turns it into the asymptotic bound $\Omega\big(\log n \log m/(\log\log m + \log\log n)\big)$, which shows that the paper's $O(\log m \log n)$ algorithm is optimal among deterministic algorithms up to a $\log\log m + \log\log n$ factor. Without it, the gap between the $\ln n$ achievable offline and the $\log m \log n$ achieved online would be unexplained. Proposition 4.1 alone gives the matching bound $\log_2 n$ when $m = \log_2 n$.

Formalizing it. Both propositions are proved in the paper; neither is formalized anywhere to our knowledge. The mission produces a reusable model of deterministic online algorithms against an adaptive adversary, with a validity notion and a cost, and machine-checked adversary arguments on it. The paper's proof tacitly lets the algorithm add one set per arrival; the statements here cover algorithms that add any number of sets per arrival, so a complete formalization also closes that gap.

Difficulty

The adversary must be adaptive, and the quantifiers are ordered instance, then algorithm, then arrival sequence. The obvious single-block argument (Proposition 4.1) forces only $k$ sets. To force $kr$ sets with $\mathrm{OPT} = 1$, the adversary must move to blocks that no chosen set has touched yet, which requires counting the blocks touched by the sets chosen so far. When an algorithm adds many sets at once, the paper's count "at most $1 + (r-1)k$ blocks after $k$ steps" no longer applies as written, and the stopping rule has to be phrased in terms of the cost already paid. The padding of Proposition 4.2 must reach exactly $n$ elements and exactly $m$ distinct sets without creating sets that help cover the adversary's elements.

Formalization scope

The ground set is a Fin type: Fin (2^k) for Proposition 4.1, Fin (k r²) × Fin (2^k) (block, element) for the block family, Fin n for Proposition 4.2. A family is a Finset (Finset X), so its cardinality counts distinct sets. Bit $i$ (1-based) of $j$ is Nat.testBit j (i-1). An online algorithm is a function from (earlier arrivals in arrival order, current element) to the finite family of sets it adds; it may add any number of sets. Validity demands coverage only for elements that some member of the family contains. Costs are unit (the problem of Section 4 is unweighted).

The offline optimum is never encoded as an infimum: lower bounds exhibit a nonempty arrival sequence and a single covering set ($\mathrm{OPT} = 1$), and the upper bound of Proposition 4.1 quantifies over all offline covers. This rules out the trivializing reading in which the empty arrival sequence satisfies $\text{cost} \ge kr \cdot \mathrm{OPT}$ as $0 \ge 0$.

The statements contain no $O(\cdot)$: every quantity is the paper's exact one. The asymptotic bound (8) under the range (7), whose final paragraph only sketches the choice of $r$ and $k$, is excluded, as are the remarks on the trivial ratio-$m$ and $O(\sqrt n)$ algorithms.

Contributions welcome: proofs of the milestones; lemmas on the chosen collection (monotonicity, decomposition along a sequence); the count of the block family; and the padding construction of Proposition 4.2. The online-algorithm model is reusable for other deterministic online covering lower bounds.

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
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The online set cover problem, Proc. 35th ACM STOC, 2003, pp. 100–105. https://doi.org/10.1145/780542.780558
• 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

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