Commit 090e06bd authored by Kawisorn Kamtue's avatar Kawisorn Kamtue
Browse files

Upload new file

parent 9783cc1e
\documentclass{beamer}
\usepackage[utf8]{inputenc}
\usepackage{utopia} %font utopia imported
\usepackage{graphicx}
\graphicspath{ {images/} }
\usetheme{Madrid}
\usecolortheme{default}
%------------------------------------------------------------
%This block of code defines the information to appear in the
%Title page
\title[SATZIlla] %optional
{SATZilla}
\subtitle{Portfolio-based algorithm selection for SAT}
\author[Kawisorn Kamtue] % (optional)
{Kawisorn Kamtue}
\institute[ENS Paris Saclay] % (optional)
{
\inst{1}%
ENS Paris Saclay
}
%\date[6 September 2016] % (optional)
%{13 June - 29 July 2016}
\AtBeginSection[]{
\begin{frame}
\tableofcontents[currentsection]
\end{frame}
}
\begin{document}
\begin{frame}
\titlepage
\end{frame}
\begin{frame}
\tableofcontents
\end{frame}
\section{Introduction}
\begin{frame}
\frametitle{\emph{Introduction}}
\begin{itemize}
\item The performance of
different algorithms across problem instance distributions
can be quite uncorrelated.
\item Use portfolio-based approach
\item SATZilla : first deployed in 2003 and won numerous competitions from 2007 onwards
\end{itemize}
\end{frame}
\section{Algorithm}
\subsection{Offline}
\begin{frame}
\frametitle{Methods}
\begin{itemize}
\item Identify a target distribution of problem instances and select a set of candidate solver
\item Identify features that characterize problem instances
\item Train: problem instance + solver $\rightarrow$ performance score
\item Identify one or more solvers to use for pre-solving instances
\item Choose a backup solver, using a validation data set
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Methods}
\begin{itemize}
\item Construct a classification model (Decision forest) : cost of coumputing feature is too expensive?
\item Construct a cost-sensitive classification
model (DF) for every pair of solvers in the portfolio: instance features $\rightarrow$ which solver performs better
\item Choose the best subset of solvers to use in the final portfolio
\end{itemize}
\end{frame}
\subsection{Online}
\begin{frame}
\frametitle{Methods}
\begin{itemize}
\item Predict whether the feature computation > 90 CPU seconds
\begin{itemize}
\item If the cost is too expensive, run the backup solver
\end{itemize}
\item Run the pre-solvers until predetermined cutoff time
\item For every pair, use DF to predict which one perform better
\item Choose the solver with highest votes
\begin{itemize}
\item In case it fails, use the second highest or back-up
\end{itemize}
\end{itemize}
\end{frame}
\section{Features}
\begin{frame}
\begin{itemize}
\item Problem size features
\item Variable-Clause graph features
\item Variable graph geatures
\item Clause graph features
\item Balance features
\item Proximity to Horn Formula
\item DPLL Probing Features
\item Local search probing features
\end{itemize}
\end{frame}
\section{Resources}
\frametitle{Resources}
\begin{frame}
\begin{itemize}
\item SATZilla: http://www.cs.ubc.ca/labs/beta/Projects/SATzilla/
\item SATzilla: Portfolio-based Algorithm Selection for SAT, Lin Xu and al., Journal of Artificial Intelligence Research 32 (2008) 565-606
\item Features: http://www.cs.ubc.ca/labs/beta/Projects/SATzilla/Report\_SAT\_features.pdf
\end{itemize}
\end{frame}
\end{document}
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment