Commit 6a60035e authored by Remi Oudin's avatar Remi Oudin
Browse files

Bibliography

parent e3fce238
......@@ -89,15 +89,18 @@
}
@misc{SATzilla,
title = "SATzilla~: Portfolio-based algorithm selection for SAT",
title = "SATzilla~: Portfolio-based algorithm selection for {SAT}",
url = "http://www.cs.ubc.ca/labs/beta/Projects/SATzilla/",
howpublished = "\url{http://www.cs.ubc.ca/labs/beta/Projects/SATzilla/}",
year= 2012,
}
@article{lammgraph,
title={Graph Neural Networks and Boolean Satisfiability},
@misc{lammgraph,
title={Graph {N}eural {N}etworks and {B}oolean {S}atisfiability},
author={Lamm, Matthew and B{\"u}nz, Benedikt},
year={2015}
year={2015},
url={https://cs224d.stanford.edu/reports/BunzBenedikt.pdf},
howpublished={\url{https://cs224d.stanford.edu/reports/BunzBenedikt.pdf}}
}
@article{xu2008,
......@@ -130,9 +133,3 @@
publisher="IEEE Press",
year={2009}
}
@article{GNNandSat,
author = {Benedikt Bünz and
Matthew Lamm},
title = {Graph Neural Network and Boolean Satisfiability},
}
......@@ -2,6 +2,8 @@
\usepackage{amsmath, amsfonts, amssymb, complexity, hyperref}
\usepackage{url}
\usepackage{graphics}
\usepackage[french]{babel}
......@@ -45,20 +47,20 @@ solving ont lieu régulièrement.
Les techniques d'apprentissage classiquement utilisées ne sont pas des
techniques d'apprentissage profond, utilisant des réseau de neurones, mais
plutôt des techniques telles que la validation croisée ou le maximum de
vraisemblance. Pourtant, le réseau de neurones est un outil qui peut se
révéler extrêmement efficace pour certains types de problèmes d'apprentissage,
et il s'agit d'un domaine en pleine expansion.
vraisemblance. Pourtant, le réseau de neurones est un outil qui peut se révéler
extrêmement efficace pour certains types de problèmes d'apprentissage, et il
s'agit d'un domaine en pleine expansion.
Notre objectif de départ a été d'essayer de combiner \SAT~solving et
apprentissage profond. Tout d'abord, nous avons cherché des articles
qui mêleraient déjà les deux, puis nous sommes divisés en plusieurs
groupes de travail. Rémi, Kawisorn, Xavier, et Emilie ont cherché à
comprendre plus précisément comment fonctionnaient les \SAT~solvers
les plus performants actuellement ; Paul et Léo ont fait des
recherches supplémentaires sur les réseaux de neurones en étudiant
plus particulièrement un type de réseau de neurones appliqué aux
graphes ; Johan et Jules ont travaillé sur un article utilisant des
réseaux de neurones sur des images représentant des formules \SAT.
apprentissage profond (aussi appelé Deep Learning dans la suite du document).
Tout d'abord, nous avons cherché des articles qui mêleraient déjà les deux,
puis nous sommes divisés en plusieurs groupes de travail. Rémi, Kawisorn,
Xavier, et Emilie ont cherché à comprendre plus précisément comment
fonctionnaient les \SAT~solvers les plus performants actuellement; Paul et Léo
ont fait des recherches supplémentaires sur les réseaux de neurones en étudiant
plus particulièrement un type de réseau de neurones appliqué aux graphes; Johan
et Jules ont travaillé sur un article utilisant des réseaux de neurones sur des
images représentant des formules \SAT.
\section{État de l'art des \SAT~Solvers}
......@@ -76,11 +78,11 @@ de manière efficace les formules, ou bien de les regrouper selon divers
facteurs.
Suite à quelques recherches, nous avons trouvé plusieurs articles du même
groupe d'auteur-e-s~: Carlos Ans{\'o}tegui, Maria Luisa Bonet, Jes\'us
Gir\'aldez-Cru, Jordi Levy \cite{Ansotegui2009, Ansotegui2012, Ansotegui2013,
Ansotegui2016}. Nous avons donc convergé vers la même problématique~: Comment
classifier efficacement des formules, et comment cela est-il utilisé en
pratique dans les \SAT~solvers actuels~?
groupe d'auteur-e-s~: Carlos Ans{\'o}tegui, Maria Luisa Bonet, Jes{\'u}s
Gir{\'a}ldez-Cru, et Jordi Levy \cite{Ansotegui2009, Ansotegui2012,
Ansotegui2013, Ansotegui2016}. Nous avons donc convergé vers la même
problématique~: Comment classifier efficacement des formules, et comment cela
est-il utilisé en pratique dans les \SAT~solvers actuels~?
Les papiers que nous avons étudié utilisaient le \SAT~solver
\emph{SATzilla}\cite{SATzilla}, Kawisorn a donc étudié son fonctionnement.
......@@ -90,37 +92,39 @@ résultats, et la comparaison avec les résultats actuels.
\subsection{Fonctionnement de \emph{SATzilla}, vainqueur du SAT Challenge 2012}
SATzilla est l'un des premiers algorithmes qui utilisent l'évaluation de
\emph{SATzilla} est l'un des premiers algorithmes qui utilise 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 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.\\
instances du problème \SAT. \emph{SATzilla} a gagné plusieurs concours de
\SAT~solving et surpasse tous les \SAT~solveurs non \emph{portfolio}. L'idée de
base de l'algorithme est, étant données des instances du problème, de choisir
le meilleur solveur pour les résoudre.\\
L'algorithme de SATzilla se consiste en deux parties : offline et online.\\
L'algorithme de \emph{SATzilla} est constitué de deux parties : offline et
online.\\
La partie offline comprend de la construction de classifier qui déterminera le
meilleur solveur pour une instance de problème. On construit l'ensemble des
La partie offline comprend la construction du classifieur qui déterminera le
meilleur solveur pour une instance du 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,
précedents) et choisit les solveurs candidats (Minisat, Rsat, Eureka,
Vallst,etc). On identifie les features des instances (pour
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
meilleur solveurs comme \emph{presolver} et \emph{backup solver}. Avec
le résultat d'entraînement, on pourrait contruire un classifier
\emph{decision forest} qui détermine si le temps de calcul pour les
features est coûteux et un classifier \emph{decision forest} qui étant
donnés deux solveurs et un instance de SAT, détermine quel est le plus
donné 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 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
Après avoir construit les classifiers, la partie online utilise le modèle
d'apprentissage 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 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
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 lui donne un point. On utilisera le solveur qui a le plus de
points.\\
......@@ -281,7 +285,7 @@ algorithmes de \SAT~solving plus efficaces.
Nous nous sommes également penché vers des méthodes de résolutions des
formules \SAT entièrement effectuées via des réseaux de
neurone. L'article \cite{GNNandSat} propose ainsi une méthode de
neurone. L'article \cite{lammgraph} propose ainsi une méthode de
résolution relativement naturelle en deux étapes :
\begin{enumerate}
......
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