Differences between revisions 1 and 10 (spanning 9 versions)
Revision 1 as of 2007-02-13 23:11:14
Size: 424
Editor: dot
Comment:
Revision 10 as of 2020-01-26 22:45:14
Size: 1466
Editor: 68
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 x0Rn and the values at the end of the loop are denoted x where n is the number of variables. Then xk is the variable values after the kth loop.

Let

M(x)=M0+k=1mxk.Mk

with symmetric matrices (Mk=Mk, and positive semidefiniteness (can you say that?) defined as:

M(x)0XRN:XM(x)X0

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:

{xRm:M(x)0Minimizing  cx

where cRm 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}nandthevaluesattheendofthelooparedenotedxwherenisthenumberofvariables.Thenx_kisthevariablevaluesafterthek{th}$$ loop.

Let

M(x)=M0+k=1mxk.Mk

with symmetric matrices (Mk=Mk, 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 cRm is a real given vector and M is called the linear matrix inequality

SemiDefinite (last edited 2020-01-26 22:45:14 by 68)