[docs] add background on infeasibility certificates

docs/make.jl

@@ -37,6 +37,7 @@ const _PAGES = [
     ],
     "Background" => [
         "background/duality.md",
+        "background/infeasibility_certificates.md",
         "background/naming_conventions.md",
     ],
     "API Reference" => [

docs/src/background/infeasibility_certificates.md

@@ -0,0 +1,123 @@
+```@meta
+CurrentModule = MathOptInterface
+DocTestSetup = quote
+    using MathOptInterface
+    const MOI = MathOptInterface
+end
+DocTestFilters = [r"MathOptInterface|MOI"]
+```
+
+# Infeasibility certificates
+
+When given an infeasible or unbounded model, some (conic) solvers can produce a
+certificate or infeasibility. This page explains what a certificate of
+infeasibility is for unbounded and infeasible models.
+
+## Conic duality
+
+MathOptInterface uses conic duality, which we use to define infeasibility
+certificates. A full explanation is given in the section [Duality](@ref), but
+here is a brief overview.
+
+For a minimization problem in geometric conic form, the primal is:
+```math
+\begin{align}
+& \min_{x \in \mathbb{R}^n} & a_0^\top x + b_0
+\\
+& \;\;\text{s.t.} & A_i x + b_i & \in \mathcal{C}_i & i = 1 \ldots m,
+\end{align}
+```
+and the dual is a maximization problem in standard conic form:
+```math
+\begin{align}
+& \max_{y_1, \ldots, y_m} & -\sum_{i=1}^m b_i^\top y_i + b_0
+\\
+& \;\;\text{s.t.} & a_0 - \sum_{i=1}^m A_i^\top y_i & = 0
+\\
+& & y_i & \in \mathcal{C}_i^* & i = 1 \ldots m,
+\end{align}
+```
+where each ``\mathcal{C}_i`` is a closed convex cone and ``\mathcal{C}_i^*`` is
+its dual cone.
+
+For a maximization problem in geometric conic form, the primal is:
+```math
+\begin{align}
+& \max_{x \in \mathbb{R}^n} & a_0^\top x + b_0
+\\
+& \;\;\text{s.t.} & A_i x + b_i & \in \mathcal{C}_i & i = 1 \ldots m,
+\end{align}
+```
+and the dual is a minimization problem in standard conic form:
+```math
+\begin{align}
+& \min_{y_1, \ldots, y_m} & \sum_{i=1}^m b_i^\top y_i + b_0
+\\
+& \;\;\text{s.t.} & a_0 + \sum_{i=1}^m A_i^\top y_i & = 0
+\\
+& & y_i & \in \mathcal{C}_i^* & i = 1 \ldots m.
+\end{align}
+```
+
+## Unbounded models
+
+If a model is unbounded, then two things are true:
+ 1. there exists a feasible primal solution
+ 2. the dual is infeasible.
+
+A feasible primal solution---if one exists---can be obtained by setting
+[`ObjectiveSense`](@ref) to `FEASIBILITY_SENSE` and then optimizing. Therefore,
+most solvers terminate after they prove the dual is infeasible via a certificate
+of dual infeasibility. This is also the reason that MathOptInterface defines the
+`DUAL_INFEASIBLE` status instead of `UNBOUNDED`.
+
+A certificate of dual infeasibility is an improving ray of the primal problem.
+That is, there exists some vector ``d`` such that for all ``\eta > 0``:
+```math
+A_i (x + \eta d) + b_i \in \mathcal{C}_i,\ \ i = 1 \ldots m,
+```
+and (for minimization problems):
+```math
+a_0^\top (x + \eta d) + b_0 < a_0^\top x + b_0,
+```
+for any feasible point ``x``. The latter simplifies to ``a_0^\top d < 0``. For
+maximization problems, the inequality is reversed, so that ``a_0^\top d > 0``.
+
+If the solver has found a certificate of infeasibility:
+
+ * [`TerminationStatus`](@ref) must be `DUAL_INFEASIBLE`
+ * [`PrimalStatus`](@ref) must be `INFEASIBILITY_CERTIFICATE`
+ * [`VariablePrimal`](@ref) must be the corresponding value of ``d``
+ * [`ObjectiveValue`](@ref) must be the value ``a_0^\top d``. Note that this is
+   the value of the objective function at `d`, ignoring the constant `b_0`.
+
+## Infeasible models
+
+A certificate of primal infeasibility is an improving ray of the dual problem.
+However, because infeasibility is independent of the objective function, we
+first homogenize the primal problem by removing its objective.
+
+Therefore, a dual improving ray is some vector ``d`` such that for all
+``\eta > 0``:
+```math
+\begin{align}
+\sum_{i=1}^m A_i^\top (y_i + \eta d_i) & = 0 \\
+(y_i + \eta d_i) & \in \mathcal{C}_i^* & i = 1 \ldots m,
+\end{align}
+```
+and:
+```math
+\sum_{i=1}^m b_i^\top (y_i + \eta d_i) < \sum_{i=1}^m b_i^\top y_i,
+```
+for any feasible dual solution ``y``. The latter simplifies to
+``\sum_{i=1}^m b_i^\top d_i < 0``. Note that conic duality is defined such that
+this inequality is independent of whether the objective sense is minimization or
+maximization.
+
+If the solver has found a certificate of infeasibility:
+
+ * [`TerminationStatus`](@ref) must be `INFEASIBLE`
+ * [`DualStatus`](@ref) must be `INFEASIBILITY_CERTIFICATE`
+ * [`ConstraintPrimal`](@ref) must be the corresponding value of ``d``
+ * [`DualObjectiveValue`](@ref) must be the value
+   ``\sum_{i=1}^m b_i^\top d_i``.