Optimization

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let labels take the values $y\in\{-1,+1\}$. The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$. A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$.

Metric (Definition 2). For a weight $\kappa>0$,

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .$$

Changing a label costs $\kappa$; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$, $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$. The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$.

Data. Training samples $(\hat x_i,\hat y_i)$, $i=1,\dots,N$, define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$.

Worst- and best-case risks.

$$\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].$$

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$, a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$, $s,r,t\in\mathbb R^N$, program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$,

$$1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .$$

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$, $\varepsilon\ge0$, $N\ge1$, all samples and every weight vector $\hat\beta$, both programs attain their minima $v$ and $w$, and

$$\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .$$

The identities hold for each fixed $\hat\beta$, so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then for any sample-dependent $\hat\beta$

$$\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,$$ $$\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .$$

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$. Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$. The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$.

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$, $\text{false}\mapsto-1$; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$, and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$.

The following choices differ from a literal reading of the page:

• The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$. This fails on the hyperplane $\langle\beta,x\rangle=0$, where $f_\beta(x)=-1$ is correct for $y=-1$. The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
• The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, as a hypothesis, and "with probability $1-\eta$" is read as "with probability at least $1-\eta$". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$, restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

Motivation

Logistic regression is among the most widely used classification methods in statistics and machine learning. Its maximum-likelihood estimator minimizes the average logloss on the training data and is known to overfit when data are scarce; practitioners respond with ad hoc regularization, typically a norm penalty on the weight vector. Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015, arXiv:1509.09259) replace the empirical average by a worst case over all distributions within a Wasserstein ball around the empirical distribution. The resulting model has a finite convex reformulation, contains classical and norm-regularized logistic regression as special cases, and comes with out-of-sample guarantees. It is one of the early instances of Wasserstein distributionally robust optimization in learning, building on the duality theory of Mohajerin Esfahani and Kuhn (Math. Program. 2018, arXiv:1505.05116); the regularization interpretation was later extended to general losses by Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (JMLR 2019, arXiv:1710.10016).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$ be the dual norm of a weight vector $\beta$. Labels are $y\in\{-1,+1\}$, and the feature-label space is $\Xi = V\times\{-1,+1\}$. The logloss of $\beta$ at $(x,y)$ is

$$l_\beta(x,y) = \log\big(1+\exp(-y\langle\beta,x\rangle)\big).$$

For a label weight $\kappa>0$, the metric of Definition 2 on $\Xi$ is

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 ,$$

so that changing a label costs $\kappa$. The Wasserstein distance $W(\mathbb Q,\mathbb P)$ between probability distributions on $\Xi$ (Definition 1) is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$, and $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$. Given training samples $(\hat x_i,\hat y_i)_{i=1}^N$, the empirical distribution is $\hat{\mathbb P}_N = \frac1N\sum_i\delta_{(\hat x_i,\hat y_i)}$, and the distributionally robust logistic regression problem (6) is

$$\hat J = \inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)} \mathbb E^{\mathbb Q}\big[l_\beta(x,y)\big].$$

Program (7) has variables $\beta$, $\lambda\in\mathbb R$, $s\in\mathbb R^N$, objective $\lambda\varepsilon + \frac1N\sum_i s_i$, and constraints $l_\beta(\hat x_i,\hat y_i)\le s_i$, $l_\beta(\hat x_i,-\hat y_i)-\lambda\kappa\le s_i$ for all $i$, and $\|\beta\|_*\le\lambda$.

Formalization targets

Goal: Theorem 1 (tractable reformulation)

For every $\varepsilon\ge0$, $\kappa>0$, $N\ge1$ and every norm on the feature space,

$$\inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta] \;=\; \inf\Big\{\lambda\varepsilon+\tfrac1N\textstyle\sum_i s_i : (\beta,\lambda,s)\text{ feasible for (7)}\Big\},$$

and for $\varepsilon>0$ the infimum of (7) is attained.

Milestones

1. §3.1 — the feasible set of (7) is convex.
2. §2 — for $\varepsilon=0$ the worst-case expected logloss is the empirical average logloss, so (6) reduces to classical logistic regression (2).
3. Theorem 1 for fixed $\beta$ — $\sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta]$ equals the attained minimum of (7) over $(\lambda,s)$ with $\beta$ fixed.
4. Remark 2, eq. (9) — at an optimal solution $(\hat\beta,\hat\lambda,\hat s)$,

$$\hat J = \hat\lambda\varepsilon + \mathbb E^{\hat{\mathbb P}_N}[l_{\hat\beta}] + \tfrac1N\textstyle\sum_i\max\{0,\hat y_i\langle\hat\beta,\hat x_i\rangle-\hat\lambda\kappa\}.$$

5. Remark 1 — as $\kappa\to\infty$ the optimal value of (7) converges to $\inf_\beta \varepsilon\|\beta\|_* + \frac1N\sum_i l_\beta(\hat x_i,\hat y_i)$.
6. Theorem 2, implication — if $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then $\mathbb P^N\{\mathbb E^{\mathbb P}[l_{\hat\beta}]\le\hat J\}\ge1-\eta$.

Significance

