Remerciez-le!

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

Satisfaction et Optimisation de Contraintes Lakhdar SAÏS CRIL - Université d’Ar

Satisfaction et Optimisation de Contraintes Lakhdar SAÏS CRIL - Université d’Artois, Lens Bureau : C307 Bureau : C307 sais@cril.univ-artois.fr sais@cril.univ-artois.fr http://www.cril.univ-artois.fr/~sais http://www.cril.univ-artois.fr/~sais Introduction SAT(isfiabilité) propositionnel Problème SAT : définitions de base Les classes polynomiales Algorithmes de résolution Résolution Énumération, Simplifications, Heuristiques,Traitement des échecs Recherche locale (GSAT, Taboo,…) Méthodes hybrides Instances de SAT Problèmes structurés problèmes aléatoires - phénomène de seuil problèmes réels Structures & résolution Extensions Directions de recherche Plan Plan (suite) CSP (Problème de satisfaction de Contraintes)  représentation de problèmes par des contraintes  Les CSP : définitions de base  Consistances partielles, filtrages et propagations de contraintes  Techniques de résolution  Graphes de contraintes, consistance et méthodes de décomposition  Extensions  Directions de recherche Autres techniques  algorithmes génétiques  ATMS Applications Conclusion & perspectives Références Web SAT : SATLIVE : http://www.satlive.org SatEx : http://www.satex.org SATLIB : http://www.satlib.org CSP : Constraints archives : http://www.cs.unh.edu/ccc/archive/ CSPLIB : http://www.csplib.org Conférences IJCAI, AAAI, CP, SAT, ICLP, JNPC-JFPLC,… Livres & articles de synthèse Foundation of constraint satisfaction problems, Edward Tsang Jun Gu etal. Algorithms for Satisfiability (SAT) Problem: A Survey Introduction & Motivation réseaux de contraintes représentation des connaissances inférence non monotone SAT raisonnements inférence classique applications Intelligence artificielle logique CSP PL CP Recherche opérationnelle PLC Problème SAT : définitions de base Problème SAT : définitions de base Notations & définitions Une formule booléenne :  , T sont des formules  une variable (atome) propositionnelle A1, A2, A3, … est une formule  si 1 et 2 sont des formules, alors 1, (1  2), (1 2), (12), (1 2 ) sont des formules  Littéral : une variable propositionnelle Ai (littéral positif) ou sa négation Ai (littéral négatif)  Atomes() : {A1, A2, A3, …An} apparaissant dans   Une formule booléenne peut être représenté par un arbre ou un DAG (graphe orienté acyclique) Notations & définitions Une interprétation complète I de  : I : Atomes() {, T } Une interprétation partielle I de  : I : A {, T}, A  Atomes() représentation d’une interprétation :,  I peut être représentée par un ensemble de littéraux : Ex: { I(A1) = T , I(A2) = }  {A1, A2}  I peut être représentée par une formule booléenne : Ex: { I(A1) = T , I(A2) = }  A1  A2 Notations & définitions I  (I satisfait )  I Ai  I(Ai) = T  I ¬  ¬I   I 1  2  I 1 et I 2  ...  est satisfiable ssi  I tq I  ( I est appelé modèle de ) 1 2   I tq I 1 alors I 2 (2 est conséquence logique de 1 )     I , I  ( est valide)  est valide  ¬ est unsatisfiable  =  =  =  =  =  =  =  =  =  =  =  =  = Équivalence et satisfiabilité 1 et 2 sont équivalente ssi,  I , I 1 ssi I 2 1 et 2 sont équi-satisfiable ssi I1 tq I1 1 ssi I2 tq I2 2 1 et 2 sont équivalente   1 et 2 sont équi-satisfiable Exemple : 1  2 et (1  ¬ A3)  (2  A3), avec A3  Atomes (1  2) sont equi-satisfiable mais pas équivalente  =  =  =  = Complexité Le problème de décider de la satisfiabilité d’une formule booléenne (SAT) est NP-complet [Cook : 71] Les problèmes les plus importants en logique (validité, déduction, équivalence, …) peuvent être réduit à SAT, et sont (co)NP-complet. (voir cours outils formels) Exemple (déduction logique): 1   1  ¬ est unsatisfiable  « Il n’existe pas » d’algorithme de complexité polynomiale! Question importante en théorie de la complexité.  = Transformation en NNF, CNF Transformation en NNF, CNF Polarité des sous-formules Polarité : le nombre de négations modulo 2 Occurrences positive/negative   apparaît positivement dans   si 1 apparaît positivement [négativement] dans  , alors 1 apparaît négativement [positivement] dans   si 1  2 ou 1  2 apparaît positivement [négativement] dans , alors 1 et 2 apparaissent positivement[négativement] dans   12 apparaît positivement [négativement] dans  , alors 1 apparaît négativement [positivement] dans  et 2 apparaît positivement [négativement] dans   1 2 apparaît dans , alors 1 et 2 apparaissent positivement et négativement dans  Forme Normal Négative (NNF)  est sous forme NNF ssi  est donnée avec uniquement les connecteurs logique  ,  et  toute formule peut être réduite sous forme NNF : 1) en remplaçant les  et  : 1  2  1  2 1  2  (1  2)  (1  2) 2) descendre les négations au niveau atomique : (1  2)  1  2 (1  2)  1  2 1  1 la réduction préserve l’équivalence, complexité linéaire. Forme Normal Conjonctive (CNF)  est sous forme CNF (clausale) ssi  est une conjonction de disjonctions de littéraux :  (  Aji) La disjonction de littéraux  Aji est appelé clause La forme CNF est plus facile à manipuler (par les algorithmes) :  liste de listes de littéraux Exemple :  = (a  b) (b  c)  (c  a)  (a  b  c) i=1 L ji=1 Ki ji=1 Ki clause Transformation en CNF Toute formule  peut être réduite à CNF() : 1. réduire en NNF; 2. Appliquer récursivement les lois de DeMorgan : (1  2)  3  (1  3)  (2  3) Atomes(CNF()) = Atomes() CNF() est équivalente à  Si 1 est équivalente à 2, alors CNF(1) = CNF(2) modulo un ordre Complexité exponentielle dans le pire des cas  Rarement utilisé en pratique. Transformation en CNF : utilisation de variables supplémentaire Toute formule  peut être réduite à CNF() : 1. réduire en NNF; 2. Appliquer récursivement les règles :   [Ai  Aj|B]  CNF(B (Ai  Aj) )   [Ai  Aj|B]  CNF(B (Ai  Aj) ) Ai et Aj sont des littéraux, et B une variable supplémentaire Atomes(CNF())  Atomes() CNF() est équi-satisfiable à  Si 1 est équivalente à 2, alors CNF(1) = CNF(2) modulo un ordre Complexité linéaire dans le pire des cas  Souvent utilisé en pratique. Transformation en CNF : version améliorée Comme dans le cas précédent, en appliquant (2.) les règles ci-dessous :   [Ai  Aj|B]  CNF(B  (Ai  Aj) ) , si Ai  Aj est positive   [Ai  Aj|B]  CNF((Ai  Aj)  B ) , si Ai  Aj est négative   [Ai  Aj|B]  CNF(B  (Ai  Aj) ), si Ai  Aj est positive   [Ai  Aj|B]  CNF( (Ai  Aj)  B ), si Ai  Aj est négative  Réduction de la taille de la formule obtenue. Représentation arborescente d ’une formule booléenne [( ((a  b))  (c  d) )((e1  e2  e3 ) (f1  f2  f3)(g1  g2  g3)) ]        a b c d    e1 e2 e3 f1 f2 f3 g1 g2 g3 Parité négative Parité positive Parité positive Parité positive et négative Transformation en CNF : un exemple Soit une formule  = [( ((a  b))  (c  d) )((e1  e2  e3 ) (f1  f2  f3)(g1  g2  g3)) ] Transformation de  en CNF : 1. ’ = NNF( ) : remplacer les  et  : - [( ((a  b))  (c  d) )((e1  e2  e3 ) (f1  f2  f3)(g1  g2  g3)) - [( ( ((a  b))  (c  d) )  ( (c  d)  ((a  b)) ) ) ((e1  e2  e3 ) (f1  f2  f3)(g1  g2  g3)) ] - [( (((a  b))  (c  d) )  ((c  d)  ((a  b)) ) ) ((e1  e2  e3 ) (f1  f2  f3)(g1  g2  g3)) ] - [(( (((a  b))  (c  d) )  ((c  d)  ((a  b)) ) ) )  ((e1  e2  e3 ) (f1  f2  f3)(g1  g2  g3)) ] Transformation en CNF : un exemple (suite)  descendre les négations au niveau atomique descendre les négations au niveau atomique : ’ = [ ((a  b  c  d)  ( (c  d)  (a  b) ))  ((e1  e2  e3 ) (f1  f2  f3)(g1  g2  g3)) ] 2. Appliquer les règles [( (a  uploads/Voyage/ socsat.pdf