Descriptif

Le problème de cohérence en logique propositionnelle (SAT) consiste à déterminer s’il existe une interprétation booléenne d’une formule propositionnelle donnée la rendant vraie. Il est l’un des problèmes centraux en théorie de la complexité et en informatique de manière général. En outre, ces dernières années ont connu une remarquable percée dans la résolution pratique du problème SAT, ce qui a ouvert de nombreux champs d’application pour ce dernier.

Etant un problème NP-complet, plusieurs classes traitables en SAT ont été identifiées dans la littérature (Horn, R-Horn, Q-Horn, Krom, etc). Une classe traitable d’un problème peut être vue comme une partie des entrées possibles pour laquelle le problème peut être résolu par une procédure s’exécutant en temps polynomial. En dépit du fait que le théorème de dichotomie de Schaefer fournit une caractérisation des classes traitables en SAT avec des conditions nécessaires et suffisantes, la caractérisation de nouvelles classes traitables en SAT par de nouvelles approches reste un défi important.

Plusieurs problèmes NP-complets connus admettent de nombreuses classes traitables, notamment dans la théorie des graphes. Cela dit, il existe peu de travaux abordant la question de trouver les contreparties équivalentes de ces classes en SAT. Partant de ce constat, l’objet de cette thèse est l’étude des liens qui peuvent exister entre des classes traitables de problèmes dans la théorie des graphes et le problème SAT. Dans la théorie des graphes, nous nous focaliserons dans notre étude, en particulier, sur le problème de recherche d’un couplage de taille maximum, qui est traitable, et aux nombreuses classes traitables du problème de recherche d’un stable de taille maximum. En d’autres termes, il s’agit ici d’utiliser ces deux problèmes pour proposer une nouvelle approche permettant de caractériser de nouvelles classes traitables dans le problème SAT.