Quels sont les principes clés du SAT en informatique ?

1. Représenter les problèmes sous forme de formules booléennes :

* Encodage : L'idée principale de l'utilisation des solveurs SAT est d'encoder un problème donné (par exemple, planification, conception de circuits, planification) en une formule booléenne sous forme normale conjonctive (CNF). Cela implique d'identifier les variables de décision du problème et de représenter les contraintes sur ces variables sous forme de clauses logiques. La beauté réside dans le fait qu’une grande variété de problèmes peuvent être exprimés dans ce format.

* Forme Conjonctive Normale (CNF) : Presque tous les solveurs SAT fonctionnent sur des formules en CNF. CNF est une formule logique qui est une conjonction (AND) de clauses, où chaque clause est une disjonction (OR) de littéraux. Un littéral est soit une variable, soit sa négation. Par exemple :`(x OR NOT y OR z) AND (NOT x OR y)`. Être au CNF rend le processus de recherche plus structuré et plus efficace.

2. Algorithme Davis-Putnam-Logemann-Loveland (DPLL) :

* Approche basée sur la recherche : DPLL est l'algorithme fondamental pour résoudre les problèmes SAT. Il s'agit d'un algorithme de recherche complet qui explore systématiquement l'espace des affectations de variables possibles.

* Décision : L'algorithme choisit une variable qui n'est actuellement pas attribuée et lui attribue « VRAI » ou « FAUX ». Ce choix crée deux branches dans l'arbre de recherche.

* Propagation des unités : Après avoir pris une décision, DPLL effectue une propagation unitaire. Une clause unitaire est une clause qui contient un seul littéral non attribué. Si une clause unitaire existe (par exemple, `x`), l'algorithme *doit* attribuer la variable `x` à la valeur qui rend la clause vraie (dans ce cas, `x =TRUE`). La propagation des unités peut se produire en cascade, conduisant à d'autres affectations de variables. Ceci est crucial pour simplifier le problème et éviter des recherches inutiles.

* Élimination littérale pure : Un littéral pur est un littéral qui apparaît dans une seule polarité (positive ou négative) dans toute la formule. Si un littéral pur existe, on peut lui attribuer une valeur pour que toutes les clauses le contenant soient vraies. Cela simplifie la formule sans affecter la satisfiabilité.

* Retour en arrière : Si une branche de la recherche conduit à un conflit (c'est-à-dire qu'une clause devient fausse), l'algorithme *fait marche arrière*. Cela signifie annuler la dernière décision et essayer la mission opposée. L'ensemble du processus se poursuit jusqu'à ce qu'une affectation satisfaisante soit trouvée (la formule est SAT) ou que toutes les affectations possibles aient été épuisées (la formule est UNSAT).

3. Apprentissage de clauses basé sur les conflits (CDCL) :

* Apprendre des conflits : Les solveurs SAT modernes sont basés sur CDCL, une extension de DPLL. L'innovation clé est que lorsqu'un conflit est rencontré, le solutionneur analyse les raisons du conflit et apprend une nouvelle clause (une clause de conflit) qui empêche que le même conflit ne se reproduise à l'avenir.

* Analyse des conflits : Le processus d'analyse des conflits utilise le graphique d'implication (un graphique représentant les dépendances entre les affectations de variables) pour déterminer un sous-ensemble des décisions qui ont conduit au conflit.

* Apprentissage des clauses : La clause de conflit est ajoutée à la formule, généralement en utilisant le schéma du « premier point d'implication unique (UIP) ». La clause résultante est une conséquence logique de la formule originale, donc son ajout ne change pas la satisfiabilité.

* Retour en arrière non chronologique (backjumping) : Les solveurs CDCL peuvent revenir en arrière de manière non chronologique. Au lieu de simplement annuler la dernière décision, ils peuvent revenir à un niveau de décision antérieur qui était responsable du conflit. Cela permet au solveur d’explorer l’espace de recherche plus efficacement.

* Suppression de clause : Pour éviter que la formule ne devienne trop volumineuse, les solveurs suppriment périodiquement certaines des clauses apprises. Les heuristiques sont utilisées pour décider quelles clauses supprimer, en équilibrant la nécessité de mémoriser des informations utiles avec la nécessité de garder la formule gérable.

4. Heuristiques de classement des variables (heuristiques de branchement) :

