Optimization

Motivation

Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. The standard decomposition methods for multistage stochastic linear programs, nested Benders decomposition and stochastic dual dynamic programming (SDDP), approximate each stage's expected cost-to-go function from below by finitely many affine cuts. This works because those functions are convex and polyhedral. With integer variables the cost-to-go functions are in general nonconvex, and no family of affine cuts can be exact at every evaluated state.

Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observe that the obstruction disappears when the state variables passed between stages are binary. Their Theorem 1 (p. 467) states that every real function of binary variables is represented exactly, at all binary points, by a convex polyhedral function on the unit cube. This is the structural fact on which their stochastic dual dynamic integer programming (SDDiP) algorithm rests: the cost-to-go function only ever needs to be evaluated at binary states, and there a convex piecewise linear under-approximation can be tight. Mixed integer states are reduced to binary ones by binary expansion (§5 of the paper).

Setting

Let $n \ge 0$ and write $\{0,1\}^n \subseteq \mathbb R^n$ for the binary points, the vectors each of whose coordinates is $0$ or $1$, and $C_n = [0,1]^n$ for the unit cube. Let $f$ be a real valued function defined on $\{0,1\}^n$.

For a set $X$ in a real vector space and $f : X \to \mathbb R$, a convex underestimator of $f$ is a function $h$ that is convex on the convex hull $\operatorname{conv}(X)$ and satisfies $h(x) \le f(x)$ for every $x \in X$ (Definition 3, p. 496). The largest convex underestimator of $f$ on $\operatorname{conv}(X)$, that is, a convex underestimator $e$ with $h \le e$ on $\operatorname{conv}(X)$ for every convex underestimator $h$, is the convex lower envelope of $f$. In this mission $X = \{0,1\}^n$.

A function $e$ is convex piecewise linear with finitely many linear pieces on $C_n$ if there are $\alpha_1, \dots, \alpha_K \in \mathbb R^n$ and $\beta_1, \dots, \beta_K \in \mathbb R$ with $e(x) = \max_k (\alpha_k^\top x + \beta_k)$ for all $x \in C_n$.

The proof works with the polyhedron of affine minorants of $f$,

$$\Pi = \{(\alpha,\beta) \in \mathbb R^n \times \mathbb R : \alpha^\top x + \beta \le f(x) \ \text{ for all } x \in \{0,1\}^n\},$$

the function $g(x) = \max_{(\alpha,\beta)\in\Pi}\{\alpha^\top x + \beta\}$, and the linear program $(P)$ defining $g(x)$ together with its dual

$$(D)\quad \min \sum_{i=1}^N f(\hat x^i)\lambda_i \ \ \text{s.t.}\ \ \hat X\lambda = x,\ e^\top\lambda = 1,\ \lambda \ge 0,$$

where $\hat X = [\hat x^1, \dots, \hat x^N]$ lists the $N = 2^n$ binary vectors.

Formalization targets

Goal: Theorem 1 (p. 467)

$f$ has a convex lower envelope, and every convex lower envelope $e$ of $f$ satisfies

$$e \text{ is convex on } [0,1]^n,\qquad e(x) = \max_{k=1,\dots,K}\big(\alpha_k^\top x + \beta_k\big)\ \ (x \in [0,1]^n),\qquad e(x) = f(x)\ \ (x \in \{0,1\}^n)$$

for some finite family of affine functions.

Milestones (proof of Theorem 1, p. 496)

1. $\operatorname{conv}(\{0,1\}^n) = [0,1]^n$.
2. For $x \in [0,1]^n$, $(P)$ and $(D)$ both attain their optima, with common value $g(x)$; in particular $g(x) < \infty$.
3. $g(x) = f(x)$ for every $x \in \{0,1\}^n$.
4. $g$ is convex on $[0,1]^n$ and is there the maximum of finitely many affine functions whose coefficients are extreme points of $\Pi$.
5. $h(x) \le g(x)$ for every $x \in [0,1]^n$ and every convex underestimator $h$ of $f$.

Significance

The result. Theorem 1 is what makes exact cutting-plane approximation possible for nonconvex value functions of binary states. In SDDiP, the expected cost-to-go function of each node is approximated from below by affine cuts; Theorem 1 guarantees that a convex polyhedral function exists that agrees with the true value function at every binary state, so a finite collection of valid cuts can be tight at every state the algorithm visits. Without it, the finite convergence of SDDiP to an optimal policy (Theorem 2 of the paper, with Lagrangian cuts from Theorem 3) would have no target to converge to. The statement fails for general finite sets in place of $\{0,1\}^n$: on $\{0,1,2\} \subseteq \mathbb R$ with $f(1) > (f(0)+f(2))/2$, no convex underestimator reaches $f(1)$.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization produces the identity $\operatorname{conv}(\{0,1\}^n) = [0,1]^n$, a finite-dimensional LP duality statement for the pair $(P)$–$(D)$, and a characterization of the convex lower envelope on the cube, each of independent use for later formalizations of binary and mixed integer programming (Lagrangian relaxations, convex closures, extended formulations).

Difficulty

Two steps carry the weight. The first is that the maximum defining $g$ is attained, with finitely many pieces coming from extreme points of the unbounded polyhedron $\Pi$: this needs LP duality and the existence of an optimal vertex for a pointed polyhedron, neither of which is a one-line consequence of Mathlib's convexity library. The second is the domination step. The printed argument handles interior points of the cube by writing a convex underestimator as a supremum of affine minorants, and binary points separately; the remaining boundary points of $[0,1]^n$ (for example $(1/2, 0)$ when $n = 2$) are covered by the paper's conclusion but not by those two cases, and require an argument that works on all of $\operatorname{conv}(\{0,1\}^n)$. Exactness at binary points uses that a binary point is not a nontrivial convex combination of other points of the cube.

Formalization scope

Points of $\mathbb R^n$ are Fin n → ℝ with the componentwise order; $C_n$ is Set.Icc 0 1, the binary points are the vectors with every coordinate $0$ or $1$, and $\alpha^\top x$ is the dot product. $f$ is a total function on $\mathbb R^n$ of which only the values at binary points enter any statement. Convexity of an underestimator is required on $\operatorname{conv}(\{0,1\}^n)$, exactly as in Definition 3, not on all of $\mathbb R^n$; the identification of this hull with $[0,1]^n$ is milestone 1, not a definition. The value $n = 0$ is allowed and no hypothesis on $n$ is added.

The readings of informal words are: "the convex lower envelope" is a predicate (largest convex underestimator on $\operatorname{conv}(X)$), so Theorem 1 asserts its existence and then its properties for every function satisfying it; "convex piecewise linear with a finite number of linear pieces" is "the maximum of finitely many affine functions on the cube"; "max" over $\Pi$ is an attained maximum, stated with IsGreatest; "min" in $(D)$ is stated with IsLeast. The proof's function $g$ is a real supremum, used only after its attainment is proved.

The convex lower envelope is not defined as $g$ (or as the value of $(D)$): under that definition convexity and piecewise linearity would be unfoldings, and Theorem 1's content, that the largest convex underestimator of Definition 3 has this form and is exact at binary points, would be lost.

A complete development needs: convex hulls of finite sets in $\mathbb R^n$, LP duality for a finite system of inequalities, extreme points of polyhedra and attainment of linear maxima at them, and Jensen's inequality for finite convex combinations. The cube identity and the LP duality milestone are reusable beyond this mission. Proofs of individual milestones, alternative proofs of Theorem 1 that bypass LP duality, and generalizations of the definitions are welcome.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Mathematical Programming, Ser. A 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. Their linear (continuous) counterparts are routinely solved by nested decomposition methods such as stochastic dual dynamic programming (SDDP; Pereira and Pinto, 1991), which approximate each node's expected cost-to-go function from below by a maximum of linear cuts. With integer variables the cost-to-go functions are no longer convex, and cuts from linear programming duality are in general not exact at the points where they are generated.

Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) restrict the state variables passed between stages to be binary and introduce a local copy $z_n$ of the parent's state at every node. Dualizing only the copy constraint $z_n = x_{a(n)}$ gives a class of cuts, the Lagrangian cuts, which the authors call "one of the major results of the paper" (p. 478). Their Theorem 3 shows that these cuts are valid (they never overestimate the true value function) and tight (they reproduce the current approximate value at the binary state where they are generated). Together with finiteness, these are the sufficient conditions of the paper's Definition 2 under which SND and SDDiP find an optimal solution in finitely many iterations with probability one (Theorem 2 of the paper, the subject of a companion mission).

Setting

Fix a node $n$ of the scenario tree and an iteration $i$ of the algorithm. The node has:

• a nodal constraint set $X_n \subseteq \mathbb R^d \times \mathbb R^d \times \mathbb R^\ell$ of triples $(z_n, x_n, y_n)$, where $x_n$ is the node's state, $y_n$ its local variables and $z_n$ the local copy of the parent's state. By assumption (A1) $X_n$ is nonempty, compact and mixed integer polyhedral: the points of a polyhedron $\{w : Aw \ge b\}$ with some coordinates integer;
• a linear objective $f_n(x_n, y_n) = c^\top x_n + e^\top y_n$;
• children $m \in \mathcal C(n)$ with conditional probabilities $q_{nm} \ge 0$, a lower bound $L_n$, and the children's cut coefficients $(v^\ell_m, \pi^\ell_m)$ for $\ell = 1, \dots, i$.

The approximate expected cost-to-go (3.2) is

$$\psi^{i+1}_n(x) = \min\Big\{\theta : \theta \ge L_n,\ \theta \ge \sum_{m} q_{nm}\big(v^\ell_m + (\pi^\ell_m)^\top x\big),\ \ell = 1,\dots,i\Big\},$$

and the updated forward problem (3.1) at a parent state $\hat x$ has value

$$\underline Q^i_n(\hat x, \psi^{i+1}_n) = \min\{ f_n(x,y) + \psi^{i+1}_n(x) : (z,x,y) \in X_n,\ z = \hat x,\ x \in \{0,1\}^d\}.$$

Let $X'_n = \{(z,x,y) \in X_n : x \in \{0,1\}^d,\ z \in [0,1]^d\}$ and let $X''_n$ add a variable $\theta \ge L_n$ that dominates every aggregated cut. The Lagrangian function and Lagrangian dual (4.3)–(4.4) are

$$\mathcal L^i_n(\pi) = \min_{(z,x,y,\theta)\in X''_n} f_n(x,y) + \theta - \pi^\top z, \qquad (R^i_n):\ \max_{\pi\in\mathbb R^d}\ \mathcal L^i_n(\pi) + \pi^\top \hat x .$$

An optimal $\hat\pi$ and $\hat v = \mathcal L^i_n(\hat\pi)$ define the Lagrangian cut $\theta \ge \hat v + \hat\pi^\top x_{a(n)}$. Given true value functions $Q_m$ of the children and $\mathcal Q_n = \sum_m q_{nm} Q_m$, the true nodal value (2.3) is $Q_n(x_a) = \min\{f_n(x,y) + \mathcal Q_n(x) : (z,x,y) \in X_n,\ z = x_a,\ x \in \{0,1\}^d\}$.

Formalization targets

Goal: Theorem 3 at one node

For binary $\hat x \in \{0,1\}^d$ and $\hat\pi$ optimal for $(R^i_n)$:

