\documentclass{beamer}
\usepackage[utf8]{inputenc}

\definecolor{ZurichBlue}{rgb}{.255,.41,.884} % RoyalBlue of svgnames
\definecolor{ZurichRed}{rgb}{1, 0, 0} % Red of svgnames
\definecolor{ZurichBlanc}{rgb}{1, 1, 1} % Red of svgnames
\definecolor{ZurichGreen}{rgb}{.196,.504,.196} % LimeGreen of svgnames
\definecolor{ZurichYellow}{rgb}{1,.648,0} % Orange of svgnames
\newcommand{\RD}[1]{ { {\textcolor{ZurichRed}{ #1}}}}
\newcommand{\BL}[1]{ { {\textcolor{ZurichBlue}{ #1}}}}
\newcommand{\GR}[1]{ { {\textcolor{ZurichGreen}{ #1}}}}
\newcommand{\BK}[1]{ { {{ #1}}}}
\newcommand{\AUT}[1]{ { \hspace*{.1in}\hfill {\small\textcolor{ZurichBlue}{ #1}}}}
\newcommand{\NATE}[1]{{\hfill\tiny{#1}}\\}
\newcommand{\NOTE}[1]{{\hfill\footnotesize{#1}}\\}
\newcommand{\URL}[1]{{\esp\hfill{\small\tt{#1}}}}

\def\it{i^*_t}
\def\iu{i^*_u}
\def\C{c_e}
\def\B{\sqrt{c_e\frac{log(\sum n_{j,t})}{n_{i,t}}}}
\def\D{\sqrt{c_e\frac{log( n_{s})}{n_{s,a}}}}
\def\A{min\left( \frac{1}{4}, \hat \sigma^2_{i,t} + \B \right)}


\def\esp{\hspace*{.2in}}
\def\bl{\hspace*{.01in}}
\def\li{\centerline{~}}
\def\blanc{\hspace*{.1in}}
\def\black{}
\def\RR{{\rm I\hspace{-0.50ex}R}}
\def\1{{\rm I\hspace{-0.50ex}{\Large 1}}}
\def\EE{{\rm I\hspace{-0.50ex}E}}
\def\NN{{\rm I\hspace{-0.50ex}N}}
\def\FIN{\end{document}}
\def\act{\mbox{\cal A}}
\usepackage{graphics}
%\usepackage{color}
%\usepackage{colortbl}
\usepackage{isolatin1}
%\setbeamertemplate{background
%canvas}{\includegraphics[width=\paperwidth,height=\paperheight]{Logos/Banner_2.jpg}}
\newcommand{\Titre}[1]{\begin{frame}\frametitle{\textcolor{ZurichBlue}{#1}}}
%\vspace*{-.5in}\hspace*{-.5in}\includegraphics[width=15cm]{Banner.jpg}

\title{Cooperation control in Parallel SAT Solving}

\author{N. Lazaar, Y. Hamadi, S. Jabbour, M. Sebag
}

\date{
\centerline{
\includegraphics[width=1.3cm]{Logos/CNRS.jpg}
\hfill
\includegraphics[width=2.9cm]{Logos/INRIA.png}
\hfill
\includegraphics[width=1.1cm]{Logos/logoLRI.pdf}
\hfill
\includegraphics[width=2.2cm]{Logos/PARISSUD.jpg}}}

%\newcommand{\Titre}[1]{\begin{frame}\frametitle{#1}}
\def\FIN{\end{document}}

\begin{document}
%\setbeamertemplate{background
%canvas}{\includegraphics[width=\paperwidth,height=\paperheight]{Logos/Banner_2.jpg}}

\frame{\titlepage}
%%%%%%%%%%%%%%
\Titre{Parallel SAT Solving}
\RD{Decentralized resolution}
\begin{itemize}
\item Each core: conflict-directed clause learning
\item Cooperation: 
each core sends the learned clauses to other cores
\item Why? additional clauses help pruning the search space.\\~\\
\end{itemize}
\RD{Previous work}\AUT{Hamadi et al. 09}
\begin{itemize}
\item Controlling the length of the shared clauses (TCP/IP congestion avoidance)  
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%
\Titre{Limitations}
\RD{Does not scale up} when the number of cores increases.\\~\\
\centerline{\bf \includegraphics[width=.9\paperwidth]{SAT/density1.png}}
\centerline{~}
\RD{Position of the problem}
\begin{itemize}
\item Dynamically control the topology of the network
\item This paper: density $\rho$ is fixed
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%
\Titre{BESS\\
Bandit Ensemble for parallel SAT Solving}
\RD{Core tasks}
\begin{itemize}
\item Design the reward
\item Adjust the decision schedule \hfill wrt internal SAT schedule\\~\\
\end{itemize}

\RD{BESS structure}
\begin{itemize}
\item Each \BL{receiver core}
\item selects $n$ \BL{emitter cores} \hfill $n = 1/2$ \# cores
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%
\Titre{Designing the reward of an emitter core}
\RD{Reward(emitter)}: sum of reward(shared clauses)\\~\\

\RD{I. Global clause rewards}
\begin{itemize}
\item Size-based: clause of length $s$ removes $2^{N-s}$ instances
\[ r(c) = -\log {1 - 2^{-s}}\] 
\item Literal-block distance\\
{\small each literal (decision level) produces unit propagations\\
LBD: difference between highest and lowest decision levels in the clause literals}
\item Mixtures of the above\\~\\
\end{itemize}
\centerline{\RD{FAIL}}
\end{frame}
%%%%%%%%%%%%%%
%%%%%%%%%%%%%%
\Titre{Designing the reward of an emitter core, 2}
\RD{II. Receiver-specific clause rewards}
\begin{itemize}
\item Literals $\ell$ are associated their activity $a(\ell)$\\
{\small \# (their assignment $\rightarrow$ failure)}
\[ r(c) = \frac{1}{c} \sum_{\ell \in c} sigmoid\left (\frac{a(\ell)}{a_{max}} \right ) \]
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%
%%%%%%%%%%%%%%
\Titre{BESS Algorithm}

\RD{In each core, independently}
\begin{itemize}
\item Maintain a reward threshold \\
\item Update the reward of alive emitters\hfill relaxation\\
\item Pr (removing emitter) = Pr (emitter reward $<$ threshold)\\
\item Turns (oldest) sleeping emitters into alive ones to achieve $n$ alive emitters at all time.
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%
\Titre{Experimental setting}
\RD{Platforms}\\
$\ast$ 8-core Intel Xeon, 16 GB RAM, 2.33GHz\\
$\ast$ 32-core AMD Opteron Proc. 6136, 64GB RAM, 2.4GHz.\\~\\

\RD{SAT instances} \hfill SAT-Challenge 2012.\\
588 SAT+UNSAT instances. \\~\\

\RD{Parameters}\\
$\ast$ CPU time limit = 30mn CPU per core\\
$\ast$ Shared clause limit size: 8\\
$\ast$ Alive emitters: 1/2 nb of cores.\\~\\

\RD{Baseline}\\
Random selection of alive emitters in each time step.
\end{frame}
%%%%%%%%%%%%%%
\Titre{Results on 8 cores}
\centerline{\includegraphics[scale=0.3]{SAT/8cores_alone.png}}
\RD{Comments}
\begin{itemize}
\item Bess slightly improves on ManySAT 2.0 for difficult problems
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%
\Titre{Results on 32 cores}
\centerline{\includegraphics[width=.5\paperwidth]{SAT/32cores-alone.png}}
\RD{Comments}
\begin{itemize}
\item Random improves on ManySAT 2.0 (confirms scalability issue)
\item Bess improves on Random and ManySAT 2.0 \\
solves the first 300 pbs in  20,000 s. versus 50,000 s.
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%
\Titre{Perspectives}
\begin{enumerate}
\item Adjust the {\em number} of emitters for each core\\~\\
\item Adjust the clause length limit\\~\\
\item Share information among cores to speed-up cooperation, enforce diversification.
\end{enumerate}
\end{frame}
\FIN



