Equivalence of optimization problems #
We define equivalence and strong equivalence, and several equivalence-preserving transformations.
References #
- [BV04] S. Boyd and L. Vandenberghe, Convex Optimization
- [Gra05] M. C. Grant, Discipliend Convex Programming
Regular notion of equivalence between optimization problems. We require maps (φ, ψ)
between
teh domains of p
and q
such that they map optimal points to optimal points.
- phi : D → E
- psi : E → D
- phi_optimality : ∀ (x : D), p.optimal x → q.optimal (self.phi x)
- psi_optimality : ∀ (x : E), q.optimal x → p.optimal (self.psi x)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Minimization.Equivalence.refl = { phi := id, psi := id, phi_optimality := ⋯, psi_optimality := ⋯ }
Instances For
Equations
- E.symm = { phi := E.psi, psi := E.phi, phi_optimality := ⋯, psi_optimality := ⋯ }
Instances For
Equations
Instances For
Equations
- Minimization.Equivalence.instTrans = { trans := fun {a : Minimization D R} {b : Minimization E R} {c : Minimization F R} => Minimization.Equivalence.trans }
An equivalence induces a map between the solution set of p
and the solution set of q
.
Equations
- E.toFwd sol = { point := E.phi sol.point, isOptimal := ⋯ }
Instances For
An equivalence induces a map between the solution set of q
and the solution set of p
.
Equations
- E.toBwd sol = { point := E.psi sol.point, isOptimal := ⋯ }
Instances For
Notion of equivalence used by the DCP procedure. It makes some proofs simpler. The
optimality-preserving requirements of (φ, ψ)
are replaced by:
- for every
p
-feasiblex
,g(φ(x)) ≤ f(x)
, i.e.φ
gives a lower bound off
. - for every
q
-feasibley
,f(ψ(y)) ≤ g(y)
, i.e.ψ
fives a lower bound ofg
.
- phi : D → E
- psi : E → D
- phi_feasibility : ∀ (x : D), p.feasible x → q.feasible (self.phi x)
- psi_feasibility : ∀ (y : E), q.feasible y → p.feasible (self.psi y)
- phi_optimality : ∀ (x : D), p.feasible x → q.objFun (self.phi x) ≤ p.objFun x
- psi_optimality : ∀ (y : E), q.feasible y → p.objFun (self.psi y) ≤ q.objFun y
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Minimization.StrongEquivalence.refl = { phi := id, psi := id, phi_feasibility := ⋯, psi_feasibility := ⋯, phi_optimality := ⋯, psi_optimality := ⋯ }
Instances For
Equations
- E.symm = { phi := E.psi, psi := E.phi, phi_feasibility := ⋯, psi_feasibility := ⋯, phi_optimality := ⋯, psi_optimality := ⋯ }
Instances For
Equations
Instances For
Equations
- Minimization.StrongEquivalence.instTrans = { trans := fun {a : Minimization D R} {b : Minimization E R} {c : Minimization F R} => Minimization.StrongEquivalence.trans }
Equal problems are equivalent. Note that the domain needs to be the same. We intentionally do
not define this as h ▸ Equivalence.refl (p := p)
so that phi
and psi
can be easily
extracted.
Equations
- Minimization.Equivalence.ofEq h = { phi := id, psi := id, phi_optimality := ⋯, psi_optimality := ⋯ }
Instances For
As expected, an Equivalence
can be built from a StrongEquivalence
.
Equations
- Minimization.Equivalence.ofStrongEquivalence E = { phi := E.phi, psi := E.psi, phi_optimality := ⋯, psi_optimality := ⋯ }
Instances For
Equations
Instances For
Equations
Instances For
Mapping the objective function by monotonic functions yields an equivalence. Also, mapping the whole domain by a function with a right inverse.
See [BV04,p.131] where g
is ψ₀
.
Equations
- Minimization.Equivalence.map_objFun h = { phi := id, psi := id, phi_optimality := ⋯, psi_optimality := ⋯ }
Instances For
Instances For
This is simply a change of variables, see ChangeOfVariables.toEquivalence
and [BV04,p.130].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rewriting the objective function or the constraints leads to equivalent problems.
We assume constraints are joind by ∧
. A problem with several constraints can be written as
⟨f, [[c1, ..., cn]]⟩
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Other equivalence-preserving transformations. These are not used by any tactic but can be used directly. They provide evidence that our notion of equivalence captures the expected transformations.
We can always add a redundant constraint. This might be useful to help the reduction algorithm
infer some constraints that cannot be easily infered by arith
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
See [BV04,p.131] where g
is ψᵢ
.
Equations
Instances For
See [BV04,p.131] where g
is ψₘ₊ᵢ
.
Equations
Instances For
Adding a slack variable [BV04,p.131].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Eliminate equality constraints [BV04,p.132].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Decompose constraint by introducing another equality constraint [BV04,p.132].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Epigraph form [BV04,p.134].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Suppose D ≃ S × E
. Let problem p := ⟨f, cs⟩
be defined over D
. Every x : D
maps
one-to-one to (s, y) : S × E
. Assume that x
is p
-feasible iff s = g y
and cs' x
. We can
think of s
as a new variable. If changing s
does not change the objective function and the new
constraints c
respect monotonicity in S
, we have that p
is equivalent to the problem
⟨f, s ≤ g y ∧ cs' x⟩
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to eq_to_le_left
with the monotonicity condition on c
flipped. In this case we have
that P
is equivalent to ⟨f, g y ≤ s ∧ cs' x⟩
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Introduce a new variable s
that replaces occurrences of (non-linear) g x
in the original
problem. The resulting problem has an extra constraint s ≤ g y
. The objective funciton and the
rest of the constraints need to satisfy the appropriate monotonicity conditions [Gra05,4.2.1].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to linearization_mono
with the monotonicity conditions flipped. The resulting problem
adds the exactra constraint g y ≤ s
in this case [Gra05,4.2.1].
Equations
- One or more equations did not get rendered due to their size.
Instances For
This can be seen as a generalization of linearization_mono
, where d
is the graph
implementation of g
. This is not used by the DCP procedure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to graph_expansion_greatest
but in the flipped monotonicity context, c.f.
linearization_antimono
. This is not used by the DCP procedure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Version of graph_expansion_least
that works with vectors.
Equations
- One or more equations did not get rendered due to their size.