$$\hat v + \hat\pi^\top \hat x = \underline Q^i_n(\hat x, \psi^{i+1}_n) \qquad \text{(tightness, (3.5))},$$

and, if the children's cuts are valid for $Q_m$ on $\{0,1\}^d$ and $\mathcal Q_n \ge L_n$ there,

$$Q_n(x_a) \ge \hat v + \hat\pi^\top x_a \quad \text{for all } x_a \in \{0,1\}^d \qquad \text{(validity, (3.4))}.$$

The paper's statement for the whole collection of cuts of an iteration follows by applying this at every sampled node from the last stage backwards, exactly as its proof does by induction.

Milestones

1. (4.5): $\hat v + \hat\pi^\top\hat x = \min\{f_n + \theta : (z,x,y,\theta) \in \mathrm{conv}(X''_n),\ z = \hat x\}$, for any parent state at which $(R^i_n)$ has an optimal solution.
2. Binary face: for binary $\hat x$, $\mathrm{conv}(X''_n) \cap \{z = \hat x\} = \mathrm{conv}(X''_n \cap \{z = \hat x\})$.
3. Tightness (display after (4.5)).
4. Validity, base case: at a last-stage node, $Q_n(x_a) \ge \mathcal L^i_n(\pi) + \pi^\top x_a$.
5. Validity, induction step ((4.6) and the display after it).

Significance

Tightness at binary states is what separates Lagrangian cuts from the cuts of continuous relaxations or of a direct Lagrangian relaxation of the constraints coupling stages: the paper's Example 2 shows a direct relaxation whose cut is not tight even at a binary state, and Example 1 shows that with a non-binary state the duality gap is positive. With valid, tight and finite cuts, SND and SDDiP become exact algorithms for multistage stochastic integer programs with binary states, and through binarization they approximate problems with general mixed-integer states.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires a Lean statement of Geoffrion's theorem for this nodal problem (Lagrangian duality equals optimization over the convex hull of a mixed integer set), which is of independent use for integer programming, and the binary-face fact for sets inside the unit cube.

Difficulty

