À chaque semestre, la direction du Département d'informatique de l'UQAM doit convenablement affecter les divers groupes-cours disponibles à ses professeurs, en se basant sur leurs préférences et certaines règles adoptées par l'assemblée départementale. Le but de notre travail est développer un algorithme qui trouve une solution de bonne qualité à ce problème, et ce dans un temps raisonnable. Dans ce mémoire, nous appliquons deux approches différentes pour résoudre le problème d'affectation des groupes-cours. La première est basée sur un algorithme branch-and-bound, qui est un algorithme de recherche exhaustif et complet. La deuxième est basée sur un processus heuristique de recherche local amélioré. Plus particulièrement, nous nous concentrons sur l'algorithme de recherche local. Des algorithmes de recherche locale divers sont présentés, entre autres, la recherche locale guidée et le recuit simulé. Ce que nous faisons n'est pas simplement d'appliquer ces algorithmes et les combiner ensemble. Nous essayons aussi de nous inspirer de ces algorithmes pour mettre au point quelques nouvelles idées appropriées pour notre propre problème. Finalement, nous utilisons les résultats expérimentaux obtenus par l'algorithme branch-and-bound comme point de référence en ce qui concerne la qualité de la solution et le temps d'exécution pour évaluer les autres approches. Les résultats que nous avons obtenus de données réelles et des données générées aléatoirement montrent que notre algorithme effectue un bon travail tant en termes de qualité de solution que de temps d'exécution. Les résultats montrent aussi que notre algorithme peut trouver une bonne solution à de grands problèmes en un temps raisonnable. ______________________________________________________________________________

Depuis quelques années, de nombreux champs de l'informatique ont été transformés par l'introduction d'une nouvelle vision de la conception et de l'utilisation d'un système, appelée approche déclarative. Contrairement à l'approche dite impérative, qui consiste à décrire au moyen d'un langage formelles opérations à effectuer pour obtenir un résultat, l'approche déclarative suggère plutôt de décrire le résultat désiré, sans spécifier comment ce «but» doit être atteint. L'approche déclarative peut être vue comme le prolongement d'une tendance ayant cours depuis les débuts de l'informatique et visant à résoudre des problèmes en manipulant des concepts d'un niveau d'abstraction toujours plus élevé. Le passage à un paradigme déclaratif pose cependant certains problèmes: les outils actuels sont peu appropriés à une utilisation déclarative. On identifie trois questions fondamentales qui doivent être résolues pour souscrire à ce nouveau paradigme: l'expression de contraintes dans un langage formel, la validation de ces contraintes sur une structure, et enfin la construction d'une structure satisfaisant une contrainte donnée. Cette thèse étudie ces trois problèmes selon l'angle de la logique mathématique. On verra qu'en utilisant une logique comme fondement formel d'un langage de « buts », les questions de validation et de construction d'une structure se transposent en deux questions mathématiques, le model checking et la satisfiabilité, qui sont fondamentales et largement étudiées. En utilisant comme motivation deux contextes concrets, la gestion de réseaux et les architectures orientées services, le travail montrera qu'il est possible d'utiliser la logique mathématique pour décrire, vérifier et construire des configurations de réseaux ou des compositions de services web. L'aboutissement de la recherche consiste en le développement de la logique CTLFO+, permettant d'exprimer des contraintes sur les données, sur la séquences des opérations d'un système, ainsi que des contraintes dites «hybrides». Une réduction de CTL-FO+ à la logique temporelle CTL permet de réutiliser de manière efficace des outils de vérification existants. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Méthodes formelles, Services web, Réseaux.