Thèse en Informatique

Gilles Audemard

Informations

• Publié par: Sheaz
• Nombre de lectures: 70
• Langue: Français

Extrait

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 expl