The validity half is weak duality and is short. The difficulty is in tightness. Step (4.5) is a strong duality statement for a nonconvex set: it needs that the convex hull of $X''_n$ is a polyhedron, which follows only because $X_n$ is compact and mixed integer polyhedral (so $X'_n$ is a finite union of polytopes), and then linear programming duality with attainment over that polyhedron. Neither the polyhedrality of convex hulls of finite unions of polytopes with a common recession direction nor finite-dimensional LP strong duality in the needed form is readily available in Mathlib. A tempting shortcut, Lagrangian duality from convex analysis with a Slater point, does not apply: a binary $\hat x$ lies on the boundary of the projection of $\mathrm{conv}(X''_n)$ onto $z$, so the constraint qualification fails and polyhedrality is genuinely needed.

Formalization scope

States, copies and multipliers are vectors in $\mathbb R^d$ (Fin d → ℝ); a state is binary when each coordinate is $0$ or $1$. Points of $X''_n$ are tuples (z, x, y, θ). Assumption (A1) is three fields of the node structure (nonempty, compact, mixed integer polyhedral after concatenating coordinates). Cuts are indexed by Fin i and children by Fin nC; probabilities are only required to be nonnegative. A last-stage node is nC = 0 with L = 0. The constraint $z \in [0,1]^d$ (2.1c) is kept in $X'_n$ and folded into $X_n$ in (2.3) and (3.1), as in the paper.

Readings of informal words:

• "min" in $\psi^{i+1}_n$, $\mathcal L^i_n$, $\underline Q^i_n$, $Q_n$: the definitions use sInf of the set of objective values, and every theorem states the minimum as an attained least element (IsLeast) or as a lower bound over all feasible points, so no junk value of sInf on an empty or unbounded set is used. The hypothesis $X''_n \ne \emptyset$ makes $\mathcal L^i_n$ a genuine minimum.
• "$\hat\pi$ optimal for (4.3)": maximizes $\pi \mapsto \mathcal L^i_n(\pi) + \pi^\top\hat x$ over all of $\mathbb R^d$.
• "the cuts are valid": $Q_n(x_a) \ge \hat v + \hat\pi^\top x_a$ is stated as a lower bound over every feasible point of (2.3), which is the paper's convention $Q_n = +\infty$ on infeasible states.
• The induction hypothesis of the validity proof is made explicit: all children's cuts $\ell = 1,\dots,i$ are valid, and $\mathcal Q_n \ge L_n$ on binary states.
• Tightness is stated with $\psi^{i+1}_n$; the proof's last line writes $\psi^i_n$, a misprint.

A trivializing formalization is ruled out: $\underline Q^i_n$ is the primal value of the forward problem (3.1) with $\psi^{i+1}_n$ from (3.2) and is never defined through the dual, and validity is required at every binary $x_a$, not only at $\hat x$.

A complete development needs: polyhedrality of convex hulls of bounded mixed integer sets, LP strong duality with attainment (or Geoffrion's theorem directly), Carathéodory-type reasoning in product spaces, and the fact that a binary point which is a positive convex combination of points of $[0,1]^d$ equals each of them. The first two are reusable well beyond this mission. Proofs of individual milestones are welcome independently; the validity milestones are accessible first.

Selected references

• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
• A. M. Geoffrion, Lagrangean relaxation for integer programming, Math. Program. Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895

Motivation

Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates $x^k\to x^*$ rather than of the limit point alone. Every local minimizer satisfies them, with or without a constraint qualification. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition $S$ is a property of the constraints at $x^*$ under which $S$ implies KKT for every objective function. The weaker this property, the larger the class of problems on which the condition certifies KKT points.

The Strong Approximate KKT (SAKKT) condition of Haeser and Schuverdt (J. Optim. Theory Appl. 149(3), 2011) asks for approximate Lagrange multipliers whose inequality part vanishes on every constraint that is strictly satisfied at the current iterate. It strictly implies the Approximate KKT condition (AKKT). Haeser and Schuverdt also showed that SAKKT is equivalent to the Approximate Gradient Projection condition AGP(0) of Martínez and Svaiter (2003). Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with each of AGP, CAKKT, LAGP and SAKKT. For AKKT the answer, the Cone Continuity Property, had been found earlier (Andreani et al. 2016). This mission formalizes the SAKKT case, Theorem 4.5 of the preprint.

Setting

Consider the nonlinear program

$$\min f(x)\quad\text{subject to}\quad h(x)=0,\ g(x)\le0, \tag{1.1}$$

with $h=(h_1,\dots,h_m)$ and $g=(g_1,\dots,g_p)$ continuously differentiable on $\mathbb R^n$. The feasible set is $\Omega=\{x:h(x)=0,\ g(x)\le0\}$, and $J(x^*)=\{j:g_j(x^*)=0\}$ is the set of active inequalities. The KKT condition holds at $x^*$ for $f$ if there are $\lambda\in\mathbb R^m$ and $\mu\in\mathbb R^p_+$, with $\mu_j=0$ for $j\notin J(x^*)$, such that $\nabla f(x^*)+\sum_i\lambda_i\nabla h_i(x^*)+\sum_j\mu_j\nabla g_j(x^*)=0$.

The linearized cone is $L_\Omega(x^*)=\{d:\langle\nabla h_i(x^*),d\rangle=0\ \forall i,\ \langle\nabla g_j(x^*),d\rangle\le0\ \forall j\in J(x^*)\}$, and $K^\circ=\{v:\langle v,k\rangle\le0\ \forall k\in K\}$ is the polar of a set $K$. For a convex set $S$, the normal cone $N_S(y)=\{w:\langle w,z-y\rangle\le0\ \forall z\in S\}$ is defined for $y\in S$ and is empty for $y\notin S$. $P_S$ is the Euclidean projection onto a nonempty closed convex set $S$.

For a point $x$, the linearized set $\Omega(x,0)$ consists of the $z$ with

• $\langle\nabla h_i(x),z-x\rangle=0$ for all $i$;
• $\langle\nabla g_j(x),z-x\rangle\le0$ for every $j$ with $g_j(x)\ge0$.

It keeps the inequalities that are active or violated at $x$ and drops those strictly satisfied at $x$.

A feasible $x^*$ satisfies SAKKT for $f$ if there are $x^k\to x^*$, $\lambda^k\in\mathbb R^m$ and $\mu^k\in\mathbb R^p_+$, with $\mu^k_j=0$ whenever $g_j(x^k)<0$, such that

$$\nabla f(x^k)+\sum_{i=1}^m\lambda_i^k\nabla h_i(x^k)+\sum_{j=1}^p\mu_j^k\nabla g_j(x^k)\to0. \tag{1.2}$$

It satisfies AGP(0) for $f$ if there is $x^k\to x^*$ with $P_{\Omega(x^k,0)}(x^k-\nabla f(x^k))-x^k\to0$. The outer limit $\limsup_{z\to z^*}F(z)$ of a set-valued map is the set of limits of sequences $w^k\in F(z^k)$ with $z^k\to z^*$ (1.6). The point $x^*$ is SAKKT-regular (Definition 4.3) if

$$\limsup_{x\to x^*}N_{\Omega(x,0)}(x)\subset N_{\Omega(x^*,0)}(x^*).$$

Formalization targets

Goal: Theorem 4.5

For continuously differentiable constraints and a feasible $x^*$,

$$x^*\ \text{SAKKT-regular}\iff\big(\forall f\in C^1:\ \text{SAKKT at }x^*\Rightarrow\text{KKT at }x^*\big).$$

The forward implication says SAKKT-regularity is a strict constraint qualification for SAKKT; the backward one says it is implied by every such qualification.

Milestones

1. Proposition 3.1: for nonempty closed convex $C$ and $x\in C$, $\omega\in N_C(x)\iff P_C(x+\omega)=x$.
2. Proposition 4.4: if $x+\varepsilon\in\Omega(x,0)$, every element of $N_{\Omega(x,0)}(x+\varepsilon)$ is $\sum_i\lambda_i\nabla h_i(x)+\sum_{g_j(x)\ge0}\mu_j\nabla g_j(x)$ with $\mu\ge0$ and $\mu_j\langle\nabla g_j(x),\varepsilon\rangle=0$; and $N_{\Omega(x,0)}(x+\varepsilon)\subset N_{\Omega(x,0)}(x)$.
3. AGP(0) $\iff$ SAKKT, for every $C^1$ objective (p. 6, from Haeser–Schuverdt).
4. $-\nabla f(x^*)\in L_\Omega(x^*)^\circ\iff$ KKT at $x^*$.
5. (4.22): $N_{\Omega(x^*,0)}(x^*)=L_\Omega(x^*)^\circ$ at a feasible $x^*$.
6. (4.23)–(4.24): an AGP(0) sequence for $f$ puts $-\nabla f(x^*)$ in $\limsup_{x\to x^*}N_{\Omega(x,0)}(x)$.
7. (4.26): every $\omega^*$ in that outer limit makes AGP(0) hold for $f(x)=-\langle\omega^*,x\rangle$.

Significance

Theorem 4.5 describes exactly the constraint systems on which a SAKKT sequence converging to $x^*$ certifies a KKT point, for every objective. Any constraint qualification already known to make SAKKT imply KKT implies SAKKT-regularity; at a point that is not SAKKT-regular, some linear objective has a SAKKT sequence converging to a non-KKT point. Because SAKKT is stronger than AKKT and AGP, its regularity condition is weaker than theirs, and Section 5 of the paper places it in the hierarchy of constraint qualifications next to AGP-regularity and CAKKT-regularity. By Proposition 4.4, SAKKT-regularity reads geometrically: the cone generated by the gradients of the equality constraints and of the inequalities that are active or violated at $x$ varies outer semicontinuously as $x\to x^*$.

The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the polyhedral convex-analysis facts behind it: the projection characterization of normal cones, the description of normal cones of $\Omega(x,0)$ at perturbed points, and the identification of $N_{\Omega(x^*,0)}(x^*)$ with $L_\Omega(x^*)^\circ$.

Difficulty

The forward direction passes to the limit in normal cones of sets $\Omega(x^k,0)$ that change with $k$: the set of rows kept depends on the sign of $g_j(x^k)$ at the moving point, not on the active set at $x^*$. Projections land at $y^k=x^k+\varepsilon^k$, while SAKKT-regularity speaks of normal cones at $x^k$, so the normal vectors must be transported from $y^k$ to $x^k$; this is Proposition 4.4, a Farkas-type statement for the cone of active rows. Moving between SAKKT and AGP(0) requires the Haeser–Schuverdt equivalence, which the paper cites rather than proves. The backward direction must build an objective function and a sequential certificate from an arbitrary element of an outer limit, which needs existence and nonexpansiveness of projections onto every $\Omega(x^k,0)$. Finally, $L_\Omega(x^*)^\circ$ and the KKT multipliers are linked by Farkas' lemma for a finitely generated cone.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.
• The standing hypothesis is that every $h_i$ and $g_j$ is $C^1$. "Smooth objective" in Theorem 4.5 is read as $C^1$, which is all the argument uses. The objective is quantified inside the equivalence, for fixed constraints and a fixed feasible $x^*$.
• KKT is the multiplier form with sign and complementarity. The paper's reading $-\nabla f(x^*)\in L_\Omega(x^*)^\circ$ is a milestone.
• SAKKT imposes $\mu^k_j=0$ when $g_j(x^k)<0$, at the iterate and not at $x^*$, and adds no complementarity limit. The page's "$x^k\to x$" is read as $x^k\to x^*$.
• The normal cone is empty outside the set, and the projection is a predicate (a nearest point), not a choice function. The outer limit is the sequential one of (1.6), with $x$ ranging over all of $\mathbb R^n$.
• Definition 4.3 is the inclusion; its trailing identity with $L_\Omega(x^*)^\circ$ is milestone 5. Proposition 4.4's "elements in $\mathbb R^m$" is read as $\mathbb R^n$.
• Junk gradients (no $C^1$ hypothesis where continuity is used), a normal cone that is nonempty at points outside the set, an objective quantified outside the equivalence, a support condition placed at $x^*$, or KKT without sign or complementarity would each trivialize or change the statement; the definitions above rule them out.

All objects are defined in the namespace StrictCQ.SAKKT. Proofs of milestones 1, 2, 4 and 5 are reusable convex analysis beyond this mission; contributions toward a proof of the Haeser–Schuverdt equivalence (milestone 3) are welcome independently of the goal.

Selected references

• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
• G. Haeser, M. L. Schuverdt, On approximate KKT condition and its extension to continuous variational inequalities, J. Optim. Theory Appl. 149(3):528–539, 2011. https://link.springer.com/journal/10957/volumes-and-issues/149-3
• J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, J. Optim. Theory Appl. 118:117–133, 2003. https://doi.org/10.1023/A:1023617925436
• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates $x^k\to x^*$ rather than of the limit alone. Every local minimizer satisfies them, with or without a constraint qualification, which makes them natural stopping criteria. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition $S$ is a property of the constraints at $x^*$ under which $S$ implies KKT for every objective function. The weaker this property, the more problems on which the stopping test is guaranteed to certify a KKT point.

The Approximate Gradient Projection (AGP) condition was introduced by Martínez and Svaiter (2003) and is the natural stopping criterion of inexact restoration methods. It is strictly stronger than the Approximate KKT condition (AKKT), and it does not require Lagrange multiplier estimates. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with AGP and with several other sequential conditions. For AKKT the answer had been found earlier: the Cone Continuity Property of Andreani, Martínez, Ramos and Silva (2016). This mission formalizes the AGP case, Theorem 4.2 of the preprint, together with its linear-constraint variant, Theorem 4.6.

Setting

Consider the nonlinear program

$$\min f(x)\quad\text{subject to}\quad h(x)=0,\ g(x)\le0, \tag{1.1}$$

with $h=(h_1,\dots,h_m)$ and $g=(g_1,\dots,g_p)$ continuously differentiable on $\mathbb R^n$. The feasible set is $\Omega=\{x:h(x)=0,\ g(x)\le0\}$, and $J(x^*)=\{j:g_j(x^*)=0\}$ is the set of active inequalities. The KKT condition holds at $x^*$ for $f$ if there are $\lambda\in\mathbb R^m$ and $\mu\in\mathbb R^p_+$, with $\mu_j=0$ for $j\notin J(x^*)$, such that $\nabla f(x^*)+\sum_i\lambda_i\nabla h_i(x^*)+\sum_j\mu_j\nabla g_j(x^*)=0$.

The linearized cone is $L_\Omega(x^*)=\{d:\langle\nabla h_i(x^*),d\rangle=0\ \forall i,\ \langle\nabla g_j(x^*),d\rangle\le0\ \forall j\in J(x^*)\}$, and $K^\circ=\{v:\langle v,k\rangle\le0\ \forall k\in K\}$ is the polar of a set $K$. For a convex set $S$, the normal cone $N_S(y)=\{w:\langle w,z-y\rangle\le0\ \forall z\in S\}$ is defined for $y\in S$ and is empty for $y\notin S$. $P_S$ denotes the Euclidean projection onto a closed convex set $S$.

For $\gamma\in[-\infty,0]$ and a point $x$, the linearized set $\Omega(x,\gamma)$ of (4.2) consists of the $z$ with

• $\langle\nabla h_i(x),z-x\rangle=0$ for all $i$;
• $\langle\nabla g_j(x),z-x\rangle\le0$ if $g_j(x)\ge0$;
• $g_j(x)+\langle\nabla g_j(x),z-x\rangle\le0$ if $\gamma<g_j(x)<0$.

A feasible $x^*$ satisfies AGP($\gamma$) for $f$ if there is a sequence $x^k\to x^*$ with

$$P_{\Omega(x^k,\gamma)}\big(x^k-\nabla f(x^k)\big)-x^k\to0. \tag{4.1}$$

The outer limit $\limsup_{z\to z^*}F(z)$ of a set-valued map is the set of limits of sequences $w^k\in F(z^k)$ with $z^k\to z^*$ (1.6). The point $x^*$ is AGP-regular (Definition 4.1) if

$$\limsup_{(x,\varepsilon)\to(x^*,0)}N_{\Omega(x,-\infty)}(x+\varepsilon)\subset N_{\Omega(x^*,-\infty)}(x^*).$$

Formalization targets

Goal: Theorem 4.2

For continuously differentiable constraints and a feasible $x^*$,

$$x^*\ \text{AGP-regular}\iff\big(\forall f\in C^1:\ \mathrm{AGP}(-\infty)\text{ at }x^*\Rightarrow\text{KKT at }x^*\big).$$

The forward implication says AGP-regularity is a strict constraint qualification for AGP; the backward one says it is implied by every such qualification.

Milestones

1. Proposition 3.1: for nonempty closed convex $C$ and $x\in C$, $\omega\in N_C(x)\iff P_C(x+\omega)=x$.
2. Nonexpansiveness of $P_C$, used in (4.10).
3. (4.6): $N_{\Omega(x^*,-\infty)}(x^*)=L_\Omega(x^*)^\circ$ at a feasible $x^*$.
4. $-\nabla f(x^*)\in L_\Omega(x^*)^\circ\iff$ KKT at $x^*$.
5. (4.8): $N_{\Omega(x^k,\gamma)}(x^k+\varepsilon^k)\subset N_{\Omega(x^k,-\infty)}(x^k+\varepsilon^k)$ for $k$ large.
6. (4.7)–(4.9): under AGP-regularity, AGP($\gamma$) implies KKT for every $\gamma\in[-\infty,0)$.
7. (4.10)–(4.11): every $\omega^*$ in the outer limit makes AGP($-\infty$) hold for $f(x)=-\langle\omega^*,x\rangle$.

Companion: Theorem 4.6

The same characterization for the Linear AGP condition (LAGP), in which the linear constraints are kept exact and the iterates stay in the set $\Omega_L$ they define. LAGP-regularity (Definition 4.4) is outer semicontinuity of $(x,\varepsilon)\mapsto N_{\Omega_{NL}(x,-\infty)\cap\Omega_L}(x+\varepsilon)$ relative to $x\in\Omega_L$. Two further items accompany it: Proposition 4.1, the explicit form of $N_{\Omega(x,-\infty)}(x+\varepsilon)$, and the equality $N_{\Omega_{NL}(x^*,-\infty)\cap\Omega_L}(x^*)=L_\Omega(x^*)^\circ$ appended to Definition 4.4.

Significance

Theorem 4.2 gives the exact boundary of the problems on which an AGP-based stopping test certifies KKT points. Any constraint qualification already known to make AGP imply KKT, for instance the Cone Continuity Property, implies AGP-regularity. Conversely, at a point that is not AGP-regular some objective function has an AGP sequence converging to a non-KKT point. In Section 5 of the paper the theorem places AGP-regularity in the hierarchy of constraint qualifications, with the regularity notions for CAKKT and SAKKT next to it.

The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the convex-analysis facts it rests on: the projection characterization of normal cones, nonexpansiveness, and the polyhedral normal cone of $\Omega(x^*,-\infty)$ as the polar of the linearized cone. These facts are reusable for any sequential optimality condition built on projections.

Difficulty

The forward direction passes to the limit in normal cones of sets $\Omega(x^k,\gamma)$ that vary with $k$ and are evaluated at perturbed points $x^k+\varepsilon^k$, which may lie outside $\Omega(x^k,-\infty)$. For finite $\gamma$ the inclusion of $N_{\Omega(x^k,\gamma)}$ in $N_{\Omega(x^k,-\infty)}$ fails at such points. It holds only for $k$ large, through a continuity argument on the inactive constraints. The backward direction must manufacture an objective function and an AGP sequence from an arbitrary element of an outer limit, which requires existence of projections onto every $\Omega(x^k,-\infty)$. The identification of $N_{\Omega(x^*,-\infty)}(x^*)$ with $L_\Omega(x^*)^\circ$ needs the localization of a polyhedral normal cone, and the link between $L_\Omega(x^*)^\circ$ and KKT multipliers is Farkas' lemma for a finitely generated cone.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.
• The standing hypothesis is that every $h_i$ and $g_j$ is $C^1$. Objectives in the characterizations are $C^1$ and are quantified inside the equivalence, for fixed constraints and fixed feasible $x^*$.
• KKT is the multiplier form with sign and complementarity. The paper's reading $-\nabla f(x^*)\in L_\Omega(x^*)^\circ$ is a milestone.
• $\gamma$ is an extended real and $-\infty$ is its bottom element. The goal states AGP as AGP($-\infty$). The paper's AGP is the $\gamma$-independent condition of Martínez–Svaiter, which this paper does not prove; milestone 6 gives the forward direction for every $\gamma<0$.
• The normal cone is empty outside the set. A normal cone that is nonempty at infeasible points makes AGP-regularity a different, stronger condition. The projection is a predicate (a nearest point), not a choice function.
• The outer limit is sequential, as in (1.6).
• The paper says the inclusion (4.8) "always holds"; it is stated for $k$ large, which is what the proof uses. Definition 4.4's "$\Omega_L\times\mathbb R^m$" is read as $\Omega_L\times\mathbb R^n$.
• A formalization with junk gradients (no $C^1$ hypothesis where the proof needs continuity), an objective quantified outside the equivalence, or KKT without sign or complementarity is ruled out by the statements above.

All objects are defined in the namespace StrictCQ.AGP. Proofs of the convex-analysis milestones are reusable beyond this mission.

Selected references

• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
• J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, J. Optim. Theory Appl. 118:117–133, 2003. https://doi.org/10.1023/A:1023617925436
• R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

The shortest-path problem in a graph of convex sets (SPP in GCS), introduced by Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024), asks for a path through a directed graph whose vertices carry convex sets, together with a point in each visited set, minimizing a sum of convex edge lengths. It models motion planning around obstacles, hybrid-system control and other problems that mix a discrete choice with continuous positions. The paper formulates it as a mixed-integer convex program whose only nonconvexity, before relaxation, is a family of bilinear equalities $Z = xy^\top$ that couple the continuous positions $x$ with the flow variables $y$.

Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by $Z = xy^\top$ are the idea behind the McCormick envelope (McCormick 1976) and the Reformulation-Linearization Technique of Sherali and Adams. This mission formalizes the paper's result that the relaxation is exact at every extreme point of the polytope $\mathcal Y$, which is the property that makes the mixed-integer formulation exact at binary flows.

Setting

Fix $\mathcal X \subseteq \mathbb R^n$ and $\mathcal Y \subseteq \mathbb R^m$. Points of $\mathbb R^n\times\mathbb R^m\times\mathbb R^{n\times m}$ are written $(x, y, Z)$.

• The perspective of $\mathcal X$ (Definition 4.1) is $\tilde{\mathcal X} := \operatorname{cl}\{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\} \subseteq \mathbb R^n \times \mathbb R$.
• The cone of valid inequalities (Definition 4.8) is $\mathcal X^\circ := \{(a, b) : a^\top x + b \ge 0 \text{ for all } x \in \mathcal X\}$.
• The dual cone of $\mathcal K \subseteq \mathbb R^n\times\mathbb R$ is $\mathcal K^* := \{(a, b) : a^\top x + b\lambda \ge 0 \text{ for all } (x, \lambda) \in \mathcal K\}$.
• The bilinear set (7.1) is $\mathcal S := \{(x, y, Z) : x \in \mathcal X,\ y \in \mathcal Y,\ Z = xy^\top\}$.
• The set-based relaxation (7.2) multiplies every valid inequality of $\mathcal X$ by every valid inequality of $\mathcal Y$ and replaces $xy^\top$ by $Z$:

$$\mathcal S' := \{(x, y, Z) : a^\top Zc + d\,a^\top x + b\,c^\top y + bd \ge 0 \text{ for all } (a, b) \in \mathcal X^\circ,\ (c, d) \in \mathcal Y^\circ\}.$$

• A polytope is a bounded set $\mathcal Y = \{y : c_i^\top y + d_i \ge 0 \text{ for all } i \in \mathcal I\}$ with $\mathcal I$ finite. Its asymmetric relaxation (7.3) is $\{(x, y, Z) : (Zc_i + d_i x,\ c_i^\top y + d_i) \in \tilde{\mathcal X} \text{ for all } i \in \mathcal I\}$.

Always $\mathcal S \subseteq \mathcal S'$, and $\mathcal S'$ is convex.

Formalization targets

Goal: Lemma 7.4 (p. 13)

Let $\mathcal X$ be compact and convex, let $\mathcal Y$ be a polytope and let $\hat y$ be an extreme point of $\mathcal Y$. Then for all $x$ and $Z$,

$$(x, \hat y, Z) \in \mathcal S \iff (x, \hat y, Z) \in \mathcal S'.$$

Milestones

1. (7.2), p. 12: $\mathcal S \subseteq \mathcal S'$ for arbitrary sets.
2. The sentence after (7.2), p. 12: for closed convex $\mathcal X, \mathcal Y$, every point of $\mathcal S'$ has $x \in \mathcal X$ and $y \in \mathcal Y$.
3. Lemma 4.9, p. 6: for nonempty closed convex $\mathcal X$, $(\tilde{\mathcal X})^* = \mathcal X^\circ$ and $(\mathcal X^\circ)^* = \tilde{\mathcal X}$.
4. Proposition 7.1, inclusion $\subseteq$, p. 12: $\mathcal S'$ is contained in the asymmetric relaxation (7.3), for every family of halfspaces.
5. Remark 4.2, p. 5: for compact convex $\mathcal X$, $\tilde{\mathcal X} = \{(x, \lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\}$, without closure.
6. Proof of Lemma 7.4, p. 13: at an extreme point of a polyhedron with finitely many inequalities, $m$ linearly independent inequalities are active.
7. Proposition 7.1, p. 12: $\mathcal S'$ equals (7.3), when the trivial inequality $1 \ge 0$ is a nonnegative combination of the defining inequalities.
8. Remark 7.5, p. 14: if $\mathcal Y \subseteq [0,1]^m$, every point of $\mathcal Y \cap \{0,1\}^m$ is an extreme point of $\mathcal Y$.
9. (7.4), p. 13: for compact convex $\mathcal X$ and $\mathcal Y = \operatorname{conv}\{\hat y_j\}_{j\in\mathcal J}$, $\operatorname{conv}\mathcal S = \{\sum_j (x_j, \lambda_j\hat y_j, x_j\hat y_j^\top) : \sum_j \lambda_j = 1,\ (x_j, \lambda_j) \in \tilde{\mathcal X}\}$.

Significance

The result. In the paper's mixed-integer program each vertex $v$ contributes a bilinear set $\mathcal S_v$ in which $\mathcal X$ is the convex set at $v$ and $\mathcal Y$ is the polytope of flows on the edges at $v$. Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing $\mathcal S_v$ by $\mathcal S'_v$ loses nothing at the integer points of the program. This gives the paper's second, geometric proof that its mixed-integer convex formulation is exact (Theorem 5.7). By Remark 7.5 the lemma also extends a known property of the first-level Reformulation-Linearization Technique for bilinear programs with binary variables from polytopes $\mathcal X$ to compact convex sets $\mathcal X$. Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of $\mathcal S'$ by one perspective-cone constraint per facet of $\mathcal Y$.

Formalizing it. The results are proved on paper; none of them has a machine-checked proof. The formalization also settles the exact hypotheses. Three statements of this section are false as printed (see Formalization scope), and the corrected versions are posed here with the counterexamples recorded. The perspective cone, the cone of valid inequalities and their duality (Lemma 4.9) are general convex-analysis facts that recur across conic and disjunctive programming.

Difficulty

The direction $\mathcal S \subseteq \mathcal S'$ is one line, since $(a^\top x + b)(c^\top y + d) \ge 0$. The converse at $\hat y$ needs three ingredients that are each standard and none of which is in Mathlib in this form.

• The duality between $\tilde{\mathcal X}$ and $\mathcal X^\circ$ is a bipolar theorem for the closed cone generated by $\mathcal X \times \{1\}$, in the product $\mathbb R^n \times \mathbb R$ with the pairing $a^\top x + b\lambda$. The cone needs care at $\lambda = 0$.
• The active-constraint characterization of extreme points of a polyhedron in halfspace form has to be proved directly.
• The step "$(u, 0) \in \tilde{\mathcal X}$ implies $u = 0$" is where boundedness enters. For unbounded $\mathcal X$ the slice $\lambda = 0$ of $\tilde{\mathcal X}$ is the recession cone, and the argument, and the lemma, fail.

Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality $(0, 1)$.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, inner products are dotProduct, $Zc$ is Z *ᵥ c and $xy^\top$ is Matrix.vecMulVec x y. Triples are (x, y, Z) in (Fin n → ℝ) × (Fin m → ℝ) × Matrix (Fin n) (Fin m) ℝ. A polytope is given by a finite family (c i, d i) over a Fintype index and the hypothesis Bornology.IsBounded; extreme points are Mathlib's Set.extremePoints ℝ, never a predicate defined through active constraints. The dual cone uses the pairing $a^\top x + b\lambda$ on the product, not an inner product.

Hypotheses added relative to the page, each with a counterexample to the printed form:

• Lemma 7.4 and (7.4): $\mathcal X$ compact. Section 7.1 only asks $\mathcal X$ to be closed and convex. For $\mathcal X = [0, \infty)$, $\mathcal Y = [0, 1]$ and $\hat y = 0$, the point $(1, 0, \tfrac12)$ is in $\mathcal S'$ but not in $\mathcal S$. Compactness is the standing assumption of Section 2 on the sets $\mathcal X_v$ that $\mathcal X$ stands for.
• Lemma 4.9: $\mathcal X$ nonempty. For $\mathcal X = \emptyset$, $\tilde{\mathcal X} = \emptyset$ but $(\mathcal X^\circ)^* = \{0\}$.
• Proposition 7.1 (equality): $1 \ge 0$ is a nonnegative combination of the rows. For $\mathcal Y = \{0\}$ written as $\{y \ge 0, -y \ge 0\}$ and $\mathcal X = [0, 1]$, the point $(5, 0, 0)$ satisfies (7.3) but not (7.2). The hypothesis holds for every polytope with an interior point and for the flow polytopes of the paper.

Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of $\mathcal X$ throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.

Trivializing formalizations ruled out: $\mathcal S'$ quantifies over all of $\mathcal X^\circ \times \mathcal Y^\circ$ and is not replaced by (7.3) in the goal; $\mathcal X$ is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable ($\mathcal X = \mathcal Y = [0,1]$, $\hat y = 0$ is checked in Lean).

A complete development needs the bipolar theorem for closed convex cones in $\mathbb R^{n}\times\mathbb R$, the closedness of the cone over a compact convex set, the active-constraint characterization of extreme points, and a finite affine Farkas lemma. All of these are reusable well beyond this mission and are welcome as separate contributions.

Selected references

• T. Marcucci, J. Umenberger, P. A. Parrilo, R. Tedrake, Shortest Paths in Graphs of Convex Sets, SIAM J. Optim. 34(1), 2024. arXiv:2101.11565v5 (the version cited). https://arxiv.org/abs/2101.11565 , https://doi.org/10.1137/22M1523790
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Corollary 11.7.2, Theorem 14.1). https://doi.org/10.1515/9781400873173
• G. P. McCormick, Computability of global solutions to factorable nonconvex programs: Part I — Convex underestimating problems, Math. Program. 10, 1976. https://doi.org/10.1007/BF01580665
• H. D. Sherali, W. P. Adams, A Reformulation-Linearization Technique for Solving Discrete and Continuous Nonconvex Problems, Kluwer, 1999. https://doi.org/10.1007/978-1-4757-4388-3