\section{Chapitre 6: Stratégies de recherche}
\label{sec:ch6}

Robustesse d'un solveur: capacité à résoudre une large variété de problèmes

\subsection{Heuristiques de choix de variables}
\label{sec:heuristiquevariables}

Instancier les variables qui ont le plus d'impact en premier

Types d'heuristiques

\begin{itemize}
\item Ordre statique: on fixe l'ordre d'instantiation manuellement
\item Plus petit domaine: plus grande probabilité d'avoir la bonne valeur
\item Variable la plus contrainte: plus grand degré, a le plus d'impact sur la solution
\item Choix structurels: obtenir un problème plus simple à résoudre
\item Combinaisons des heuristiques précédents
\end{itemize}

Techniques additionnelles

\begin{itemize}
\item Stochastique: Utilise un générateur de nombres pseudo-aléatoires pour sélectionner les branchements sur les variables
\item Apprentissage: Ces heuristiques s'adaptent au problème avec une forme d'apprentissage qui met du poids sur les variables. Plongées dans l'arbre de recherche
\end{itemize}

\subsection{Heuristiques de choix de valeurs}
\label{sec:choixvaleurs}

\begin{itemize}
\item Le choix dépend souvent d'une connaissance du problème. On peut trier les valeurs du premier choix au dernier choix.
\item Déviation: solveur branche sur une valeur qui n'est pas le premier choix
\end{itemize}

\subsection{Fouille LDS}
\label{sec:fouillelds}

\begin{algorithm}[H]
  \DontPrintSemicolon
  \Deb{
    $Candidats \leftarrow \lbrace X_i \mid |dom(X_i)|  >1 \rbrace$ \;
    \Si{$Candidats = \emptyset$}{
      \Si{$dom(X_1),\ldots,dom(X_n)$ sat. contraintes}{
        \Retour{$dom(X_1),\ldots,dom(X_n)$}
      }
      \Sinon{
        \Retour{$\emptyset$}
      }
    }
    Choisir une variable $X_i \in Candidats$ \;
    \Si{$nbDeviations < |Candidats|$}{
      $Solution \leftarrow LDS(dom(X_1),\ldots,dom(X_{i-1}),\lbrace v_1 \rbrace, \ldots, dom(X_n)4,nbDeviations)$ \;
      \Si{$Solution \neq \emptyset$}{\Retour{$Solution$}}
    }
    \Si{$nbDeviations>0$}{
      $Solution \leftarrow LDS(dom(X_1),\ldots,dom(X_{i-1}),\lbrace v_2 \rbrace, \ldots, dom(X_n),nbDeviations)$ \;
      \Si{$Solution \neq \emptyset$}{\Retour{$Solution$}}
    }
    \Retour{$\emptyset$} \;
  }
  \caption{LDS($dom(X_1),\ldots,dom(X_n)$,nbDeviations)}
\end{algorithm}

\subsection{Redémarrage}
\label{sec:redemarrage}

\begin{itemize}
\item Heuristique stochastique: après un certain temps ou un certain nombre de retours arrières, on redémarre la recherche
\item Possibilité de visiter deux fois le même noeud: risque à prendre, inefficace, mais acceptable
\item Si on ne fait pas attention: possibilité de ne jamais visiter une branche de l'arbre, inacceptable
\end{itemize}

Stratégies de redémarrage:

Garantissent que la totalité de l'arbre est visité
\begin{itemize}
\item Géométrique: $1, r, r^2, r^3, ... | r>1$
\item Luby: $1,1,2,1,1,2,4,1,1,2,1,1,2,4,8, \ldots$ nombre de retours arrières est à un facteur logarithmique de la séquence optimale
\end{itemize}

\subsection{Nogoods}
\label{sec:nogoods}

\begin{itemize}
\item Cette stratégie réduit la possibilité de revisiter des noeuds
\item Contrainte ajoutée au modèle, prévient un second retour arrière pour les mêmes raisons
\item Un noeud est identifié par un ensemble de contraintes de branchement $p(n)= \lbrace b1, \ldots, b_j\rbrace$
\item Soit $n$ le noeud où le retour arrière est déclenché sans avoir visité ses descendants. Au moins une contrainte a été violée.
  \begin{align}
    J(n) = \lbrace b_i \in p(n) \mid portée(bi) \cap portée(C) \neq \emptyset \rbrace
  \end{align}
\item Si un retour arrière se produit sur chacun des enfants $c_1, \ldots, c_k$ de $n$
  \begin{align}
    J(n) = p(n) \bigcup_{i=1}^k J(c_i)
  \end{align}
\item Favoriser l'arité du nogood la plus petite
\item Gestion: Effacer ...
  \begin{itemize}
  \item les plus vieux, 
  \item les moins appelés, 
  \item ceux avec arité la plus grande
  \end{itemize}
\end{itemize}

Les solveurs SAT utilisent des heuristiques d'apprentissage, le redémarrage et des nogoods



%%% Local Variables:
%%% mode: latex
%%% TeX-master: "notes_de_cours"
%%% End: