|
Size: 424
Comment:
|
← Revision 10 as of 2020-01-26 22:45:14 ⇥
Size: 1466
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 5: | Line 5: |
| == SemiDefinite Matrices == | == SemiDefinite Matrices == |
| Line 10: | Line 10: |
| {{{#!latex2 Let $M(x):\mathbb{R}^m \rightarrow \mathbb{R}$ }}} |
The following is taken from page 9 of Cousot05VMCAI reference - see my bibtex. Suppose you have a loop in a program where the values of the variable values at the start of the loop are denoted $$x_0 \in \mathbb{R}^n$$ and the values at the end of the loop are denoted $$x$$ where $$n$$ is the number of variables. Then $$x_k$$ is the variable values after the $$k^{th}$$ loop. Let $$$M(x)=M_0 + \sum\limits^m_{k=1} x_k.M_k$$$ with symmetric matrices $$(M_k = M_k^{\top}$$, and positive semidefiniteness (can you say that?) defined as: $$$M(x) \succeq 0 \equiv \forall X \in \mathbb{R}^N : XM(x)X^{\top} \ge 0$$$ Somehow I believe that $$M$$ is an encoding of the constraints in the loop. It doesn't say that in Cousot05VMCAI, but that is what I think it means. Then the SemiDefinite programming optimization problem is to find a solution to the constraints: $$$\left\{\begin{array}{l} \exists x \in \mathbb{R}^m : M(x) \succeq 0 \\ Minimizing~~c^{\top} x \end{array}\right.$$$ where $$c \in \mathbb{R}^m$$ is a real given vector and $$M$$ is called the ''linear matrix inequality'' |
SemiDefinite What?
This page contains definitions for SemiDefinite things like matrices, programs, etc.
SemiDefinite Matrices
A positive SemiDefinite matrix is a HermitianMatrix all of whose eigenvalues are nonnegative. Thus any symmetric matrix that has a 0 on the diagonal is a SemiDefinite matrix.
SemiDefinite Programming
The following is taken from page 9 of Cousot05VMCAI reference - see my bibtex.
Suppose you have a loop in a program where the values of the variable values at the start of the loop are denoted $$x_0 \in \mathbb{R}^n$$ and the values at the end of the loop are denoted $$x$$ where $$n$$ is the number of variables. Then $$x_k$$ is the variable values after the $$k^{th}$$ loop.
Let
$$$M(x)=M_0 + \sum\limits^m_{k=1} x_k.M_k$$$
with symmetric matrices $$(M_k = M_k^{\top}$$, and positive semidefiniteness (can you say that?) defined as:
$$$M(x) \succeq 0 \equiv \forall X \in \mathbb{R}^N : XM(x)X^{\top} \ge 0$$$
Somehow I believe that $$M$$ is an encoding of the constraints in the loop. It doesn't say that in Cousot05VMCAI, but that is what I think it means. Then the SemiDefinite programming optimization problem is to find a solution to the constraints:
$$$\left\{\begin{array}{l} \exists x \in \mathbb{R}^m : M(x) \succeq 0 \\ Minimizing~~c^{\top} x \end{array}\right.$$$
where $$c \in \mathbb{R}^m$$ is a real given vector and $$M$$ is called the linear matrix inequality