* Impact sur l'efficacité : L'ordre dans lequel les variables sont sélectionnées pour la décision (branchement) a un impact considérable sur les performances des solveurs SAT. De bonnes heuristiques peuvent réduire considérablement la taille de l’arbre de recherche.

* VSIDS (somme décroissante indépendante de l'état variable) : Une heuristique populaire est VSIDS. Il maintient un score pour chaque variable, qui est incrémenté chaque fois que la variable est impliquée dans un conflit. Les scores diminuent périodiquement, donnant la préférence aux variables récemment impliquées dans des conflits. Cette heuristique concentre la recherche sur les parties « actives » de la formule.

* Autres heuristiques : D'autres heuristiques prennent en compte la fréquence des variables dans les clauses, le nombre de clauses non résolues contenant une variable, ou utilisent des techniques d'apprentissage automatique pour apprendre des stratégies de branchement.

5. Heuristique de classement des clauses :

* Propagation des unités directrices : L'ordre dans lequel les clauses sont prises en compte pour la propagation des unités peut également affecter les performances.

* Littéraux regardés : La plupart des solveurs utilisent une technique appelée littéraux surveillés. Pour chaque clause, deux littéraux sont choisis comme « surveillés ». La propagation unitaire ne doit être déclenchée que lorsque l'un des littéraux surveillés devient faux. Cela réduit considérablement le nombre de clauses à examiner.

6. Stratégies de redémarrage :

* Échapper aux minima locaux : Les solveurs CDCL peuvent parfois rester bloqués dans une partie de l’espace de recherche difficile à explorer. Le redémarrage périodique du solveur peut aider à échapper à ces minimums locaux.

* Redémarrage à base de glucose : Les solveurs modernes utilisent souvent des stratégies de redémarrage basées sur la qualité des clauses apprises. Par exemple, la stratégie de redémarrage du glucose redémarre le solveur plus fréquemment lorsqu'il apprend de nombreuses clauses de mauvaise qualité.

7. Prétraitement et traitement entrant :

* Simplification de la formule : Les techniques de prétraitement sont appliquées à la formule *avant* le début du processus de recherche principal. Ces techniques visent à simplifier la formule en supprimant les clauses redondantes, en remplaçant les variables et en effectuant d'autres transformations logiques.

* Traitement en cours : Les techniques de traitement sont appliquées *pendant* le processus de recherche. Ces techniques peuvent simplifier dynamiquement la formule en fonction de l'état actuel de la recherche.

* Exemples : Le prétraitement et le traitement incluent la subsomption (suppression des clauses logiquement impliquées par d'autres clauses), la résolution (ajout de nouvelles clauses à la formule en fonction des clauses existantes) et l'élimination de variables (remplacement d'une variable par sa définition).

8. Résolution SAT parallèle :

* Diviser pour régner : Les solveurs parallèles SAT exploitent le parallélisme inhérent au processus de recherche. Ils peuvent diviser l’espace de recherche en plusieurs parties et les explorer simultanément.

* Approches de portefeuille : Une autre approche consiste à exécuter plusieurs solveurs SAT différents (avec des paramètres différents) en parallèle, et à espérer que l'un d'entre eux trouvera rapidement une solution.

* Partage de clause : Les solveurs parallèles peuvent partager les clauses apprises entre différents processus pour améliorer l'efficacité globale de la recherche.

9. Résolution théorique (SMT) :

* Au-delà de la logique booléenne : Les solveurs SAT sont souvent utilisés comme composant central des solveurs Satisfiability Modulo Theories (SMT). Les solveurs SMT peuvent raisonner sur des formules contenant des variables et des contraintes issues d'autres théories, telles que l'arithmétique, les chaînes ou les tableaux.

* Combiner SAT avec des solveurs spécifiques à la théorie : Les solveurs SMT utilisent une combinaison de techniques de résolution SAT et de solveurs spécifiques à la théorie pour déterminer la satisfiabilité des formules.

En résumé, les principes clés de la résolution SAT tournent autour de l'exploration efficace de l'espace des affectations de variables possibles, de l'apprentissage des conflits pour éviter de répéter les erreurs et de la simplification de la formule pour réduire l'espace de recherche. Les solveurs SAT modernes sont des outils très sophistiqués capables de résoudre des problèmes comportant des millions de variables et de clauses.