Theorem 1 turns a minimax problem over an infinite-dimensional family of distributions into a finite convex program whose size grows linearly in $N$; with the $\ell_1$, $\ell_2$ or $\ell_\infty$ norm it is a standard exponential-cone or conic program. Remark 1 explains norm-regularized logistic regression as a distributionally robust model: the regularizer is the dual norm of the transport cost on features, and the regularization weight is the radius of the ambiguity set. Remark 2 exposes an additional term that accounts for label noise and vanishes as label changes become prohibitively expensive. Theorem 2 makes the optimal value $\hat J$ a certificate on the out-of-sample logloss whenever the ball contains the true distribution.

The paper's proofs are in a technical appendix and have not been machine-checked. Mathlib contains no Wasserstein distributionally robust duality. This mission produces a formal statement of the reformulation with an arbitrary norm and a label-dependent cost, together with formal versions of the paper's printed consequences of it (Remarks 1 and 2, the $\varepsilon=0$ reduction, and the implication in Theorem 2).

Difficulty

The worst-case expectation ranges over every Borel probability distribution within transport distance $\varepsilon$ of the empirical distribution, including distributions with unbounded support and distributions that move mass across labels. Exhibiting good distributions in the ball shows only that the robust value is at least the value of (7); the reverse inequality must control every distribution in the ball at once, and nothing in the definition of the ball bounds its elements' supports. The obvious simplification, restricting attention to distributions supported on finitely many points, again yields only a one-sided bound unless the supremum is shown to be approached by such distributions. The label term of the metric couples the two label classes, so results for a pure norm cost on the features do not apply directly, and the dual norm enters through an arbitrary norm rather than the Euclidean one.

Formalization scope

• The feature space is an abstract finite-dimensional real normed space V standing for $(\mathbb R^n,\|\cdot\|)$ with an arbitrary norm; weights are continuous linear functionals V →L[ℝ] ℝ, and $\|\beta\|_*$ is their operator norm, which is exactly the dual norm. Labels are Bool, embedded as $\pm1$; the label $-y$ is Boolean negation. The metric of Definition 2 is written literally.
• The Wasserstein distance is of type 1, valued in $[0,\infty]$, with couplings ranging over all probability measures on $\Xi\times\Xi$ with the two prescribed marginals. The ball consists of probability measures.
• Expectations of the positive logloss are lower Lebesgue integrals in $[0,\infty]$, and the supremum over the ball is taken there; the optimal value of (7) is the infimum of its (nonnegative) objective over the feasible set, also in $[0,\infty]$. A Bochner integral, which vanishes on non-integrable functions, would make the worst case trivially finite and is not used.
• The standing hypotheses are $\kappa>0$, $\varepsilon\ge0$, $N\ge1$.
• Correction. The paper prints "min" in (7) for all $\varepsilon\ge0$. At $\varepsilon=0$ the minimum can fail to be attained ($V=\mathbb R$, $N=1$, $\hat x_1=1$, $\hat y_1=+1$: the value is $0$ but every feasible point has positive objective). The goal states the value identity for $\varepsilon\ge0$ and attainment for $\varepsilon>0$.
• Remark 1 is formalized as convergence of optimal values as $\kappa\to\infty$; a metric with $\kappa=\infty$ is not formalized. Only convexity, not tractability, of (7) is stated. The first claim of Theorem 2 (the radius (8) and the light-tail assumption) is not formalized; the confidence of the ball event is a hypothesis of milestone 6.
• A formalization in which the ball is taken only over distributions supported on the training samples, or in which the label term of the metric is dropped, trivializes the second constraint group of (7) and is ruled out: the ball here contains every Borel probability distribution on $\Xi$ within the prescribed distance.
• Infrastructure needed and reusable beyond this mission: type-1 optimal transport on product spaces with a label component, couplings and their marginals, and elementary properties of the logloss as a function of $\beta$. Contributions of such supporting lemmas as independent theorems are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://arxiv.org/abs/1509.09259
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://arxiv.org/abs/1505.05116
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://arxiv.org/abs/1312.2128
• S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Regularization via Mass Transportation, Journal of Machine Learning Research 20 (2019). https://arxiv.org/abs/1710.10016

Motivation

Set covering asks for the fewest members of a family of sets whose union is everything the family covers. It models crew scheduling, facility siting, test-suite reduction, logic minimization and fault testing; Johnson names the last two as its practical applications. Karp showed in 1972 that the decision version is NP-complete (Karp 1972), so in practice one runs a heuristic and asks how far from optimal it can be.

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (JCSS 9, 256–278) is one of the founding papers of the worst-case analysis of approximation algorithms. For set covering it analyses the obvious greedy rule, repeatedly take a set that covers the most still-uncovered points, and proves that on families whose sets have at most $k$ elements its output is never more than the harmonic number $H(k) = \sum_{j=1}^k 1/j$ times the optimum, and that this factor is attained.

Timeline.

• 1974: Johnson proves the $H(k)$ bound for unweighted set cover with sets of size at most $k$, together with a matching family of examples (this mission).
• 1975: Lovász proves the same bound for the fractional relaxation, giving an integrality-gap statement (Lovász 1975).
• 1979: Chvátal extends the bound to weighted set cover, with the greedy rule choosing the set of least cost per newly covered point (Chvátal 1979).
• 1998: Feige shows that no polynomial-time algorithm achieves $(1-\varepsilon)\ln n$ unless NP has slightly superpolynomial deterministic algorithms (Feige 1998), so the greedy guarantee is essentially the best possible.

Setting

