Operations Research

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

The stable set problem (find a largest, or maximum-weight, set of pairwise non-adjacent nodes in a graph) is NP-hard, and its linear programming relaxations have been studied since the 1970s as a test bed for polyhedral combinatorics. Lovász and Schrijver (SIAM J. Optim. 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation to a cone of $(n+1)\times(n+1)$ matrices, impose conditions every 0–1 solution satisfies, and project back. Its semidefinite version, the operator $N_+$, is one of the first systematic uses of positive semidefinite constraints in combinatorial optimization, and it is the ancestor of the Sherali–Adams, Lasserre and sum-of-squares hierarchies used today in approximation algorithms and proof complexity.

For the stable set problem the paper measures the strength of the operators by an index: how many rounds are needed before a given valid inequality is implied. This mission formalizes the paper's result that one round of $N_+$ already implies four of the classical families of facets of the stable set polytope.

Timeline:

• 1975: Chvátal shows that the rank constraint of a connected α-critical graph defines a facet of its stable set polytope (Chvátal 1975); clique, odd hole and odd antihole constraints are special rank constraints.
• 1981–88: Grötschel, Lovász and Schrijver show that the weighted stable set problem is solvable in polynomial time for perfect and $h$-perfect graphs, through the theta body $\mathrm{TH}(G)$ (Grötschel, Lovász, Schrijver 1988).
• 1991: Lovász and Schrijver define the operators $N$ and $N_+$ and prove Corollary 2.15: clique, odd hole, odd wheel and odd antihole constraints have $N_+$-index 1.

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$. The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$. Let $Q$ be the cone spanned by the 0–1 vectors with $x_0 = 1$. For a convex cone $K \subseteq Q$, the matrix cone $M_+(K)$ consists of the symmetric positive semidefinite matrices $Y = (y_{ij})$ with $y_{ii} = y_{0i}$ for $1 \le i \le n$ and $u^{\mathsf T}Yv \ge 0$ for all $u \in K^*$, $v \in Q^*$. The operator is

$$N_+(K) = \{Ye_0 : Y \in M_+(K)\},$$

and $N_+^0(K) = K$, $N_+^t(K) = N_+(N_+^{t-1}(K))$.

Let $G = (V, E)$ be a finite graph with no isolated nodes (the paper's standing assumption for Section 2). $\mathrm{STAB}(G)$ is the convex hull of incidence vectors $\chi^A$ of stable sets $A$. $\mathrm{FRAC}(G)$ is the polytope given by $x_i \ge 0$ and $x_i + x_j \le 1$ for $ij \in E$. $\mathrm{FR}(G) \subseteq \mathbb R^{V\cup\{0\}}$ is the cone $x_i \ge 0$, $x_i + x_j \le x_0$. The relaxations are

$$N_+^r(G) = \{x \in \mathbb R^V : (1, x) \in N_+^r(\mathrm{FR}(G))\},$$

so $N_+^0(G) = \mathrm{FRAC}(G) \supseteq N_+^1(G) \supseteq \dots \supseteq \mathrm{STAB}(G)$. The $N_+$-index of an inequality $a^{\mathsf T}x \le b$ valid for $\mathrm{STAB}(G)$ is the least $r$ with $a^{\mathsf T}x \le b$ valid for $N_+^r(G)$.

The four constraint families are:

• clique: $\sum_{i\in B} x_i \le 1$ for a clique $B$;
• odd hole: $\sum_{i\in C} x_i \le \frac12(|C|-1)$ for $C$ inducing a chordless odd cycle;
• odd wheel: $\sum_{i\in U\setminus\{u_0\}} x_i + \frac{|U|-2}{2}x_{u_0} \le \frac{|U|-2}{2}$ for $U$ inducing an odd wheel with center $u_0$ (an odd hole plus a node adjacent to all of it);
• odd antihole: $\sum_{i\in D} x_i \le 2$ for $D$ inducing a chordless odd cycle in the complement of $G$.

The contraction of a node $v$ turns $a^{\mathsf T}x \le b$ into the inequality with the coefficients of $v$ and its neighbours removed and right-hand side $b - a_v$.

Formalization targets

Goal: Corollary 2.15

For every graph $G$ without isolated nodes, each clique constraint (clique of size at least 3), odd hole constraint, odd wheel constraint and odd antihole constraint has $N_+$-index exactly 1:

$$a^{\mathsf T}x \le b \text{ holds on } N_+^1(G) \quad\text{and fails somewhere on } \mathrm{FRAC}(G).$$

Milestones

1. Lemma 1.5: for a closed convex cone $K \subseteq Q$ and $a$ with $a_i \le 0$ ($i \ge 1$), $a_0 \ge 0$, if $a^{\mathsf T}x \ge 0$ holds on $K \cap G_i$ (where $G_i = \{x_i = x_0\}$) for every $i$ with $a_i < 0$, then it holds on $N_+(K)$.
2. Lemma 2.14: if $a^{\mathsf T}x \le b$ is valid for $\mathrm{STAB}(G)$, and the contraction of every node with positive coefficient is valid for $N_+^r(G)$, then $a^{\mathsf T}x \le b$ is valid for $N_+^{r+1}(G)$.
3. Bipartite support (Section 2.c): an inequality valid for $\mathrm{STAB}(G)$ whose nonzero-coefficient nodes induce a bipartite graph is valid for $\mathrm{FRAC}(G)$.
4. Contraction property (Section 2.d): contracting a node with positive coefficient in any of the four constraints leaves positive-coefficient nodes that induce a bipartite subgraph.

Further result

Corollary 2.19 (first sentence): the $N_+$-index of a $\mathrm{STAB}(G)$-valid inequality $a^{\mathsf T}x \le b$ is at most the independence number of the subgraph induced by the nodes with positive coefficient.

Significance

Corollary 2.15 shows that a single round of $N_+$, a relaxation over which one can optimize in polynomial time for each fixed number of rounds (the paper's Theorem 2.1), captures all clique, odd hole, odd wheel and odd antihole inequalities at once. Consequently $N_+(G) = \mathrm{STAB}(G)$ for every $h$-perfect graph, in particular for perfect and $t$-perfect graphs. The result is a standard reference point when comparing lift-and-project hierarchies, and the lemmas behind it (Lemma 1.5 and Lemma 2.14) are the paper's general tools for bounding $N_+$-ranks.

The theorem was proved in 1991. To our knowledge it has not been machine-checked: this mission would produce the first formal development of the Lovász–Schrijver $N_+$ operator, its iterates, and the stable set relaxations $\mathrm{STAB}$, $\mathrm{FRAC}$, $\mathrm{FR}$ in Lean.

Difficulty

The lower bound (each constraint fails on $\mathrm{FRAC}(G)$) is a direct computation; the upper bound is where the work lies. The obvious approach, deriving each constraint from the linear conditions on the lifted matrix $Y$ alone, cannot succeed: those conditions define the linear operator $N$, and the goal is specifically about what positive semidefiniteness adds. The general lemmas are stated for arbitrary cones and require a working theory of polar cones and closedness in $\mathbb R^{n+1}$, including closedness of the iterates $N_+^r(\mathrm{FR}(G))$, which the paper uses without comment. The graph-theoretic steps require facts about the stable set and fractional stable set polytopes of bipartite graphs and a careful case analysis of chordless odd cycles in a graph and in its complement, none of which is in Mathlib.

Formalization scope

• Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι, with none the special coordinate $x_0$. For graphs, ι := V.
• $M$ is defined by condition (iii) with polar cones, not by its reformulations. Only $M_+$, $N_+$ and their iterates are defined; the linear operator $N$ is not used.
• Lemma 1.5 carries the hypothesis that $K$ is closed. The paper takes it tacitly (all its cones are polyhedral); without it the lemma fails, since $N_+(K)$ depends only on the closure of $K$.
• $\mathrm{FR}(G)$ is defined by its constraints, which agree with the paper's "cone spanned by the vectors $(1,x)$, $x \in \mathrm{FRAC}(G)$" because $G$ has no isolated nodes. Every graph statement carries the no-isolated-nodes hypothesis.
• Contraction is written on the same graph $G$ as a zeroed coefficient vector, rather than on the subgraph $G - \Gamma(v) - v$.
• Odd holes include triangles; odd antiholes have at least 5 nodes (a 3-node "antihole" is a stable set, for which the constraint is false); odd wheels are an odd hole plus a center adjacent to all its nodes.
• Clique constraints in the goal are restricted to cliques with at least 3 nodes: cliques of size 1 or 2 give inequalities already valid on $\mathrm{FRAC}(G)$, of index 0.
• "$N_+$-index at most $r$" is stated as validity on $N_+^r(G)$; the index itself is stated with IsLeast, never with an infimum that would default to 0 on an empty set.

A formalization asserting only validity on $N_+^1(G)$, or only for one fixed graph, would be weaker than the paper's statement and is ruled out: the goal states the exact index for all graphs without isolated nodes and all four families.

Not formalized: the linear operator $N$ and its results, the polynomial-time separation results (Theorem 2.1, Corollaries 2.20–2.21), the theta-body results (Lemma 2.17, Corollary 2.18), graph indices (Corollary 2.16), and the second sentence of Corollary 2.19.

Reusable infrastructure includes the polar cone, the matrix cone $M_+$ and the $N_+$ operator (usable for any 0–1 program), the polytopes $\mathrm{STAB}$ and $\mathrm{FRAC}$, and odd holes, antiholes and wheels as finite-set predicates. Contributions proving closedness of the iterates, the integrality of $\mathrm{FRAC}$ for bipartite graphs, or the $M$-cone reformulations (iii′)–(iii″) are welcome.

Selected references

• L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2), 1991, 166–190. https://doi.org/10.1137/0801013
• M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988 (2nd ed. 1993). https://doi.org/10.1007/978-3-642-78240-4
• V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory B 18, 1975, 138–154. https://doi.org/10.1016/0095-8956(75)90041-6

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

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