Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Socsat Satisfaction et Optimisation de Contraintes Lakhdar SA? S CRIL - Université d ? Artois Lens Bureau C sais cril univ-artois fr http www cril univ-artois fr sais Plan n Introduction n SAT isfiabilité propositionnel n Problème SAT définitions de base

Satisfaction et Optimisation de Contraintes Lakhdar SA? S CRIL - Université d ? Artois Lens Bureau C sais cril univ-artois fr http www cril univ-artois fr sais Plan n Introduction n SAT isfiabilité propositionnel n Problème SAT définitions de base n Les classes polynomiales n Algorithmes de résolution n Résolution n Énumération Simplifications Heuristiques Traitement des échecs n Recherche locale GSAT Taboo ? n Méthodes hybrides n Instances de SAT n Problèmes structurés n problèmes aléatoires - phénomène de seuil n problèmes réels n Structures résolution n Extensions n Directions de recherche Plan suite n CSP Problème de satisfaction de Contraintes n représentation de problèmes par des contraintes n Les CSP définitions de base n Consistances partielles filtrages et propagations de contraintes n Techniques de résolution n Graphes de contraintes consistance et méthodes de décomposition n Extensions n Directions de recherche n Autres techniques n algorithmes génétiques n ATMS n Applications n Conclusion perspectives Références SAT Web n SATLIVE http www satlive org n SatEx http www satex org n SATLIB http www satlib org CSP n Constraints archives http www cs unh edu ccc archive n CSPLIB http www csplib org Conférences IJCAI AAAI CP SAT ICLP JNPC-JFPLC ? Livres articles de synthèse n Foundation of constraint satisfaction problems Edward Tsang n Jun Gu etal Algorithms for Satisfiability SAT Problem A Survey Introduction Motivation Intelligence artificielle représentation des connaissances raisonnements inférence classique inférence non monotone logique SAT PL CSP PLC CP Recherche opérationnelle réseaux de contraintes applications Problème SAT définitions de base Notations définitions n Une formule booléenne n n T sont des formules n une variable atome propositionnelle A A A ? est une formule n si n et n sont des formules alors nn n n n n n n n nn n n n sont des formules n Littéral une variable propositionnelle Ai littéral positif ou sa négation n Ai littéral négatif n Atomes n A A A ? An apparaissant dans n n Une formule booléenne peut être représenté par un arbre ou un DAG graphe orienté acyclique Notations définitions n Une interprétation complète I de n I Atomes n n T n Une interprétation partielle I de n I A n n T A n Atomes n n représentation d ? une interprétation n I peut être représentée par un ensemble de littéraux Ex I A T I A n n A n A n I peut être représentée par une formule booléenne Ex I A T I A n n A n n A Notations définitions n I n n I satisfait n n I n Ai n I Ai T n I n n n I n n n I n n n n n I n n et I nn n n n est satisfiable ssi n I tq I n n I est appelé modèle de n n n n n n n I tq I n n alors I nn n est conséquence logique de n n n n