An input $F$ of SET COVERING I is a finite family $\{S_1, \dots, S_p\}$ of finite sets. The set to be covered is $T = \bigcup_{S \in F} S$. A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S \in F'} S = T$, and its measure is $|F'|$. The optimum $F^*$ is the minimum measure of a subcover; $F$ itself is a subcover, so the minimum exists. The subproblem SC(k) restricts the inputs to families no set of which has more than $k$ elements.

Algorithm C1 keeps a family SUB of chosen sets, the set UNCOV of uncovered points, and an array SET$[i]$ holding the still-uncovered part of $S_i$. It starts with SUB $= \emptyset$, UNCOV $= T$, SET$[i] = S_i$. While UNCOV is nonempty it chooses an index $j$ with $|\mathrm{SET}[j]|$ maximal, adds $S_j$ to SUB, and removes SET$[j]$ from UNCOV and from every SET$[i]$. When UNCOV is empty it returns SUB. When several indices tie at Step 3 any of them may be chosen, so one input can have several choosable outputs. Following Section 2 of the paper, the algorithm's value $C1(F)$ is the worst choosable output, here the largest, and the ratio is $r(C1, F) = C1(F)/F^*$.

For the proof the paper introduces configurations $K = \langle N_K, \mathrm{UNCOV}_K, \langle \mathrm{SET}_K[1], \dots, \mathrm{SET}_K[N_K]\rangle\rangle$ with $\bigcup_i \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$, runs from a configuration (sequences of admissible choices ending when UNCOV is empty), $\mathrm{Numbers}(R)$, the set of indices chosen in a run $R$, and calls a set $M$ selectable from $K$ if $M = \mathrm{Numbers}(R)$ for some run $R$ from $K$. Write $n(K, i) = |\mathrm{SET}_K[i]|$.

Formalization targets

Goal: Theorem 4

For every $k \ge 1$:

$$\text{for every input } F \in SC(k) \text{ and every choosable } F_1:\quad |F_1| \le H(k)\cdot F^*,$$ $$\text{and some } F \in SC(k) \text{ with } F^* > 0 \text{ has a choosable } F_1 \text{ with } |F_1| = H(k)\cdot F^*.$$

The paper states this as $R[C1, SC(k)](n) \le \sum_{j=1}^k (1/j)$ for all $n > 0$, with equality for all sufficiently large $n$. The two-part form above is the size-free equivalent.

Milestones

1. Lemma 1. For a subcover $F_1$ with index set $M1 = \{i : S_i \in F_1\}$ and $K$ the configuration after Step 1: $F_1$ is choosable by C1 if and only if $M1$ is selectable from $K$.
2. Lemma 2. For any configuration $K$, any $M1$ selectable from $K$ and any $M0$ with $\bigcup_{i \in M0} \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$:

$$|M1| \le \sum_{i \in M0} \sum_{j=1}^{n(K,i)} \frac{1}{j}.$$

3. Fig. 1. For every $k \ge 1$ there is an explicit input of $SC(k)$ on $k \cdot k!$ points with $F^* = k!$ and a choosable output of $k!\,H(k)$ sets.

Significance

The result. Theorem 4 is the first proof that greedy set cover has a worst-case guarantee depending only on the largest set size, and it pins the guarantee down exactly: the constant $H(k)$ cannot be lowered for any $k$. Since $H(k) \le 1 + \ln k$, it also gives the well-known $1 + \ln n$ bound for general inputs. The $H(k)$ bound and its later refinements are the standard reference point for analyses of greedy covering, dual fitting and submodular covering.

Formalizing it. The theorem has been proved since 1974. As far as a search of the platform shows, no machine-checked proof of it exists: the platform holds a Kearns–Vazirani-style statement ComputationalLearning.greedy_set_cover (the $\mathrm{opt}\cdot\ln|U|$ form for a greedy sequence, still open) and a dual-fitting certificate lemma for weighted set cover, neither of which covers the $SC(k)$ bound, the tie-breaking semantics or the tightness construction. A complete development provides both halves of Theorem 4, the configuration and run machinery of Lemmas 1–2, and the explicit Fig. 1 family.

Difficulty

The obvious argument charges each chosen set to the points it newly covers and compares the charges with an optimal cover. A statement about the initial input alone, with the original sizes of the optimal sets, does not survive a single greedy step: after a step the optimal sets are only partly uncovered and the remaining run faces a different instance. This is why Lemma 2 is stated for an arbitrary configuration, in terms of the current sizes $n(K, i)$, and for an arbitrary covering subfamily $M0$. Because Step 3 breaks ties arbitrarily, the statement must hold for every admissible run, and a formalization that fixes one tie-breaking rule proves a weaker upper bound and cannot express the tightness example, which relies on adversarial ties at every stage.

For the tightness half, the difficulty is bookkeeping: showing that the $k!/j$ blocks of each segment are admissible choices at each stage and that no cover uses fewer than $k!$ sets.

Formalization scope

