Date : 1993
Editeur / Publisher : [S.l.] : [s.n.] , 1993
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : DE NOMBREUX PROBLEMES INTRAITABLES AVEC LES METHODES DE RESOLUTION CLASSIQUES PRESENTENT UNE STRUCTURE TRES SYMETRIQUE (L'ECHANGE DE PROPOSITIONS LAISSE CETTE STRUCTURE INVARIANTE). DANS LA PREMIERE PARTIE, ON MONTRE QUE L'UTILISATION DES PROPRIETES DE SYMETRIES PERMET UNE AMELIORATION CONSIDERABLE DE L'EFFICACITE DES ALGORITHMES DE DEMONSTRATION AUTOMATIQUE (PREUVE DE COMPLEXITE LINEAIRE POUR LE PROBLEME DE PIGEON-HOLE, PREMIERE DEMONSTRATION AUTOMATIQUE DU PROBLEME DE RAMSEY R(3,3,3)) AINSI QU'UNE REPRESENTATION PLUS COMPACTE DE L'ENSEMBLE DES SOLUTIONS. DANS LA SECONDE PARTIE, CE TRAVAIL A AMENE LE DEVELOPPEMENT D'UNE EXPRESSION PLUS NATURELLE ET COMPACTE DES PROBLEMES, FONDEE SUR LA NOTION DE CARDINALITE QUI GENERALISE LA REPRESENTATION CLAUSALE CLASSIQUE. UNE CLAUSE GENERALISEE EST UN COUPLE (N,L): OU N DESIGNE LE NOMBRE MINIMUM DE LITTERAUX DE LA AFFECTER A VRAI. UNE METHODE DE RESOLUTION COMPLETE ET DECIDABLE POUR CES CLAUSES EST DECRITE. UNE PROPRIETE D'EQUIVALENCE ENTRE LA REPRESENTATION CLAUSALE CLASSIQUE ET CLAUSES GENERALISEES EST DEMONTRE. CETTE PROPRIETE PERMET D'ADAPTER EFFICACEMENT CERTAINS OUTILS DE LA RESOLUTION CLASSIQUE