Thèse en Informatique
145 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Thèse en Informatique

-

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
145 pages
Français

Description

Annee´ 2001`THESEpresent´ ee´ a`´L’UNIVERSITE D’AIX MARSEILLE Iau sein du Laboratoire d’Informatique de Marseillepour obtenir le titre de´DOCTEUR DE L’UNIVERSITE D’AIX MARSEILLE ISpecialit´ e´ : Informatiquepar Gilles AUDEMARD´ ` ´ ´Resolution du probleme SAT et generation demodeles` finis en logique du premier ordreSoutenue le 25 octobre 2001Devant le jury compose´ deBelaid BENHAMOU Maˆıtre de Conference´ a` l’Universite´ de Provence (directeur de these)`Jean Jacques CHABRIER Professseur a` l’Universite´ de Bourgogne (rapporteur)Chu Min LI Maˆıtre de Conference´ a` l’Universite´ de Picardie (examinateur)Lakhdar SAIS Professeur a` l’Universite´ Paul Sabatier (examinateur)Pierre SIEGEL a` l’Universite´ de Provence (eJian ZHANG Research Professor - Chinese Academy of Sciences (rapporteur)`Table des matieresListe des figures iiiListe des tableaux vListe des algorithmes viiIntroduction 1`I A propos du probleme SAT 51 Logique propositionnelle et probleme` SAT 71.1 La logique propositionnelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81.1.2 Semantique´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81.1.3 Consequence´ logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91.1.4 Forme conjonctive normale CNF . . . . . . . . . . . . . . . . . . ...

Sujets

Informations

Publié par
Nombre de lectures 70
Langue Français

Exrait

Annee´ 2001
`THESE
present´ ee´ a`
´L’UNIVERSITE D’AIX MARSEILLE I
au sein du Laboratoire d’Informatique de Marseille
pour obtenir le titre de
´DOCTEUR DE L’UNIVERSITE D’AIX MARSEILLE I
Specialit´ e´ : Informatique
par Gilles AUDEMARD
´ ` ´ ´Resolution du probleme SAT et generation de
modeles` finis en logique du premier ordre
Soutenue le 25 octobre 2001
Devant le jury compose´ de
Belaid BENHAMOU Maˆıtre de Conference´ a` l’Universite´ de Provence (directeur de these)`
Jean Jacques CHABRIER Professseur a` l’Universite´ de Bourgogne (rapporteur)
Chu Min LI Maˆıtre de Conference´ a` l’Universite´ de Picardie (examinateur)
Lakhdar SAIS Professeur a` l’Universite´ Paul Sabatier (examinateur)
Pierre SIEGEL a` l’Universite´ de Provence (e
Jian ZHANG Research Professor - Chinese Academy of Sciences (rapporteur)`Table des matieres
Liste des figures iii
Liste des tableaux v
Liste des algorithmes vii
Introduction 1
`I A propos du probleme SAT 5
1 Logique propositionnelle et probleme` SAT 7
1.1 La logique propositionnelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.1.2 Semantique´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.1.3 Consequence´ logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.1.4 Forme conjonctive normale CNF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.1.5 Le probleme` SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
Methodes´ incompletes` . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
M´ completes` . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2 Algorithmes enum´ eratifs´ pour SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.3 Heuristiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.3.1 Heurisitique de type ¡¡Maximum Occurences in Minimun Size Clauses¿¿ . . . . . . . . . . 14
1.3.2 Heuristiques de type UP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.4 Instances difficiles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.5 Quelques methodes´ enum´ erati´ ves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.5.1 Le systeme` POSIT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.5.2 Le systeme` SATZ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.5.3 Le systeme` SATO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.5.4 Le systeme` CSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.5.5 Vers des algorithmes cibles´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21ii Table des Matier` es
2 La methode´ AVAL 23
2.1 Production des mono–litteraux´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.2 La methode´ AVAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3 Une version dynamique de RLI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.4 Le choix des litteraux´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3 Experimentations´ 33
3.1 Comparaison des methodes´ DP et AVAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.2 Taux de reussite´ dans la production de litteraux´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3 Seuil de production des mono–litteraux´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.4 Complexite´ de l’algorithme RLI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.5 Comparaison avec SATZ, SATO et POSIT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.5.1 Instances aleatoires´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.5.2 Challenge DIMACS et Beijing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
´ ´ `II Generation de Modeles Finis 43
4 Gen´ eration´ de modeles` finis en logique du premier ordre 45
4.1 La logique des predicats´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
´4.1.2 Semantique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.1.3 Conventions et notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.1.4 Formes normales conjonctives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
Theories´ equationnelles´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.2 Quelques gen´ erateurs´ de modeles` finis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.2.1 La methode´ MACE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.2.2 La methode´ FMSET . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.2.3 La methode´ SEM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.2.4 La methode´ FINDER . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.2.5 La methode´ FMC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.2.6 La methode´ MGTP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
4.3 Conclusion et discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5 Propagations de Contraintes et Heuristiques 61
5.1 Filtrage des domaines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
5.1.1 Transformation des clauses (Approche statique) . . . . . . . . . . . . . . . . . . . . . . . . 62
´5.1.2 Elimination dynamique des valeurs incompatibles . . . . . . . . . . . . . . . . . . . . . . . 63
Heuristique UP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
5.2 Dependances´ des symboles fonctionnels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
5.2.1 Graphe de dependances´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67Table des Matier` es iii
5.2.2 Creation´ d’un ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.2.3 Heuristiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
L’heuristique GOT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
L LNHO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6 Suppression de symetries´ 73
6.1 Symetries´ en logique du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.1.1 Notion de groupes et de groupes symetriques´ . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.1.2 Les symetries´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6.2 Differentes´ approches de suppression des symetries´ . . . . . . . . . . . . . . . . . . . . . . . . . . 76
6.2.1 Heuristique LNH et valeurs interchangeables . . . . . . . . . . . . . . . . . . . . . . . . . 76
6.2.2 Recherche dynamique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
6.2.3 Rajout de contraintes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.2.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
6.3 XLNH : Une extension de l’heuristique LNH . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
6.3.1 Les fonctions unaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
6.3.2 Gen´ eration´ d’une fonction unaire bijective . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.3.3 La procedure´ d’enum´ eration´ selon l’heuristique XLNH . . . . . . . . . . . . . . . . . . . . 81
Premiere` etape´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
Deuxieme` etape´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
6.3.4 Extension a` toutes les fonctions unaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
6.4 Recherche et exploitation dynamique des symetries´ . . . . . . . . . . . . . . . . . . . . . . . . . . 88
6.4.1 Notion de symetries´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
6.4.2 Detection´ des symetries´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
Les conditions necessaires´ de la symetrie´ . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
Calcul de la symetrie´ : verification´ de la condition suffisante . . . . . . . . . . . . . . . . . 90
6.4.3 Exploitation des symetries´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
6.4.4 Combinaison des symetries´ detect´ ees´ avec celles de LNH . . . . . . . . . . . . . . . . . . . 94
6.4.5 Symetries´ horizontales et verticales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
6.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
7 Experimentations´ 97
7.1 Liste des problemes` experiment´ es´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.1.1 Groupes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.1.2 Anneaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
7.1.3 Algebre` ternaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
7.1.4 Quasigroupes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
7.1.5 Verification´ de programmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
7.1.6 Logique temporelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
7.2 Comportement des differentes´ strategies´ proposees´ . . . . . . . . . . . . . . . . . . . . . . . . . . 100
7.2.1 La methode´ VESEM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100iv Table des Matier` es
7.2.2 Les heuristiques GOT et LNHO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
Une nouvelle heuristique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
7.2.3 La methode´ XLNH . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
7.2.4 Recherche dynamique de symetries´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
7.3 Comparaison des differentes´ methodes´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
7.3.1 Le probleme` NAG . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
7.3.2 Le probleme` GRP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
7.3.3 Le probleme` RU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
7.3.4 Les probleme` RNA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
7.3.5 Le probleme` RNG025-8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
7.3.6 Le probleme` PRV004 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
7.3.7 Les quasigroupes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
7.4 Recherche de tous les modeles` . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
`7.4.1 Recherche de tous les modeles de AG . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
7.4.2 de tous les modeles` de RU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
7.4.3 Recherche de tous les modeles` de TBA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
7.4.4 Le challenge du probleme` LTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
7.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
Conclusion et perspectives 119
Bibliographie 123v
Liste des figures
1.1 Phenom´ ene` de seuil pour 3–SAT aleatoires´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.2 Difficulte´ des instances 3–SAT aleatoires´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.3 Exemple d’arbre de clauses avec SATO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1 Arbres de recherche gen´ er´ es´ par les methodes´ DP et AVAL . . . . . . . . . . . . . . . . . . . . . . . 27
3.1 Reussite´ des appels a` RLI en fonction de la profondeur . . . . . . . . . . . . . . . . . . . . . . . . 35
3.2 Localisation des appels a` RLI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.3 Seuil de production . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.4 Complexite´ des differents´ algorithmes RLI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.1 Transformation d’une theorie´ dans MACE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.2 Classification des gen´ erateurs´ de modeles` finis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
5.1 Arbre de recherche avec la transformation de clauses reductibles´ . . . . . . . . . . . . . . . . . . . 63
5.2 Arbre de sans transformation des clauses r´ . . . . . . . . . . . . . . . . . . . . 64
5.3 Graphe de dependances´ d’un anneau unitaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.4 Axiomes et graphe de dependance´ du probleme` RNG041–1 . . . . . . . . . . . . . . . . . . . . . . 70
5.5 Graphe de dependances´ du probleme` RNG025–8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
6.1 Comportement de LNH et de XLNH . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
6.2 L’arbre de recherche avec XLNH pour les groupes abeliens´ d’ordre 5 . . . . . . . . . . . . . . . . . 84
6.3 Une interpretation´ unaire canonique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
6.4 Symetrie´ horizontale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
6.5 Symetrie´ verticale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
7.1 Forme de la fonction unaire dans un modele` de LTL . . . . . . . . . . . . . . . . . . . . . . . . . . 116vii
Liste des tableaux
3.1 Comparaison entre DP et AVAL (Nœuds) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.2 Comparaison entre DP et AVAL (Temps) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3 Pourcentage de succes` de l’algorithme RLI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.4 Comparaison sur les Problemes` Aleatoires´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.5 sur le challenge DIMACS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.6 Comparaison sur le challenge Beijing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6.1 Nombre de partitions den . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
6.2 d’interpretations´ gen´ er´ ees´ parInterpr´ etation Can . . . . . . . . . . . . . . . . . . . . 88
7.1 Axiomes d’un groupe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
7.2 d’un anneau . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
7.3 Axiomes d’une algebre` ternaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
7.4 Axiomes des quasigroupes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
7.5 de LTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
7.6 Impact de la proposition 5.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
7.7 Impact de l’heuristique UP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
7.8 Nombre de valeurs de domaines supprimees´ par la methode´ VESEM . . . . . . . . . . . . . . . . . 102
7.9 Differents´ ordres pour la resolution´ de RU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
7.10 Comportement des heursitiques GOT et LNHO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
7.11 Amelioration´ de l’heuristique LNHO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
7.12 Importance de l’ordre des fonctions dans l’heuristique XLNH. . . . . . . . . . . . . . . . . . . . . 104
7.13 Influence de la suppression des valeurs interchangeables dans XLNH . . . . . . . . . . . . . . . . . 104
7.14 Comportement de l’algorithme de recherche des symetries.´ . . . . . . . . . . . . . . . . . . . . . . 105
7.15 Influence de l’heuristique LNHO+ sur la recherche des symetries´ . . . . . . . . . . . . . . . . . . . 105
7.16 Temps de resolution´ du probleme` NAG . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
7.17 Temps de r´ du probleme` GRP100 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
7.18 Temps de resolution´ du probleme` RU . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
7.19 Temps de r´ du probleme` RNA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
7.20 Temps de resolution´ du probleme` RNG025 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
7.21 Temps de resolution´ du probleme` PRV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
7.22 Temps de r´ du probleme` QG1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
7.23 Temps de resolution´ du probleme` QG6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112viii Liste des Tableaux
7.24 Temps de resolution´ lors de la recherche de tous les modeles` de AG . . . . . . . . . . . . . . . . . . 113
7.25 Temps de r´ lors de la de tous les modeles` de RU . . . . . . . . . . . . . . . . . . 114
7.26 Temps de resolution´ lors de la recherche de tous les modeles` de TBA . . . . . . . . . . . . . . . . . 115
7.27 Temps de r´ et nombre de modeles` gen´ er´ es´ pour LTL . . . . . . . . . . . . . . . . . . . . . 116