• An input is an indexed family S : ι → Finset α over a finite index type ι and a ground type with decidable equality. The indices play the role of $1, \dots, N$; two indices may carry the same set, which only widens the input class. The family, subcovers and $F^*$ are taken over the set of sets family S, as on the page. $F^*$ is a Finset.inf' over the nonempty finite set of subcovers; if $T = \emptyset$ then $F^* = 0$.
• C1 is a nondeterministic step relation: a step is allowed for every index maximizing $|\mathrm{SET}[j]|$. An output is choosable if a finite chain of steps from the initial state reaches a halting state with that SUB. No tie-breaking rule is fixed.
• The paper's $R[A, P](n)$ is a maximum over inputs of size at most $n$ in an unspecified notation; it is replaced by the size-free two-part statement above, which is equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$.
• Ratios are stated multiplicatively in $\mathbb{Q}$ ($|F_1| \le H(k)\cdot F^*$), never as a quotient, so an input with $F^* = 0$ does not make the bound vacuous, and the attainment part requires $F^* > 0$. $H(k)$ is Mathlib's harmonic k.
• Configurations carry the covering condition as a field; runs are an inductive predicate on the list of chosen indices; Selectable K M means $M$ is the set of indices of some run.
• Lemma 1 assumes the family's sets are pairwise distinct (the paper's family is a set of sets); without that the index set $\{i : S_i \in F_1\}$ may contain a duplicate index C1 never chose.
• Trivializing formalizations are ruled out: a deterministic tie-break, a ratio written as a division, the original set sizes in place of $n(K, i)$ in Lemma 2, or an attaining input with $F^* = 0$ would each change the theorem.

Contributions welcome: proofs of Lemma 2 (the core induction), of Lemma 1, of the Fig. 1 run, and of Theorem 4 from these; the configuration/run layer and the Fig. 1 family are reusable for other greedy covering analyses.

Selected references

• David S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• Richard M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• László Lovász, On the ratio of optimal integral and fractional covers, Discrete Mathematics 13 (1975), 383–390. https://doi.org/10.1016/0012-365X(75)90058-8
• Vašek Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233
• Uriel Feige, A threshold of ln n for approximating set cover, Journal of the ACM 45 (1998), 634–652. https://doi.org/10.1145/285055.285059

Motivation

Many problems in scientific computing and statistics ask for a solution of a linear system $Ax\approx b$ that uses as few unknowns as possible. In statistics this is subset selection (Golub and Van Loan, Matrix Computations, 1983). In coding theory over binary matrices it is the minimum weight solution problem (Gallager, 1968). Natarajan's own motivation was radial basis interpolation (Hardy, 1988). There the coefficients of the interpolant solve a square nonsingular linear system (Michelli, 1986). Few nonzero coefficients make the interpolant cheap to evaluate and, by Occam's razor, less prone to fitting noise.

Natarajan's paper (SIAM J. Comput. 24 (1995) 227–234) makes two contributions. First, finding the sparsest approximate solution over the reals is NP-hard (Theorem 1, the subject of the companion mission). Second, the obvious greedy heuristic, a QR factorization whose column pivots are chosen by their correlation with the right-hand side, is provably good (Theorem 2). This mission formalizes Theorem 2. The greedy method is known today as orthogonal least squares (OLS), a variant of orthogonal matching pursuit. Natarajan's bound is among the earliest worst-case guarantees for this family of algorithms and is widely cited in the sparse approximation and compressed sensing literature.

Setting

Let $A\in\mathbb R^{m\times n}$ have columns $a_1,\dots,a_n$, let $b\in\mathbb R^m$ and $\varepsilon>0$. Write $\|\cdot\|_2$ for the Euclidean norm and $\|x\|_0$ for the number of nonzero entries of $x$. The sparse approximate solution problem asks for $x$ with $\|Ax-b\|_2\le\varepsilon$ and $\|x\|_0$ minimal. Define

$$\operatorname{Opt}(\delta)=\min\{\|x\|_0 : \|Ax-b\|_2\le\delta\}.$$

Let $\mathbf A$ be $A$ with every column divided by its Euclidean norm. Let $\mathbf A^+$ be its Moore–Penrose pseudo-inverse, the unique matrix $P$ with $\mathbf AP\mathbf A=\mathbf A$, $P\mathbf AP=P$ and $\mathbf AP$, $P\mathbf A$ symmetric. Let $\|\mathbf A^+\|_2$ be its spectral norm, the $\ell_2\to\ell_2$ operator norm.

Algorithm Greedy keeps a working matrix $A^{(r)}$ with columns $a^{(r)}_j$, a working vector $b^{(r)}$ and a set $\tau$ of chosen indices. It starts from $A^{(0)}=\mathbf A$, $b^{(0)}=b$, $\tau=\emptyset$. While $\|b^{(r)}\|_2>\varepsilon$, it chooses an index $k\notin\tau$ that maximizes $|a_k^{(r)T}b^{(r)}|$ and replaces $b^{(r)}$ by its projection onto the orthogonal complement of $a^{(r)}_k$. It adds $k$ to $\tau$ and replaces every column outside $\tau$ by its normalized projection onto that complement. If every correlation $a_j^{(r)T}b^{(r)}$ vanishes, the algorithm stops ("no solution exists"). A final solution phase solves the linear system $Bx=b^{(0)}-b^{(r)}$ in the chosen columns $B$ of $A$. The number of nonzero entries of the output is therefore at most the number $t$ of selection iterations.

Formalization targets

Goal: Theorem 2, for $A$ with linearly independent columns

If the columns of $A$ are linearly independent and some $x$ satisfies $\|Ax-b\|_2\le\varepsilon/2$, then every run of the selection phase, with any tie-breaking, performs

$$t\le\Big\lceil 18\,\operatorname{Opt}(\varepsilon/2)\,\|\mathbf A^+\|_2^2\,\ln\frac{\|b\|_2}{\varepsilon}\Big\rceil$$

iterations. The paper prints the theorem without the independence hypothesis. The hypothesis is needed (see Formalization scope).

Milestones

The proof on pp. 230–233 passes through the following statements, in order:

