Commit 0af9b714 authored by JulesKzl's avatar JulesKzl
Browse files

1er Merge Jules et Jo

parents fa85746d bc8d5352
No preview for this file type
\documentclass[a4paper, 11pt]{article}
\documentclass[titlepage, a4paper, 11pt]{article}
\usepackage{amsmath, amsfonts, amssymb, complexity, hyperref}
......@@ -27,6 +27,8 @@ Kozolinsky},\\\textsc{Poulot-Cazajous, Colisson, Jeanmaire, Oudin}}
\tableofcontents
\newpage
\section*{Introduction}
Le problème \SAT~est un problème fondamental en informatique, car un grand
......@@ -282,11 +284,11 @@ algorithmes de \SAT~solving plus efficaces.
\begin{enumerate}
\item On commence par traduire la formule SAT sous forme de graphe
\item On lance un réseau de neurone sur ce graphe
\item On lance un réseau de neurones sur ce graphe
\end{enumerate}
Cependant, nous nous sommes aperçus que faire un réseau de neurone
travaillant sur des graphe (et exploitant véritablement la structure
Cependant, nous nous sommes aperçus que faire un réseau de neurones
travaillant sur des graphes (et exploitant véritablement la structure
précise du graphe) n'est pas trivial, et nous nous sommes inspirés du
papier \cite{graphNeuralNetwork} afin de comprendre comment on pouvait
construire de tels réseaux.
......@@ -351,11 +353,11 @@ neurone \og{}informatique\fg{} possède des entrées et une sortie, comme illust
\end{figure}
À chaque entrée $i$, on associe un poids synaptique $w_i$. Ainsi, pour calculer
la sortie d'un réseau de neurone, on procède de la manière suivante :
la sortie d'un réseau de neurones, on procède de la manière suivante :
\begin{enumerate}
\item On commence par multiplier toutes les entrées $x_i$ par leurs poids
associé respectifs $w_i$
\item on somme le tout
\item On somme le tout
\item On ajoute un paramètre $b$ (utile pour \og{}recentrer\fg{} la distribution)
\item Il ne reste plus qu'à appliquer une fonction dite d'activation $f$
non linéaire, en principe dérivable. La sigmoïde est souvent utilisée,
......@@ -400,7 +402,7 @@ la sortie d'un réseau de neurone, on procède de la manière suivante :
\label{fig:sigm}
\end{figure}
Ensuite, pour faire un réseau de neurone, il suffit de mettre des neurones
Ensuite, pour faire un réseau de neurones, il suffit de mettre des neurones
bouts à bouts par couche, les sorties des unes devenant les entrées des autres,
comme illustré \autoref{fig:reseau} :
......@@ -509,6 +511,21 @@ Maintenant que l'on sait faire apprendre nos réseaux de neurones, il reste
maintenant à trouver une structure à notre réseau. Pour l'apprentissage sur les
graphes, ce n'est pas évident de prime abord.
\subsection{Traduction des formules \SAT}
Les formules propositionnelles considérées dans \SAT\ sont représentées sous
forme normale conjonctive (conjonction de clauses de taille fixée).
Deux façons d'encoder ces formules dans des graphes sont présentées:
\begin{itemize}
\item les graphes de facteurs clause-variable (figure) dans lesquels clauses
et variables sont deux types de n\oe uds distincts: les graphes ainsi formés
sont bipartis, et l'étiquette des arêtes représente la négation ou non de
la variable dans la clause;
\item les graphes variable-variable, dans lesquels les n\oe uds correspondent
aux variables de la formule et les arêtes relient les variables apparaissant
au moins une fois dans la même clause.
\end{itemize}
\subsection{Résultats sur des réseaux de neurones}
......@@ -519,16 +536,20 @@ graphes, ce n'est pas évident de prime abord.
Après l'état de l'art des \SAT~Solver réalisé par le premier groupe, Johan et Jules étaient quant à eux chargés de dresser celui des \SAT~Solver utilisant le \textit{deep-learning}. \\
Lors des compétitions de \SAT~Solving, peu de programmes utilisaient de l'apprentissage profond au sein de la résolution. Néanmoins il existe pourtant une catégorie de programmes, nommés \textit{portfolios}, utilisant l'apprentissage profond en amont du \SAT~Solving.
\subsection{Etude du papier de recherche :\textit{ Deep Learning for Algorithm Portfolios} \cite{loreggia2015deep}}
Il s'agit d'un papier publié en 2016 par Andrea Loreggia, Yuri Malitsky, Horst Samulowitz et Vijay Saraswat, chercheurs à IBM Research.
\subsubsection{L'intérêt des portfolios}
Dans la plupart des cas, il semble vain de trouver un algorithme qui sera efficace sur un très large spectre de problèmes. D'où l'intérêt de combiner plusieurs solver en un seul, le portfolio. Sur une instance donnée, le portfolio donnera le meilleur \SAT~Solver pour cette instance.
On souhaite ainsi apprendre à notre algorithme quel \SAT~Solver solver utiliser et cela grâce à un réseau de neurones.
\subsubsection{Représentation des données}
\paragraph{Format des données\\}
On représente les problèmes \SAT sous forme \textit{DIMACS}. Les formules \SAT sont représentées sous forme \CNF. Pour $(x_1 \vee \neg x_3)\wedge(x_2 \vee x3 \vee \neg x_1)$, on écrit :
\begin{verbatim}
......@@ -540,21 +561,20 @@ Il s'agit d'un papier publié en 2016 par Andrea Loreggia, Yuri Malitsky, Horst
Pour des problèmes de contraintes non descriptibles sous forme \CNF, on utilise un autre format, le format \textit{XCSP} :
\begin{verbatim}
<domains nbDomains="1">
<domain name="d0" nbValues="2">1..2</domain>
</domains>
<variables nbVariables="2">
<variable name="A1" domain="d0"/>
<variable name="A2" domain="d0"/>
</variables>
<constraint name="c0" arity="2" scope="A1 A2"
reference="global:alldifferent"/
\end{verbatim}
<domain name="d0" nbValues="2">1..2</domain>
</domains>
<variables nbVariables="2">
<variable name="A1" domain="d0"/>
<variable name="A2" domain="d0"/>
</variables>
<constraint name="c0" arity="2" scope="A1 A2" reference="global:alldifferent"/>
\end{verbatim}
\paragraph{Transformation des données\\}
Une méthode applicable sur toute sorte de syntaxes de définition est souhaitable pour notre algorithme. Les données texte, de format DIMACS ou XCSP, sont donc converties en image en suivant un processus simple. Premièrement chaque caractère texte et remplacer par son code ASCII, ce qui représente donc un pixel en niveau de gris. Enfin le vecteur de ces pixel est formaté en un carré, puis ajusté à la taille choisie (pour le réseau neuronal).
Une méthode applicable sur toute sorte de syntaxes de définition est souhaitable pour notre algorithme. Les données texte, de format DIMACS ou XCSP, sont donc converties en image en suivant un processus simple. Premièrement chaque caractère texte et remplacer par son code ASCII, ce qui représente donc un pixel en niveau de gris. Enfin le vecteur de ces pixel est formaté en un carré, puis ajusté à la taille choisie (pour le réseau neuronal).
\begin{figure}[h]
\begin{figure}[H]
\begin{center}
\includegraphics[scale=0.5]{images/image_SAT.png}
\hspace{5mm}
......@@ -563,11 +583,13 @@ Une méthode applicable sur toute sorte de syntaxes de définition est souhaitab
\caption{Images créées à partir d'une formule SAT et d'une formule CSP}
\end{figure}
\subsubsection{Utilisation d'un réseau neuronal}
Un réseau neuronal artificiel est un ensemble d'algorithmes inspiré du fonctionnement des neurones biologiques. Un type particulier de réseau de neurones sont les réseaux de neurones convolutifs où le motif de connexion entre les neurones est ici plus particulièrement inspiré par le cortex visuel des animaux.
Les réseaux neuronaux convolutifs sont très largement utilisés pour la classification d'image.\\
\begin{figure}[h]
\begin{figure}[H]
\begin{center}
\includegraphics[scale=0.5]{images/reseau_de_neurone.png}
\end{center}
......@@ -579,7 +601,9 @@ deux couches entièrement connectées avec une couche de drop-out au milieu. \\
Malheureusement la tâche de classification, i.e. prédire le meilleur \SAT~Solver pour une instance donnée) obtient de mauvais résultats. Les auteurs du papier ont donc choisi un réseau effectuant une simple régression qui prédit simplement quel \SAT~Solver peut résoudre l'instance donnée ou non.
\subsubsection{Résultats et perspectives}
\subsubsection{Résultats}
\paragraph{Conditions des expériences : }environ $1000$ instances pour entrainement limité à $100$ \textit{epochs}. (Un \textit{epoch} consiste à un cycle d'entrainement sur l'ensemble des données d'entrainements.)
\begin{figure}[h]
......@@ -607,21 +631,21 @@ deux couches entièrement connectées avec une couche de drop-out au milieu. \\
\end{itemize}
On notera finalement que les temps de calcul ne sont pas donnés . Ce serait pourtant un critère important pour comparer plus précisément CNN et CSHC.
\subsubsection{Conclusion et perspectives}
\subsection{Conclusion et perspectives}
Bien que l'objectif initial n'a pas été atteint, les résultats sont bons et laissent à espérer des percés dans le domaine des \SAT~Solver grâce au deep-learning, qui est encore un domaine de recherche jeune.
Bien que l'objectif initial n'a pas été atteint, les résultats sont bons et laissent à espérer des percés dans le domaine des \SAT~Solver grâce au deep-learning, qui est encore un domaine de recherche jeune.
Une question légitime (merci Léo) est de se demander comment peuvent varier les résultats de cet algorithme en fonction de l'encodage initial du problème. Selon l'article, l'encodage importe peu mais on pourrait facilement imaginer des encodages absurde obfusquant les données importantes du problème et donc l'image sur laquelle travaille le réseau. (\textit{e.g} chaque caractère de notre fichier initial est séparé par un texte quelconque d'une centaine de caractère).\\
Une question légitime (merci Léo) est de se demander comment peuvent varier les résultats de cet algorithme en fonction de l'encodage initial du problème. Selon l'article, l'encodage importe peu mais on pourrait facilement imaginer des encodages absurde obfusquant les données importantes du problème et donc l'image sur laquelle travaille le réseau. (\textit{e.g} chaque caractère de notre fichier initial est séparé par un texte quelconque d'une centaine de caractère).\\
Quelques autres pistes à explorer :
Quelques autres pistes à explorer :
\begin{itemize}
\item Le redimensionnement de l'image est effectué de manière automatique. Il pourrait être intégré dans le processus de deep learning.
\item Utiliser les réseaux de neurones pour résoudre directement les problèmes combinatoires.
\item Utiliser les portfolios pour d'autres tâches comme l'Opinion mining (l'analyse des sentiments à partir de sources textuelles dématérialisées sur de grandes quantités de données (big data).
\end{itemize}
\bibliographystyle{plain}
\bibliography{report}
......
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