## source code for slides-cp2000

The document Universally Quantified Interval Constraint Solving, by Frédéric Benhamou and Frédéric Goualard (Institut de Recherche en Informatique de Nantes, France), uses prosper and incorporates lots of overlays and PostScript images. LaTeX source:

\documentclass[pdf,contemporain,slideColor,colorBG,accumulate,nototal]{prosper}
\usepackage{macros-cp}

\newcommand{\ItvSet}{ITVSET}
\newcommand{\ITVCC}[2]{$#1,2$}
\newcommand{\ItvComplement}{ITVCOMPL}
\newcommand{\SetVarItvBox}{SETVARITVBOX}
\newcommand{\RSet}{\Re{}}
\newcommand{\Vector}[1]{{\bf #1}}
\newcommand{\Relation}{Relation}
\newcommand{\FUNC}{FUNC}
\newcommand{\Hull}{Hull}
\newcommand{\CRel}{CRel}
\newcommand{\UCRel}{UCRel}
\newcommand{\ALGO}{ALGO}

\title{Universally Quantified~\ \\ Interval Constraint Solving}
\author{Frédéric Benhamou and Frédéric Goualard}
\institution{Institut de Recherche en Informatique de Nantes, France}

\begin{document}
\maketitle

%--------------------------------------------------------------- first slide

\overlays{4}{%
\begin{slide}{Motivations}
\small

\vspace*{-10pt}

Object $\Omega$ with trajectory:
{\scriptsize$\left[\begin{array}{l} x(\theta)=3\sin\theta\cos\theta(\sin\theta-\cos\theta)\\ y(\theta)=3\sin\theta\cos\theta(\sin\theta+\cos\theta)\\ z(\theta)=0 \end{array}\right.$}

\PDForPS{%
\untilSlide{3}{\rput[t](8.9,1.9){\includegraphics[angle=45,bb=36 603 243 801,width=5.5cm]{trajectoirePDF.ps}}}}{%
\untilSlide{3}{\rput[t](8.9,1.9){\includegraphics[angle=45,bb=36 603 243 801,width=5.5cm]{trajectoirePS.ps}}}}%
\onlyInPDF{\fromSlide{4}{\rput[t](8.5,.6){\includegraphics[width=4cm]{exemple-WOpAC-2.ps}}}}%

\fromSlide{2}{%
\vspace*{10pt}
\begin{minipage}{5cm}
Positions of a camera $\Gamma$ s.t. \\ $|\Gamma,\Omega|\geq0.5$ at any time?
\end{minipage}}

\fromSlide{3}{%
\vspace*{1.5cm}
{\fontsize{6pt}{6pt}\selectfont$\forall\theta\in\ITVCC{-\pi}{\pi}\colon$\\
$\sqrt{(3\sin\theta\cos\theta(\sin\theta-\cos\theta)-x)^2+ (3\sin\theta\cos\theta(\sin\theta+\cos\theta)-y)^2+ z^2}\geq0.5$}}%

\fromSlide{4}{Non-linear real constraint: compulsory to solve it
\emph{soundly}}

\end{slide}}

%------------------------------------------------------------------- next slide

\begin{slide}{Outline}

\vspace*{-8pt}
\begin{itemize}
\item Sound techniques
\begin{itemize}
\item Cylindrical Algebraic Decomposition
\item Interval arithmetic and inner-approximation computation
\end{itemize}
\item Complete techniques
\begin{itemize}
\item Interval constraint solving
\end{itemize}
\item Interval constraint solving and soundness
\item Solving constraints with universal quantifiers
\item Conclusion and perspectives
\end{itemize}
\end{slide}

%------------------------------------------------------------------- next slide

\overlays{2}{%
\begin{slide}{Cylindrical Algebraic Decomposition}

[Collins, 1973] (quantifier elimination)

\begin{itemize}
\item Powerful method (handling of universal/existential quantifiers)
\item Sound solving of real constraints
\end{itemize}

\FromSlide{2}%
But:
\begin{itemize}
\item Method restricted to polynomial constraints
\item High complexity (time consuming)
\end{itemize}

\end{slide}}

%------------------------------------------------------------------ next slide

\begin{slide}{Interval Arithmetic}

\vspace*{-11pt}
\scriptsize

[Moore, 1966] Interval set \ItvSet:
$\ITVCC{a}{b}=\{x\in\RSet\mid a\leq x\leq b\}$

\medskip
\textbf{Interval extension:}
\begin{itemize}
\item \emph{Extension of a real function.} $f\colon\RSet^n\to\RSet$,
$F\colon\ItvSet^n\to\ItvSet$ s.t.
$\forall\Vector{B}\colon\mathcal{D}_f(\Vector{B})\subseteq F(\Vector{B})$

\vspace*{-.2cm}
\PDForPS{%
\hspace*{-.1cm}\includegraphics[bb=45 359 563 512,height=3.3cm]{evaluation-forme-horner-2.ps}}{%
\hspace*{-.1cm}\includegraphics[bb=45 359 563 512,height=3.3cm]{evaluation-forme-horner-2-ps.ps}}
\item \emph{Extension of a real relation $\rho\subseteq\RSet^n~$.} Set of
boxes $\mathcal{R}$ such that:

\vspace*{-24pt}
$$(a_1,\dots,a_n)\in\rho\Rightarrow\exists(I_1,\dots,I_n)\in\mathcal{R} \mbox{ s.t. } a_1\in I_1,\dots, a_n\in I_n$$
\end{itemize}
\end{slide}

%------------------------------------------------------------------ next slide

\overlays{5}{%
\begin{slide}{Approximation of a relation}
\small

\vspace*{-12pt}
Outer approximation of $\rho$: $\Hull{\rho}=\bigcap\{\Vector{B}\in\ItvSet^n \mid \Relation\subseteq \Vector{B}\}$
Inner approximation of $\rho$:

\vspace*{-.6cm}
$$\FUNC{Inner}(\rho)=\{a\in\RSet^n\mid\Hull{\{a\}}\subseteq\rho\}$$
Splitting/evaluation scheme (SES) for straightforward
inner approximation computation:

\textbf{Example.} $c\colon f(x)\leq0$?
\begin{center}
\PDForPS{%
\onlySlide*{1}{%
\includegraphics[bb=50 331 566 509,height=3cm]{correction-eval-1.ps}}%
\onlySlide*{2}{%
\includegraphics[bb=50 331 566 509,height=3cm]{correction-eval-2.ps}}%
\onlySlide*{3}{%
\includegraphics[bb=50 331 566 509,height=3cm]{correction-eval-3.ps}}%
\onlySlide*{4}{%
\includegraphics[bb=50 331 566 509,height=3cm]{correction-eval-4.ps}}%
\fromSlide*{5}{%
\includegraphics[bb=50 331 566 509,height=3cm]{correction-eval-5.ps}}}{%
\includegraphics[bb=50 331 566 509,height=3cm]{correction-eval-ps.ps}}%
\end{center}
\end{slide}}

%-------------------------------------------------------------------- next slide

\overlays{5}{%
\begin{slide}{EIA4}
\small

\vspace*{-12pt}
[Jardillier \& Languénou, 1998] (Modelling of camera movements)

Solving $\forall v\in\ITVCC{a}{b}\colon c(x,v)$ with the SES:

\bigskip
\begin{center}
\onlySlide*{1}{%
\includegraphics[height=4cm]{eia4-d.eps}}%
\onlySlide*{2}{%
\includegraphics[height=4cm]{eia4-c.eps}}%
\onlySlide*{3}{%
\includegraphics[height=4cm]{eia4-b.eps}}%
\onlySlide*{4}{%
\includegraphics[height=4cm]{eia4-a.eps}}%
\onlySlide*{5}{%
\includegraphics[height=4cm]{eia4.eps}}%
\end{center}

\vspace*{-10pt}
\onlySlide{5}{$\Rightarrow$ algorithm EIA4 (very costly)}
\end{slide}}

%-------------------------------------------------------------------- next slide

\begin{slide}{Interval constraint solving}
\small

\vspace*{-10pt}
\begin{itemize}
\item Variables $x_1,\dots,x_n$ $\rightarrow$ domains $D_1,\dots,D_n$
\item Constraint $c(x_1,\dots,x_n)$ \\
\hspace*{1cm}$\rightarrow$ \emph{contracting operator} $\CNO{c}$ \par
\hspace*{1cm}{\footnotesize[\textsc{Benhamou} \& \textsc{Older}, \textsc{Apt}, \dots]}

\medskip
{\small$\Vector{D}=D_1\times\cdots\times D_n$
\raisebox{-7pt}{\PDForPS{\includegraphics[height=20pt]{cno.eps}}{%
\includegraphics[height=20pt]{cno-ps.eps}}}
$\Vector{D'}\subseteq\Vector{D}$}\\[6pt]
\item Properties: contractance, monotony,\\
\emph{completeness} ($\CRel{c}\cap\Vector{D}\subseteq N[c](\Vector{D})$)
\item Constraint system $c_1,\dots,c_m$~:
domain propagation algorithm (AC3 [\textsc{Mackworth,1977}])
\item Discarding values: \emph{local consistency} $+$ splitting
\end{itemize}
\end{slide}

%------------------------------------------------------------------------ next slide

\begin{slide}{Box consistency}
\small

\vspace*{-10pt}
[Benhamou, McAllester, Van Hentenryck, 1994]

Given $c$ a real constraint, $C$ an interval extension for $c$,
$\Vector{B}=I_1\times\allowbreak\cdots\times I_n$ a box

$c$ is \emph{box-consistent w.r.t.\ \Vector{B}} iff $\forall k\in\{1,\dots,n\}\colon$

\vspace*{-24pt}
{\footnotesize
$$\begin{array}{l} I_k=\Hull{I_k\cap\{a_k\in \RSet\mid C(I_1,\dots,I_{k-1}, \Hull{\{a_k\}},I_{k+1},\dots,I_n)\}} \end{array}$$

\vspace*{-2cm}
\PDForPS{%
\rput(8.3,-1.5){\includegraphics[bb=48 357 563 573,
height=3cm]{box-consistance-1.ps}}}{%
\rput(8.3,-1.5){\includegraphics[bb=48 357 563 573,height=3cm]{box-consistance-ps.ps}}}

\vspace{2.6cm}
Box consistency operator:

\vspace{-30pt}
\begin{multline*}
\Vector{B}\cap\CRel{c} \subseteq \FUNC{OCb}_{c}(\Vector{B})=
\max\{\Vector{B'}\mid
\Vector{B'}\subseteq\Vector{B}\\[-5pt]
\wedge c\mbox{ is box-consistent \Wrt\ }
\Vector{B'}\}
\end{multline*}
\end{slide}

%----------------------------------------------------------------------- next slide

\overlays{2}{%
\begin{slide}{Interval constraint solving}
\small

%\vspace*{-10pt}
\begin{itemize}
\item Efficiency
(systems of non-linear real equations with punctual solutions)
\item No restriction to polynomials
\item Completeness: no solution lost
\end{itemize}

\FromSlide{2}%
But:
\begin{itemize}
\item Continuum of solutions? (systems of inequations)
\item Soundness ?
\item Quantified variables?
\end{itemize}
\end{slide}}

%------------------------------------------------------------------------ next slide

\overlays{2}{%
\begin{slide}{Achieving soundness}
\small

Computing with interval constraint prog. techniques on $\neg c$:\\
$\Rightarrow$ completeness for $\neg c$\\
$\Rightarrow$ \emph{correctness} for $c$

For discarded box $\Vector{B}=I_1\times\cdots\times I_n\times I_v$:
$\neg(\exists x_1\dots\exists x_n\exists v\colon x_1\in I_1\dots x_n\in I_n v\in I_v\wedge \neg c(x_1,\dots,x_n,v))$

\FromSlide{2}%
\medskip
That is: $\forall x_1\dots\forall x_n\forall v\colon x_1\in I_1\dots x_n\in I_n v\in I_v\Rightarrow c(x_1,\dots,x_n,v)$\\
(computation of inner approximation for \CRel{c})

\bigskip
Negation of $c$: easy for inequations
\end{slide}}

%--------------------------------------------------------------------- next slide

\overlays{2}{%
\begin{slide}{Handling quantifiers}
\small

\vspace*{-10pt}
Solving $\forall v\in I_v\colon c$

\vspace*{-7pt}
\begin{itemize}
\item Computing box consistency on $\neg c$
\item Saving discarded boxes $B'=I'_1\times\cdots\times I'_n\times I'_v$
with $I_v=I'_v$
\item Splitting undiscarded boxes and iterating
\end{itemize}

\FromSlide{2}%
Solving
$\forall v\in I^1\colon c_1\wedge\cdots\wedge\forall v\in I^m\colon c_m$

\vspace*{-7pt}
\begin{itemize}
\item Applying the previous scheme on $c_1,\dots,c_n$ in sequence once
\item Using the output after $c_i$ as input for $c_{i+1}$
\end{itemize}

\end{slide}}

%--------------------------------------------------------------------- next slide

\begin{slide}{Solving $\forall v\in I_v\colon c$}
\footnotesize

\vspace*{-12pt}
\begin{tabbing}
123\=12345\=12345\=12345\=12345\=\kill
\NUM{1}\>$\ALGO{ICAb3}_{c}$($\KWD{in}\colon\Vector{B}\in\ISet^n, % v\in\VariableSet_{\RSet}$;
$\:\KWD{out}\colon\GSet{W}\in\PIFSetN{n}$)\\[-3pt]
\NUM{2}\>\BEGIN \\[-3pt]
\NUM{3} \>\> \Vector{B'} \Gets \OCB{c}{\Vector{B}} \\[-3pt]
\NUM{4} \>\> \IF{\Domain{v}{\Vector{B'}}=\Domain{v}{\Vector{B}}} \THEN \\[-3pt]
\NUM{5}\>\>\> \Vector{D} \Gets \OCB{\CNeg{c}}{\Vector{B'}}\\[-3pt]
\NUM{6}\>\>\> $\GSet{W}$\Gets $\ItvComplement{\Vector{B'}}{\SetVarItvBox{\Vector{D}}{v}{\Vector{B'}}}$\\[-3pt]
\NUM{7}\>\>\> \IF{\Vector{D}\neq\emptyset ~\AND~ \neg\CanonicalV{\Vector{D}}{v}} \THEN \\[-3pt]
\NUM{8}\>\>\>\> $(\Vector{D_1},\Vector{D_2})$ \Gets %
\SplitV{v}{\SetVarItvBox{\Vector{D}}{v}{\Vector{B'}}}\\[-3pt]
\NUM{9}\>\>\>\> $\GSet{W}$ \Gets $\GSet{W}\cup\ICBThree{c}{\Vector{D_1}}{v}\cup\ICBThree{c}{\Vector{D_2}}{v}$ \\[-3pt]
\NUM{10}\>\>\> \FI \\[-3pt]
\NUM{11}\>\>\> \RETURN{\GSet{W}} \\[-3pt]
\NUM{12} \>\> \ELSE \\[-3pt]
\NUM{13} \>\>\> \RETURN{\emptyset} \\[-3pt]
\NUM{14}\>\END
\end{tabbing}
\end{slide}

%----------------------------------------------------------------------- next slide

\begin{slide}{Constraint systems and $\forall$}
\footnotesize

\vspace*{-14pt}
Solving
$\forall v\in I^1\colon c_1\wedge\cdots\wedge\forall v\in I^m\colon c_m$

\begin{tabbing}
123\=12345\=12345\=12345\=12345\=12345\=\kill
\NUM{1}\>\FUNC{ICAb5}($\KWD{in}\colon\Set=\{(c_1,I^1),\dots, (c_m,I^m)\},$\\[-5pt]
\>\>$\GSet{A}\in\PIFSetN{n}$, $v\in\VariableSet_{\RSet}$; %
$\:\KWD{out}\colon\GSet{W}\in\PIFSetN{n}$)\\[-6pt]
\NUM{2}\>\BEGIN \\[-6pt]
\NUM{3}\>\> \IF{\Set\neq\emptyset} \THEN\\[-6pt]
\NUM{4}\>\>\> $\GSet{B} \Gets \emptyset$\\[-6pt]
\NUM{5}\>\>\> \FOREACH $\Vector{D}\in \GSet{A}$ \DO\\[-6pt]
\NUM{7}\>\>\>\> $\GSet{B}$ \Gets
$\GSet{B}\cup\ICBThree{c_1}{\SetVarItvBox{\Vector{D}}{v}{I^1},v}$\\[-6pt]
\NUM{9}\>\>\> \ENDFOREACH\\[-6pt]
\NUM{10}\>\>\> \IF{\GSet{B}=\emptyset} \THEN\\[-6pt]
\NUM{11}\>\>\>\> \RETURN{\emptyset}\\[-6pt]
\NUM{12}\>\>\> \ELSE\\[-6pt]
\NUM{13}\>\>\>\> \RETURN{\ALGO{ICAb5}(\Set
\setminus\{(c_1,I^1)\},\GSet{B},v)}\\[-6pt]
\NUM{14}\>\>\> \FI\\[-6pt]
\NUM{15}\>\> \ELSE \\[-6pt]
\NUM{16}\>\>\> \RETURN{\GSet{A}}\\[-6pt]
\NUM{17}\>\> \FI\\[-6pt]
\NUM{18}\>\END
\end{tabbing}

\end{slide}

%---------------------------------------------------------------------- next slide

\begin{slide}{Properties}
Given \UCRel{i}, relation associated with $\forall v\in I_v\colon c_i$

\bigskip
Soundness:
$$\begin{array}{l} \ALGO{ICAb3}_c(\Vector{B},v)\subseteq\FUNC{Inner}(\Vector{B}\cap\UCRel{c})\\ \ALGO{ICAb5}(\Set,\{\Vector{B}\},v)\subseteq \FUNC{Inner}(\Vector{B}\cap\UCRel{1}\cap \cdots\cap\UCRel{m}) \end{array}$$
Comparison with EIA4:
$$\ALGO{EIA4}(\{c_1,\dots,c_m\},\Vector{B},v) \subseteq\ALGO{ICAb5}(\GSet{S},\{\Vector{B}\},v)$$

%Termination
\end{slide}

%---------------------------------------------------------------------- next slide

\begin{slide}{ICAb5 vs. EIA4}
\footnotesize

\vspace*{-12pt}
All solutions:

\medskip
\begin{center}\renewcommand{\arraystretch}{.95}
\begin{tabular}{lrrr}
\hline
Benchmark &  \FUNC{EIA4}  & \FUNC{ICAb5} & $\quad\FUNC{EIA4}/\FUNC{ICAb5}$  \\
\hline
Projection$_{3,5}$ & 783 & 68 & 11\\
Projection$_{3,10}$ & $>$9000 & 3634 & $>${2}\\
Projection$_{5,5}$ & $>${9000} & {3612} & $>${2}\\
School Problem$_{3,1}$   & {156}      & {13} & {12}\\
Flying Saucer$_{4,1}$    & {1459}      & {1078} & {1}\\
Simple Circle$_{2,1}$    & {12789}    & {651} & {19}\\
Simple Circle$_{2,2}$    & {1579}    & {56} & {28}\\
\hline
\multicolumn{4}{r}{\tiny\textit{Time in s.\ on a SUN UltraSparc 1/167\,MHz.}}
\end{tabular}
\end{center}

\medskip
N.B.: first solution only $\Rightarrow$ speed-up much more important
\end{slide}

%---------------------------------------------------------------------- next slide

\begin{slide}{Conclusion and perspectives}
\footnotesize

\vspace*{-10pt}
Alg.\ ICAb5:

\vspace*{-7pt}
\begin{itemize}\setlength{\itemsep}{-1pt}
\item solving of non-linear real constraints (polynomial or not)
with one universally quantified variable per constraint
\item Speed-up compared to splitting/evaluation (EIA4)
\item Still costly
\end{itemize}

Solutions?

\vspace*{-7pt}
\begin{itemize}\setlength{\itemsep}{-1pt}
\item More precise interval extensions (Bernstein)
\item Other interval arithmetics (Kaucher/Markov, modal arithmetic)
\item Cooperation of symbolic/numerical methods (CAD?)
\end{itemize}

\vspace{-4pt}
Handling of constraints as full first-order expressions?
\end{slide}

%-------------------------------------------------------------- final slide

\overlays{5}{%
\begin{slide}{Interval constraint solving (2)}
\small
\begin{itemize}
\item Constraint system $c_1,\dots,c_m$~:
domain propagation algorithm (AC3 [\textsc{Mackworth,1977}])
\end{itemize}
\PDForPS{%
\onlySlide*{1}{%
\includegraphics[bb=136 706 304 790,width=7cm]{exemple-store-1.ps}}%
\onlySlide*{2}{%
\includegraphics[bb=136 706 304 790,width=7cm]{exemple-store-2.ps}}%
\onlySlide*{3}{%
\includegraphics[bb=136 706 304 790,width=7cm]{exemple-store-3.ps}}%
\fromSlide*{4}{%
\includegraphics[bb=136 706 304 790,width=7cm]{exemple-store-4.ps}}}{%
\includegraphics[bb=136 706 304 790,width=7cm]{exemple-store-ps.ps}}%
\FromSlide{5}
\rput[tl](0,3.4){\begin{minipage}{5cm}
Properties:
\begin{itemize}\setlength{\itemsep}{-2pt}
\item Termination
\item Contractance
\item Confluency
\item Completeness
\end{itemize}\end{minipage}}
\end{slide}
}

\end{document}