Commit c58b13b5 authored by Xavier Poulot-cazajous's avatar Xavier Poulot-cazajous
Browse files

Update report.tex

parent c3557dda
......@@ -87,7 +87,7 @@ résultats, et la comparaison avec les résultats actuels.
SATzilla est l'un des premiers algorithmes qui utilisent l'évaluation de
solveurs pour résoudre le problème \SAT (portfolio-based). La motivation vient
de l'observation que les performances des \Sat~solvers diffèrent selon les instances
de l'observation que les performances des \SAT~solvers diffèrent selon les instances
de problème. SATzilla a gagné plusieurs concours de SAT et surpasse tous les
non-porfolio solveurs. L'idée de base de l'algorithme est étant données les
instances de problème, choisir le meilleur solveur pour résoudre.\\
......@@ -95,11 +95,11 @@ instances de problème, choisir le meilleur solveur pour résoudre.\\
L'algorithme de SATzilla se consiste en deux parties : offline et online.\\
La partie offline comprend de la construction de classifier qui déterminera le
meilleur solveur pour un instance de problème. On construit l'ensemble des
meilleur solveur pour une instance de problème. On construit l'ensemble des
instances (on prend les instances qui apparaissent dans les concours
précedents) et choisit les candidats solveurs (Minisat, Rsat, Eureka,
Vallst,etc). On identifie les features des instances (pour
SATzilla2012, il y a 138 caracteristiques). Pour chaque instance dans des
SATzilla2012, il y a 138 caractéristiques). Pour chaque instance dans des
données d'entraînement, on détermine le temps pour calculer des
features et le temps d'exécution pour chaque solveur. On identifie deux
meilleur solveurs comme \emph{presolveur} et \emph{backup solveur}. Avec
......@@ -110,13 +110,13 @@ donnés deux solveurs et un instance de SAT, détermine quel est le plus
performant parmi les deux.\\
Après avoir construit les classifiers, la partie online utilise le learning
modèle pour résoudre le SAT problème. Etant donnée l'instance de problème, on
modèle pour résoudre le problème \SAT. Etant donnée l'instance de problème, on
prédit si le temps de calcul pour les features est coûteux. Dans le
cas coûteux, on utilise le \emph{back-up solveur} pour résoudre notre
problème. Sinon, on execute \emph{pre solveur} pour une certaine limite de
problème. Sinon, on exécute \emph{presolveur} pour une certaine limite de
temps. Si le \emph{presolveur} ne termine pas, on calcule des features
de l'instance et pour chaque couple de solveurs, on détermine lequel est le
meilleur et on le donne un point. On utilisera le meilleur solveur a le plus de
meilleur et on lui donne un point. On utilisera le solveur qui a le plus de
points.\\
SATzilla montre que la portfolio-based méthode est la méthode très efficace,
......@@ -268,26 +268,7 @@ algorithmes de \SAT~solving plus efficaces.
Finalement, la dernière amélioration qui peut être apportée, et qui est
suggérée par les auteurs est de trouver une mesure de complexité de la
formule plus pertinente que le rapport clause/littéraux. Celle-ci est
beaucoup trop simpliste pour être représentative de la difficulté d'une
formule.
\begin{figure}[t]
\centering
\begin{tabular}{c||c|c|c|c|c}
runtime & $\text{Structure}_{V Cr}$ & $\text{Structure}_{V
r}$&$\text{Structure}_{V C}$&$\text{Structure}_{V}$ & SATzilla \\
\hline
minimum & 0.26 & 0.26 & 0.26 & 0.26 & 0.26 \\
median & 272.62 & 268.10 & 262.02 & 310.27 & 261.84 \\
average & 874.59 & 863.32 & 876.84 & 881.15 & 831.61 \\
stdev & 1199.59 & 1197.70 & 1200.11 & 1207.83 & 1143.55\\
maximum & 4913.23 & 4913.23 & 4913.23 & 4913.23 & 4745.21\\
\hline
\#solved & 285 & 281 & 285 & 281 & 288
\end{tabular}
\caption{Runtime over 300 industrial instances\cite{Ansotegui2016}}
\end{figure}
formule plus pertinente que le rapport clause/littéraux.
\section{Réseaux de neurones et graphes}
......
Markdown is supported
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