Jeux combinatoires et formules booléennes quantifiées (QBF) : encodages pour le jeu de Tic-Tac-Toe d'Harary

Boucher, Steve (2026). « Jeux combinatoires et formules booléennes quantifiées (QBF) : encodages pour le jeu de Tic-Tac-Toe d'Harary » Thèse. Montréal (Québec), Université du Québec à Montréal, Doctorat en informatique.

Fichier(s) associé(s) à ce document :

Prévisualisation	PDF Télécharger (811kB)

Résumé

Les jeux combinatoires posent des défis complexes et nécessitent des raisonnements sophistiqués pour déterminer si un joueur a, ou non, une stratégie gagnante, et ce, indépendamment des choix de l’autre joueur. Les formules booléennes quantifiées (QBF), où l’alternance de quantificateurs universels et existentiels est de nature interactive, possèdent une sémantique naturelle en termes de jeux, ce qui en fait une représentation totalement adéquate et prometteuse pour la détermination de stratégies gagnantes. Toutefois, en pratique, la résolution de jeux à l’aide des solveurs QBF actuels reste difficile dans des délais raisonnables. Néanmoins, les QBF offrent un formalisme très souple et versatile qui permet d’exprimer de nombreuses conditions, de manières très différentes. L’objectif de cette thèse est d’explorer cette versatilité pour analyser les stratégies gagnantes du jeu de Tic-Tac-Toe d’Harary (HTTT), un achievement game bien connu qui a suscité l’intérêt autant des théoriciens que des membres de la communauté QBF. À la différence des travaux existants sur les encodages QBF pour les jeux combinatoires, cette thèse innove en exploitant la dualité entre les joueurs et en introduisant des encodages tant pour l’existence d’une stratégie gagnante pour le premier joueur que pour l’existence d’une stratégie bloquante pour le second. De plus, ce travail montre qu’on peut formaliser avec profit l’existence de stratégies spécifiques, tout en ne réduisant pas la portée de la méthode en termes pratiques. Tous les encodages introduits dans cette thèse sont évalués expérimentalement de façon détaillée sur un vaste ensemble d’instances HTTT. Cela permet non seulement d’établir la performance des méthodes développées, comparativement aux encodages existants, à l’aide des solveurs QBF les plus performants, mais aussi de tirer des conclusions générales sur le jeu de HTTT. Cette dernière avancée est d’importance puisque, au-delà de la performance de la résolution de HTTT, il y a un grand intérêt en combinatoire pour déterminer s’il y a, ou non, une stratégie gagnante pour les instances particulières de HTTT. Cette thèse contribue donc à l’avancement des connaissances et de la performance de l’approche QBF, tout en appliquant ses méthodes à un jeu, en l’occurence HTTT, qui est d’un intérêt allant bien au-delà de la communauté QBF.

Type:	Thèse ou essai doctoral accepté
Informations complémentaires:	Fichier numérique reçu et enrichi en format PDF/A.
Directeur de thèse:	Villemaire, Roger
Mots-clés ou Sujets:	Formule booléenne quantifiée / Jeux combinatoires / Tic-Tac-Toe d’Harary
Unité d'appartenance:	Faculté des sciences > Département d'informatique
Déposé par:	Service des bibliothèques
Date de dépôt:	22 janv. 2026 14:39
Dernière modification:	22 janv. 2026 14:39
Adresse URL :	http://archipel.uqam.ca/id/eprint/19528

Modifier les métadonnées (propriétaire du document)

Statistiques