Problème SAT
Un article de Wikipédia, l'encyclopédie libre.
Vous avez de
Sommaire |
[modifier] Le problème SAT
Le problème SAT est un problème de décision d'une grande importance en théorie de la complexité.
Le problème SAT s'énonce de la manière suivante :
- Données : une formule logique F de m clauses sur n variables.
- Question : F est elle satisfiable ? – c'est-à-dire, existe-t-il une façon d'assigner les valeurs « vrai » ou « faux » aux variables afin de rendre la formule vraie ?
SAT est un problème NP-complet d'après le théorème de Cook.
On obtient de même un problème NP-complet si on se restreint au problème 3SAT : étant donné une formule logique de la forme (u1∨v1∨w1) ∧ ... ∧ (um∨vm∨wm), avec les ui, vi, wi choisis dans un ensemble de n variables et de leurs négations. Par exemple avec n=4; les variables sont {a,b,c,d} On recherche si l'expression (a1∨!b1∨c1) ∧ (!a1∨c1∨d1) a une solution. L'algorithme doit fonctionner sur toutes les formules à 4 variables de la forme (u1∨v1∨w1) ∧ ... ∧ (um∨vm∨wm) Comme il n'y a pas de méthode générique fonctionant quelque soit l'expression, il faut à chaque fois essayer les 2 puissance n (ici 2 puissance 4) jeux de solutions possibles pur a et b.
[modifier] Implémentation informatique
Le Centre de Recherche en Informatique de Lens à Lens (France) a développé une bibliothèque de solveurs SAT en Java nommée SAT4j. Le site de satex organise tout les ans une compétition entre les meilleurs SAT solver open source. Les résultats sont consultables en lignes, et les liens vers les auteurs sont disponibles.
Les algorithmes de résolution, fonctionent en traitant des cas particuliers, comme par exemple en détectant les symétries dans les formules, mais comme il existe toujours des cas casse pieds, la complexité, reste dans le cas général NP.