1. (12): some column satisfies $|a_j^{(r)T}b^{(r)}|\ge\|b^{(r)}\|_2^2/(2\sqrt{N^{(r)}}\|u^{(r)}\|_2)$. Here $u^{(r)}$ is a sparsest vector with $\|A^{(r)}u^{(r)}-b^{(r)}\|_2\le\varepsilon/2$ and $N^{(r)}=\|u^{(r)}\|_0$.
2. (18): $\|b^{(r+1)}\|_2^2\le(1-1/\rho)\|b^{(r)}\|_2^2$ whenever $\rho\ge 4N^{(r)}\|u^{(r)}\|_2^2/\|b^{(r)}\|_2^2$.
3. Lemma 1: $t\le\lceil2\rho\ln(\|b\|_2/\varepsilon)\rceil$ for any such $\rho$ valid at every iteration.
4. Lemma 3: $N^{(r+1)}\le N^{(r)}\le N^{(0)}$.
5. $N^{(0)}=\operatorname{Opt}(\varepsilon/2)$.
6. The columns of $\mathbf A$ indexed by the support $\sigma$ of $u^{(r)}$ and by the chosen set $\tau$ are linearly independent, and $\sigma\cap\tau=\emptyset$.
7. (31): $\|u^{(r)}\|_2\le\frac32\|Z^+\|_2\|b^{(r)}\|_2$ for the matrix $Z$ of those columns.
8. The singular-value comparison $\|Z^+\|_2\le\|M^+\|_2$ for a column submatrix $Z$ of a matrix $M$ with independent columns.
9. Lemma 2: $\|u^{(r)}\|_2\le\frac32\|\mathbf A^+\|_2\|b^{(r)}\|_2$, for $A$ with independent columns.

Items 1–7 hold for every matrix $A$. Items 8, 9 and the goal carry the independence hypothesis.

Significance

Theorem 2 is a bicriteria approximation guarantee for an NP-hard problem. The greedy output meets the error $\varepsilon$ with at most a factor $18\|\mathbf A^+\|_2^2\ln(\|b\|_2/\varepsilon)$ more nonzeros than the best solution at error $\varepsilon/2$. The factor depends only on the conditioning of the normalized matrix and logarithmically on the required accuracy. Its structure follows Johnson's analysis of the greedy set cover algorithm (1974): a potential decreases by a constant factor per step, which gives a logarithmic number of steps. The intermediate facts (12), (18) and Lemma 1 are the template of many later analyses of matching pursuit and OLS.

The result is proved on paper, with a gap. The last step of the proof of Lemma 2 compares singular values of a submatrix with those of $\mathbf A$, and this comparison holds only when $\mathbf A$ has full column rank. For general $A$, Theorem 2 and Lemma 2 are false as printed. The formalization produces a machine-checked proof of the corrected theorem and pins down exactly where the hypothesis enters. The hypothesis-free statements (12), (18), Lemma 1, Lemma 3 and (31) form reusable infrastructure for greedy sparse approximation. No existing formalization of this algorithm or of its guarantee, in Lean or elsewhere, was found for this mission.

Difficulty

Each step of the proof is short, but the objects are defined by an iteration. The columns $a^{(r)}_j$ are repeatedly projected and renormalized, and the columns already chosen are left untouched. Every claim about iteration $r$ therefore needs invariants: chosen columns are orthonormal and orthogonal to $b^{(r)}$, and the remaining columns are normalized projections of the original ones onto the orthogonal complement of the chosen ones. A proof has to establish these by induction before any lemma can be applied. The sparsest vector $u^{(r)}$ is defined by minimality, so Lemma 3 and the linear-independence claim are exchange arguments on supports rather than computations. Finally, the passage from (31) to Lemma 2 needs a quantitative fact about pseudo-inverses of column submatrices. Mathlib has neither the Moore–Penrose inverse of a rectangular matrix nor its norm as a reciprocal singular value.

A naive attempt to bound $\|u^{(r)}\|_2$ directly by $\|\mathbf A^+\|_2\|A^{(r)}u^{(r)}\|_2$ fails: $u^{(r)}$ multiplies the projected columns $A^{(r)}$, not $\mathbf A$, and different sparsest solutions can have different norms.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m), so every $\|\cdot\|_2$ is the Euclidean norm. The only $\|\cdot\|_\infty$ is the maximum of $|a_j^{(r)T}b^{(r)}|$, which is written out explicitly. The algorithm is a recursion greedyState A b k r in the sequence of choices k : ℕ → Fin n. A run of $t$ iterations (IsGreedyRun) requires, at each $r<t$: the strict while-condition $\|b^{(r)}\|_2>\varepsilon$, an unchosen index, a nonzero correlation, and maximality over the unchosen columns. The residual and the columns are computed, never assumed. Normalization sends $0$ to $0$, so a column lying in the span of the chosen ones stays zero and is never chosen. $\operatorname{Opt}$ is an infimum over ℕ, and the goal assumes that some $x$ has $\|Ax-b\|_2\le\varepsilon/2$, since otherwise the infimum would be $0$. The ceiling is the natural-number ceiling. It agrees with the printed one whenever the loop runs at least once, because then $\|b\|_2>\varepsilon$. The pseudo-inverse is any matrix satisfying the four Penrose equations. It is never defined as $(\mathbf A^T\mathbf A)^{-1}\mathbf A^T$, which would hide the rank assumption.

