Changeset 115 for docs/trunk/omega-test-slides

Legend:

Unmodified

Added

Removed

• docs/trunk/omega-test-slides/crg-group-beamer.sty

  r106	r115
  1	\definecolor{KentBlue}{rgb}{0.0,0.2196,0.5098}(削除) (削除ここまで)
  2	\definecolor{KentRed}{rgb}{0.7058,0.0117,0.3607}(削除) (削除ここまで)
  3	\definecolor{KentGreen}{rgb}{0.0,0.4785,0.3686}(削除) (削除ここまで)
  1	\definecolor{KentBlue}{rgb}{0.0,0.2196,0.5098}(追記) % (追記ここまで)
  2	\definecolor{KentRed}{rgb}{0.7058,0.0117,0.3607}(追記) % 180, 3, 92 (追記ここまで)
  3	\definecolor{KentGreen}{rgb}{0.0,0.4785,0.3686}(追記) % 0, 122, 94 (追記ここまで)
  4	4
  5	5	\usepackage{pifont}

• docs/trunk/omega-test-slides/omega-test.tex

  r113	r115
  10	10
  11	11	%4up
  12	(追記) %notes (追記ここまで)
  12	13	\usepackage{crg-group-beamer}
  13	14
  …	…
  86	87	\begin{itemize}
  87	88	\item Equality: $\displaystyle\sum_{i=0}^n a_i x_i = 0$
  88	\item Inequality: $\displaystyle\sum_{i=0}^n a_i x_i (削除) >= (削除ここまで) 0$
  89	\item Inequality: $\displaystyle\sum_{i=0}^n a_i x_i (追記) \geq (追記ここまで) 0$
  89	90	\item $x_0 = 1, \therefore a_0$ is the constant term
  90	91	\end{itemize}
  …	…
  211	212	\end{itemize}
  212	213	\end{itemize}
  214	(追記) \end{frame} (追記ここまで)
  215	(追記) (追記ここまで)
  216	(追記) \begin{frame}[fragile] (追記ここまで)
  217	(追記) \frametitle{Variable Elimination} (追記ここまで)
  218	(追記) We want to eliminate the variables one by one. (追記ここまで)
  219	(追記) Pick a variable (for illustration, $x_n$) and rephrase the set of inequalities 0ドル \leq \displaystyle\sum_{i=0}^n a_i x_i$ as: (追記ここまで)
  220	(追記) (追記ここまで)
  221	(追記) \begin{tabular}{cll} (追記ここまで)
  222	(追記) $a_n$ & Rephrase & Bound\\ \hline (追記ここまで)
  223	(追記) 0 & \textit{$x_n$ already eliminated} & \\ \hline (追記ここまで)
  224	(追記) Pos & $\displaystyle\sum_{i=0}^{n-1} a_i x_i \leq a x_n$ where $a = a_n$ & Lower\\ \hline (追記ここまで)
  225	(追記) Neg & $b x_n \leq \displaystyle\sum_{i=0}^{n-1} a_i x_i$ where $b = -a_n$ & Upper\\ \hline (追記ここまで)
  226	(追記) (追記ここまで)
  227	(追記) \end{tabular} (追記ここまで)
  228	(追記) (追記ここまで)
  229	(追記) N.B. $a > 0,ドル $b > 0$ (追記ここまで)
  230	(追記) (追記ここまで)
  231	(追記) \end{frame} (追記ここまで)
  232	(追記) (追記ここまで)
  233	(追記) \begin{frame}[fragile] (追記ここまで)
  234	(追記) \frametitle{Bounding Pairs} (追記ここまで)
  235	(追記) Consider each (upper,lower) bound pair on $x$: (追記ここまで)
  236	(追記) (追記ここまで)
  237	(追記) $\beta \leq bx$ and $ax \leq \alpha$ (追記ここまで)
  238	(追記) (追記ここまで)
  239	(追記) $a\beta \leq abx$ and $abx \leq b\alpha$ (追記ここまで)
  240	(追記) (追記ここまで)
  241	(追記) \note{It is important here that $a$ and $b$ are positive, (追記ここまで)
  242	(追記) otherwise it would screw up the inequalities (multiplying (追記ここまで)
  243	(追記) an inequality by a negative number reverses the direction (追記ここまで)
  244	(追記) of the inequality)} (追記ここまで)
  245	(追記) (追記ここまで)
  246	(追記) $a\beta \leq abx \leq b\alpha$ (追記ここまで)
  247	(追記) (追記ここまで)
  248	(追記) We can eliminate $x$ ($a\beta \leq b\alpha$) but there may be solutions to that but not the original. (追記ここまで)
  249	(追記) Consider 7ドル \leq 3x$ and 5ドルx \leq 14$; 35ドル \leq 42$ has a solution! (追記ここまで)
  250	(追記) (追記ここまで)
  251	(追記) \note{Bear in mind we are looking for integer solutions to $x$. (追記ここまで)
  252	(追記) These examples (which are not normalised, merely illustrative) (追記ここまで)
  253	(追記) have no integer solution for $x,ドル but after $x$ is eliminated (追記ここまで)
  254	(追記) the equation is solveable.} (追記ここまで)
  255	(追記) (追記ここまで)
  256	(追記) \end{frame} (追記ここまで)
  257	(追記) (追記ここまで)
  258	(追記) %TODO can the above be shown *clearly* with graphics? The original paper doesn't do a good job (追記ここまで)
  259	(追記) %TODO maybe the number line? (追記ここまで)
  260	(追記) (追記ここまで)
  261	(追記) \begin{frame}[fragile] (追記ここまで)
  262	(追記) \frametitle{Shadows} (追記ここまで)
  263	(追記) \begin{itemize} (追記ここまで)
  264	(追記) \item Set of constraints $C_R$ ($a\beta \leq b\alpha$ for all pairs) is real shadow of constraints $C$. (追記ここまで)
  265	(追記) %\item If ($L,ドル$U$) are the number of (lower,upper) bounds on eliminated variable, the real shadow introduces $L.U$ new equations. (追記ここまで)
  266	(追記) \item We at least know: $\lnot \operatorname{hasIntSol}(C_R) \implies \lnot \operatorname{hasIntSol}(C)$ (追記ここまで)
  267	(追記) \end{itemize} (追記ここまで)
  268	(追記) $\operatorname{hasIntSol}(C_R) \land \lnot \operatorname{hasIntSol}(C) \implies (\lnot \exists x: a\beta \leq abx \leq b\alpha)$ (追記ここまで)
  269	(追記) \note{Using: (追記ここまで)
  270	(追記) (追記ここまで)
  271	(追記) $(A \land \lnot B) \implies C$ (追記ここまで)
  272	(追記) (追記ここまで)
  273	(追記) $\lnot (A \land \lnot B) \lor C$ (by definition) (追記ここまで)
  274	(追記) (追記ここまで)
  275	(追記) $(\lnot A \lor B) \lor C$ (De Morgan's Law) (追記ここまで)
  276	(追記) (追記ここまで)
  277	(追記) $(\lnot A \lor C) \lor B$ (Distributivity of Or) (追記ここまで)
  278	(追記) (追記ここまで)
  279	(追記) $\lnot (A \land \lnot C) \lor B$ (De Morgan's Law) (追記ここまで)
  280	(追記) (追記ここまで)
  281	(追記) $(A \land \lnot C) \implies B$ (by definition) (追記ここまで)
  282	(追記) } (追記ここまで)
  283	(追記) $\operatorname{hasIntSol}(C_R) \land (\exists x: a\beta \leq abx \leq b\alpha) \implies \operatorname{hasIntSol}(C)$ (追記ここまで)
  284	(追記) \end{frame} (追記ここまで)
  285	(追記) (追記ここまで)
  286	(追記) \begin{frame}[fragile] (追記ここまで)
  287	(追記) \frametitle{Integers} (追記ここまで)
  288	(追記) \includegraphics[width=100mm]{Omega-Test-Number-Line.png} (追記ここまで)
  289	(追記) (追記ここまで)
  290	(追記) $\neg \exists x: a\beta \leq abx \leq b\alpha \implies b\alpha - a\beta \leq ab - a - b$ (追記ここまで)
  291	(追記) (追記ここまで)
  292	(追記) \note{Using: (追記ここまで)
  293	(追記) (追記ここまで)
  294	(追記) $A \implies B$ (追記ここまで)
  295	(追記) (追記ここまで)
  296	(追記) $\lnot A \lor B$ (by definition) (追記ここまで)
  297	(追記) (追記ここまで)
  298	(追記) $\lnot A \lor \lnot \lnot B$ ($\lnot\lnot A = A$) (追記ここまで)
  299	(追記) (追記ここまで)
  300	(追記) $\lnot B \implies \lnot A$ (by definition) (追記ここまで)
  301	(追記) } (追記ここまで)
  302	(追記) (追記ここまで)
  303	(追記) $b\alpha - a\beta > ab - a - b \implies \exists x: a\beta \leq abx \leq b\alpha$ (追記ここまで)
  304	(追記) (追記ここまで)
  305	(追記) $b\alpha - a\beta \geq ab - a - b + 1 \implies \ldots$ (追記ここまで)
  306	(追記) (追記ここまで)
  307	(追記) $b\alpha - a\beta \geq (a - 1)(b - 1) \implies \ldots$ (追記ここまで)
  308	(追記) (追記ここまで)
  309	(追記) Term this constraint $C_D$. $\operatorname{hasIntSol}(C_D) \implies \exists x: a\beta \leq abx \leq b\alpha$. (追記ここまで)
  310	(追記) Therefore $\operatorname{hasIntSol}(C_R) \land \operatorname{hasIntSol}(C_D) \implies \operatorname{hasIntSol}(C)$ (追記ここまで)
  311	(追記) (追記ここまで)
  312	(追記) N.B. $a = 1 \vee b = 1 \implies b\alpha - a\beta \geq 0 \implies b\alpha \geq a\beta$ (追記ここまで)
  313	(追記) (追記ここまで)
  314	(追記) (追記ここまで)
  213	315	\end{frame}
  214	316
  …	…
  268	370	% TODO wrap my head around this!
  269	371
  372	(追記) %TODO be careful - if a and b are identical, you still can't cancel them! (追記ここまで)
  373	(追記) (追記ここまで)
  374	(追記) \begin{frame}[fragile] (追記ここまで)
  375	(追記) \frametitle{Real and Dark Shadows} (追記ここまで)
  376	(追記) %True, but irrelevant here: (追記ここまで)
  377	(追記) %$\forall X. \operatorname{hasIntSol}(X) \implies \operatorname{hasRealSol}(X)$ (追記ここまで)
  378	(追記) (追記ここまで)
  379	(追記) $C_R$ is the real shadow of $C,ドル $X_D$ is the dark shadow of $C$ (追記ここまで)
  380	(追記) (追記ここまで)
  381	(追記) $\forall X. (C_R = C_D) \implies (\operatorname{hasIntSol}(C) \iff \operatorname{hasIntSol}(C_R))$ (追記ここまで)
  382	(追記) (追記ここまで)
  383	(追記) $\forall X. \lnot \operatorname{hasIntSol}(C_R) \implies \lnot \operatorname{hasIntSol}(C)$ (追記ここまで)
  384	(追記) $\operatorname{hasIntSol}(C_R) \land \operatorname{hasIntSol}(C_D) \implies \operatorname{hasIntSol}(C)$ (追記ここまで)
  385	(追記) (追記ここまで)
  386	(追記) If $\operatorname{hasIntSol}(X_R) \wedge \neg \operatorname{hasIntSol}(X_D) \wedge (X_R \neq X_D),ドル we can't yet tell the value of $\operatorname{hasIntSol}(X$ (追記ここまで)
  387	(追記) (追記ここまで)
  388	(追記) \end{frame} (追記ここまで)
  389	(追記) (追記ここまで)
  270	390
  271	391	\section{Tricky Parts}

Note: See TracChangeset for help on using the changeset viewer.