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érale. Étant un problème NP-complet, plusieurs classes traitables de ce problème ont été identifiées dans la littérature (Horn, Horn-renommable, 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. Dans ce contexte, 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 pouvant exister entre des classes traitables de problèmes dans la théorie des graphes et le problème SAT.

Lors de la première contribution de cette thèse, nous proposons une nouvelle approche de caractérisation de classes traitables pour le problème SAT. Ces dernières sont obtenues en considérant particulièrement la classe de graphes sans-étoile pour laquelle le problème de recherche d'un stable maximum est traitable. La seconde contribution de cette thèse concerne le problème Exactly-One-SAT qui consiste à déterminer si une formule CNF admet un modèle tel que chaque clause a exactement un littéral satisfait. La classe introduite est définie par une propriété qui doit être satisfaite par des combinaisons de clauses. Cette classe peut être considérée comme une contrepartie des classes traitables pour le problème de recherche d'un stable maximum.

Rapporteurs :

  • Chu-Min Li, Professeur à l'Université de Picardie Jules Verne
  • Eric Monfroy, Professeur à l'Université d'Angers

Examinateurs :

  • Jean-François Condotta, Professeur à l'Université d'Artois
  • Souhila Kaci, Professeur à l'Université de Montpellier
  • Lakhdar Sais, Professeur à l'Université d'Artois (Directeur)
  • Yakoub Salhi, Maître de Conférences, HdR à l'Université d'Artois (Co-encadrant)