Added hypothesis. The goal, Lemma 2 and the singular-value step assume that the columns of $A$ are linearly independent, which forces $n\le m$. Without it, Theorem 2 fails. Take $m=2$, $n=200$, columns $(\cos\theta_j,\sin\theta_j)$ and $(\sin\theta_j,\cos\theta_j)$ for 100 distinct $\theta_j\in[0.001,0.01]$, $b=\sqrt2(1,1)$ and $\varepsilon=1$. Then $\operatorname{Opt}(1/2)=2$ and the bound evaluates to $1$, but Greedy selects two columns. Lemma 2 fails for $\mathbf A=[e_1,e_2,(e_1+e_2)/\sqrt2]$ and $b=\beta(-1,1)/\sqrt2$. The paper's motivating interpolation systems are square and nonsingular, so they satisfy the hypothesis. A hypothesis-free goal would replace $\|\mathbf A^+\|_2$ by the largest $\|Z^+\|_2$ over linearly independent column subsets $Z$ of $\mathbf A$, which is what (31) gives. That quantity is not printed in the paper, so it is not the goal here.

A statement in which the iterates are free sequences constrained by hypotheses, the greedy choice is dropped, or $\operatorname{Opt}$ is taken over an empty set would be trivially true or would not describe this algorithm. The encoding above rules these out.

A complete development needs Gram–Schmidt-type invariants of the iteration, exchange arguments for sparsest solutions, and the Moore–Penrose inverse with its spectral norm. The last of these is reusable well beyond this mission. Contributions of any milestone, of the general Penrose-inverse facts, or of alternative proofs are welcome.

Selected references

• B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM J. Comput. 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
• G. H. Golub and C. F. Van Loan, Matrix Computations, Johns Hopkins University Press, 1983.
• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9:256–278, 1974. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. Penrose, A generalized inverse for matrices, Proc. Cambridge Philos. Soc. 51:406–413, 1955. https://doi.org/10.1017/S0305004100030401

Motivation

Maximum satisfiability asks for a truth assignment satisfying as many clauses of a propositional formula as possible. The paper notes that the restriction $MS(k)$, in which every clause has at least $k$ literals, is polynomial complete for every $k \ge 1$, so exact optimization is out of reach in general and one asks instead how close a fast algorithm is guaranteed to come. David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 256–278) set up a framework for exactly this question — optimization problems, nondeterministic approximation algorithms, and the worst-case ratio between the optimum and the algorithm's output — and applied it to subset-sum, maximum satisfiability, set covering, graph coloring and maximum clique. It is one of the founding papers of the theory of approximation algorithms.

Section 4 of the paper treats maximum satisfiability with two algorithms. This mission covers the first, a greedy literal-selection rule called B1, and its exact worst-case ratio (Theorem 2). A companion mission covers the weighted algorithm B2 (Theorem 3).

Timeline, for orientation:

• 1971–1972: Cook and Karp establish NP-completeness of satisfiability and of many combinatorial problems.
• 1974: Johnson proves that B1 has worst-case ratio exactly $(k+1)/k$ on $MS(k)$ and that the weighted algorithm B2 achieves $2^k/(2^k-1)$ (Theorems 2 and 3).
• 1990s: semidefinite and LP-based algorithms (Goemans–Williamson, SIAM J. Discrete Math. 1994) improve the constants for general MAX-SAT.

Setting

Let $L = \bigcup_{i>0}\{x_i, \bar x_i\}$ be the set of literals; the complement of $x_i$ is $\bar x_i$ and conversely. A clause is a finite set $C \subseteq L$. A truth assignment is a set $T \subseteq L$ containing no complementary pair $\{x_i, \bar x_i\}$; it may leave variables unassigned. $T$ satisfies $C$ if $C \cap T \ne \emptyset$.

An input is a finite set $S$ of clauses. Its feasible solutions are the subsets $S' \subseteq S$ satisfied by a single truth assignment, measured by $|S'|$, and the optimum is

