Thèse en Informatique

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 . . . . . . . . . . . . . . . . . . ...