|
Size: 1836
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 \usepackage{amsmath}% \setcounter{MaxMatrixCols}{30}% \usepackage{amsfonts}% \usepackage{amssymb}% \usepackage{graphicx} \usepackage{geometry} \newtheorem{theorem}{Theorem} \newtheorem{acknowledgement}[theorem]{Acknowledgement} \newtheorem{algorithm}[theorem]{Algorithm} \newtheorem{axiom}[theorem]{Axiom} \newtheorem{case}[theorem]{Case} \newtheorem{claim}[theorem]{Claim} \newtheorem{conclusion}[theorem]{Conclusion} \newtheorem{condition}[theorem]{Condition} \newtheorem{conjecture}[theorem]{Conjecture} \newtheorem{corollary}[theorem]{Corollary} \newtheorem{criterion}[theorem]{Criterion} \newtheorem{definition}[theorem]{Definition} \newtheorem{example}[theorem]{Example} \newtheorem{exercise}[theorem]{Exercise} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{notation}[theorem]{Notation} \newtheorem{problem}[theorem]{Problem} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{remark}[theorem]{Remark} \newtheorem{solution}[theorem]{Solution} \newtheorem{summary}[theorem]{Summary} \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }{\ \rule{0.5em}{0.5em}} \geometry{left=0.5in,right=0.5in,top=0.5in,bottom=0.5in} |
|
| Line 41: | Line 11: |
| %%end-prologue%% 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. |
The following is taken from page 9 of Cousot05VMCAI reference - see my bibtex. |
| Line 44: | Line 13: |
| Let $M(x)=M_0 + \sum\limits^m_{k=1} x_k.M_k }}} |
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