$$S^* = \max\{|S'| : S' \subseteq S,\ \text{some truth assignment satisfies every } C \in S'\}.$$

The subproblem $MS(k)$ admits only inputs whose clauses each contain at least $k$ distinct literals.

Algorithm B1 keeps four variables: SUB (clauses already satisfied), LEFT (clauses not yet satisfied), TRUE (literals made true) and LIT (literals still available). It starts with SUB $=$ TRUE $= \emptyset$, LEFT $= S$, LIT $= L$. While some literal of LIT occurs in a clause of LEFT, it picks a literal $y \in$ LIT contained in the most clauses of LEFT, moves those clauses $YT$ from LEFT to SUB, adds $y$ to TRUE, and removes $y$ and $\bar y$ from LIT. When no literal of LIT occurs in LEFT it returns SUB.

The choice of $y$ is not determined when several literals tie. Following the paper's framework, every output reachable by some sequence of admissible choices is choosable, and the performance of B1 on $S$ is the smallest $|X|$ over choosable outputs $X$. The worst-case ratio on inputs of size at most $n$ is

$$R[B1, MS(k)](n) = \max\{S^*/B1(S) : S \in MS(k),\ |S| \le n\}.$$

Formalization targets

Goal: Theorem 2 (p. 262)

For all $k \ge 1$,

$$R[B1, MS(k)](n) \le \frac{k+1}{k}\quad\text{for all } n > 0,$$

with equality for all sufficiently large $n$. In the size-free form used here: every choosable output $X$ on every $S \in MS(k)$ satisfies $k\,S^* \le (k+1)\,|X|$, and for every $k \ge 1$ some $S \in MS(k)$ has a choosable $X$ with $|X| > 0$ and $k\,S^* = (k+1)\,|X|$.

Milestones (from the proof of Theorem 2, pp. 262–263)

1. In each iteration, the number of clauses saved (added to SUB) is at least the number of clauses remaining in LEFT that are wounded (lose a literal from LIT without being satisfied).
2. When B1 halts, every clause left in LEFT is dead: each of its literals has had its complement made true.
3. When B1 halts on an input of $MS(k)$, $|\mathrm{SUB}| \ge k\,|\mathrm{LEFT}|$, and SUB and LEFT partition $S$.
4. On the four-clause input $\{\{x_1,x_2,x_3\},\{\bar x_1,x_4,x_5\},\{\bar x_2,x_6,x_7\},\{\bar x_3,x_8,x_9\}\}$ of $MS(3)$, $S^* = 4$ while B1 may return three clauses.

Significance

The bound is stronger than a ratio: milestone 3 shows that B1 always satisfies at least $\tfrac{k}{k+1}|S|$ clauses, whatever the optimum. The tightness half shows that this simple greedy rule cannot be analysed any better, which is what motivated the weighted algorithm B2 of the same section, with ratio $2^k/(2^k-1)$. The pair of theorems is an early instance of a now standard pattern: a potential-style counting argument for an upper bound, and an adversarial tie-breaking instance for the matching lower bound.

The result is proved in the paper; it has not, to our knowledge, been machine-checked. This mission produces a formal model of Johnson's framework for a maximization problem with a nondeterministic algorithm, a formal proof of the upper bound through the "saved versus wounded" accounting, and explicit tightness instances for every $k \ge 1$. The paper spells out only $k = 3$ and states that "similar examples can be constructed for any other $k > 0$"; the formal goal requires them for all $k$.

Difficulty

The upper bound needs an invariant over entire runs, not over a single step: a clause wounded in one iteration may be saved in a later one, so wounds and saves must be tallied globally, and the count of wounds received by a clause that ends in LEFT must be matched with its number of literals. That matching relies on the facts that B1 never makes both a literal and its complement true and that a clause containing a true literal has already left LEFT. Clauses containing both $x_i$ and $\bar x_i$ are allowed and have to be handled.

The lower bound cannot be obtained from a fixed tie-breaking rule: the attaining run chooses negative literals whose count merely ties the maximum. For general $k$ the instance has to be built so that every literal occurs in few enough clauses that the adversarial choice is admissible at every step; at $k = 1$ the paper's pattern degenerates and needs adjusting.

Formalization scope

• A literal is a pair (variable index in $\mathbb N$, sign); a clause is a Finset of literals; an input is a Finset of clauses, so duplicate clauses are not allowed, as on the page. Tautological clauses are allowed.
• A truth assignment is a Set of literals without a complementary pair (partial, as in the paper). $S^*$ is the maximum of $|S'|$ over the finite nonempty family of satisfiable subsets, taken with Finset.sup'.
• B1 is a nondeterministic run relation: a state holds SUB, LEFT, TRUE and the set of decided variables (LIT is its complement, since $L$ is infinite); one step chooses any literal of LIT, of either sign, with maximum count; "choosable" is reachability of a halting state with the given SUB. No tie-break is fixed. A formalization that picks a variable and then its better sign, or that resolves ties deterministically, is a different algorithm and would make the tightness half false.
• The ratio $R[B1, MS(k)](n)$, whose problem size is left unspecified in the paper, is replaced by its size-free equivalent, and ratios are written multiplicatively in $\mathbb N$: $k\,S^* \le (k+1)|X|$. The tightness half requires $|X| > 0$, so the empty input cannot witness it.
• The running time $O(n \log n)$ is not stated.

Welcome contributions: proofs of the milestones, the invariants of reachable B1 states (SUB and LEFT partition $S$; TRUE is consistent and exactly covers the decided variables; no clause of LEFT meets TRUE), and the family of tightness instances for general $k$. The run-relation encoding of choosable outputs is reusable for the other algorithms of the paper.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• M. X. Goemans and D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM Journal on Discrete Mathematics 7 (1994), 656–666. https://doi.org/10.1137/S0895480192243516

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.

Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity $b$ so as to fill it as much as possible. For this problem the paper gives a family of algorithms $A_k$, one for each $k \ge 1$, whose guaranteed ratio $(k+1)/k$ tends to $1$. It is one of the first examples of what is now called a polynomial-time approximation scheme: for every $\epsilon > 0$ there is a polynomial-time algorithm within a factor $1 + \epsilon$ of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.

This mission formalizes Theorem 1 of the paper, the performance guarantee of $A_k$ together with its tightness.

Setting

An input $\langle T, s, b\rangle$ of SUBSET-SUM is a finite set $T$, a positive rational size $s(x)$ for every $x \in T$, and a positive rational bound $b$. An approximate solution is a subset $T' \subseteq T$ with $m(T') \le b$, where the measure is $m(T') = \sum_{x \in T'} s(x)$. The problem is a maximization problem with optimal measure

