|
Size: 1836
Comment:
|
Size: 2512
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 42: | Line 42: |
| 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. | 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. |
| Line 44: | Line 44: |
| Let $M(x)=M_0 + \sum\limits^m_{k=1} x_k.M_k | 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 Cousot05vmaci, 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. \] |
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
\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}
%%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. 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 Cousot05vmaci, 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.
\]