$$\langle T, s, b\rangle^* = \max\{\, m(T') : T' \subseteq T,\ m(T') \le b \,\}.$$

Fix $k \ge 1$ and call $x$ big if $s(x) > b/(k+1)$ and small otherwise. Algorithm $A_k$ keeps a set $\mathrm{SUB}$, its measure $\mathrm{SUM}$, and the remaining elements $\mathrm{LEFT}$:

1. $\mathrm{SUB}$ is a subset of the big elements whose measure is as large as possible without exceeding $b$; $\mathrm{SUM} = m(\mathrm{SUB})$ and $\mathrm{LEFT} = T \setminus \mathrm{SUB}$.
2. If $s(x) + \mathrm{SUM} > b$ for every $x \in \mathrm{LEFT}$, return $\mathrm{SUB}$.
3. Otherwise pick $y \in \mathrm{LEFT}$ with $s(y) + \mathrm{SUM}$ as large as possible without exceeding $b$, move it from $\mathrm{LEFT}$ to $\mathrm{SUB}$, add $s(y)$ to $\mathrm{SUM}$, and return to step 2.

Steps 1 and 3 may have ties. Following the paper, a set $T_1$ is choosable by $A_k$ if some resolution of all ties produces it, and the performance $A_k(u)$ on input $u$ is the smallest measure of a choosable output. The ratio is $r(A_k, u) = u^*/A_k(u) \ge 1$, and $R[A_k](n)$ is its maximum over inputs of size at most $n$.

Formalization targets

Goal: Theorem 1 (p. 260)

For $k \ge 1$ and $n > 0$,

$$R[A_k](n) \le \frac{k+1}{k}, \qquad \lim_{n \to \infty} R[A_k](n) = \frac{k+1}{k}.$$

Formally, for every $k \ge 1$: every choosable output $T_1$ of every input satisfies $k\,\langle T,s,b\rangle^* \le (k+1)\,m(T_1)$; and for every $\delta > 0$ some input has a choosable output $T_1$ with $m(T_1) > 0$ and $\langle T,s,b\rangle^* > \big(\tfrac{k+1}{k} - \delta\big)\,m(T_1)$.

Milestones

1. For $T_1$ choosable and $T_0$ any approximate solution, $m(T_1^{\mathrm{BIG}}) \ge m(T_0^{\mathrm{BIG}})$ (p. 260).
2. If a small $x \in T$ is not in a choosable $T_1$, then $s(x) + m(T_1) > b$, hence $m(T_1) > kb/(k+1) \ge \tfrac{k}{k+1}\langle T,s,b\rangle^*$ (p. 261).
3. The stronger dichotomy: $m(T_1) = \langle T,s,b\rangle^*$ or $m(T_1) \ge \tfrac{k}{k+1}\,b$ (p. 260).
4. The lower-bound input $T = \{a_1,\dots,a_{k+2}\}$, $s(a_1) = 1+\varepsilon$, $s(a_i) = 1$ otherwise, $b = k+1$: its optimum is $k+1$, some output is choosable, and every choosable output has measure $k + \varepsilon$ (p. 261).

Significance

Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above $1$, in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms $A_k$ are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of $A_k$ itself cannot be sharpened.

The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly $(k+1)/k$. The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.

Difficulty

The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing $A_k$ as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as $\mathrm{SUM}$ always equalling $m(\mathrm{SUB})$ or which elements can enter $\mathrm{SUB}$ after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general $k$: exactly $k-1$ unit elements are added after $a_1$, and this must be shown for every choosable run, not only for one.

Formalization scope

• Numbers. Sizes and the bound are rationals (ℚ), as in the paper; sizes are required to be positive on $T$ and $b > 0$. The index $k$ is a natural number with $1 \le k$ as a hypothesis; $b/(k+1)$ is rational division, and "big" is the strict inequality $s(x) > b/(k+1)$.
• Optimum. opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains $\emptyset$; it is $0$ when no element fits.
• Run relation. Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning $T_1$. Every "closest to, without exceeding" is an existential choice among all maximizers.
• Size-free restatement. The paper's input size $|u|$ ("in some standard notation") is never fixed, so the goal quantifies over all inputs instead of over sizes. The upper bound for all choosable outputs is equivalent to $R[A_k](n) \le (k+1)/k$ for all $n$; since $R[A_k]$ is nondecreasing, the limit claim is equivalent to the supremum of the ratio over all inputs being $(k+1)/k$, which is the second part.
• Multiplicative ratios. No ratio is written as a division, so an output of measure $0$ cannot satisfy a bound vacuously; the lower-bound part requires $m(T_1) > 0$. The value $(k+1)/k$ is not claimed to be attained: the paper's family has ratio $(k+1)/(k+\varepsilon)$.
• Lower-bound input. A def on Fin (k + 2) exactly as on the page, with $0 < \varepsilon < 1$ (the page leaves the range implicit; $\varepsilon < 1$ keeps $a_1$ the only big element that fits when $k = 1$).
• Ruled out. A formalization with a deterministic tie-break, with a bound of the form $\mathrm{opt}/m \le c$ in a field where $x/0 = 0$, or with tightness for a single fixed $k$ would be trivial or weaker; none of these is the target.

Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ($O(n^k)$ for step 1) and Sahni's knapsack extension are not part of the mission.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• S. Sahni, Approximate algorithms for the 0/1 knapsack problem, Journal of the ACM 22 (1975) 115–124. https://doi.org/10.1145/321864.321873
• O. H. Ibarra, C. E. Kim, Fast approximation algorithms for the knapsack and sum of subset problems, Journal of the ACM 22 (1975) 463–468. https://doi.org/10.1145/321906.321909
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9