De la résolution du problème SAT
à
la résolution de problèmes autour de SAT



 
 

La représentation des connaissances et les problèmes d'inférence associés restent à l'heure actuelle une problématique riche et centrale en Intelligence Artificielle.
Considérant la logique propositionnelle comme langage de représentation, l'étude théorique et pratique du problème de la satifiabilité d'une formule booléenne (SAT) devient essentielle.
Mais, au-delà de ces objectifs, le problème SAT (problème NP-Complet de référence) se retrouve comme sous-problème ou cas particulier dans de nombreux domaines comme les problèmes de satisfaction de contraintes, la démonstration automatique, la vérification de circuit, la planification, la cryptographie, etc.

Dans la première partie, je presente  mes contributions sur « la résolution du problème SAT » qui se structurent autour de quatre thèmes :

  • exploitation des propriétés structurelles,
  • aspects liés au codage et à l'extension du formalisme,
  • aspects algorithmiques
  • la génération aléatoire et phénomène de seuil.
  • Dans la seconde partie, je décris mes travaux « autour de SAT» :
  • la résolution des problèmes de satisfaction de contraintes (CSP)
  • la compilation et la révision des bases de connaissances,
  • fusion et validation de bases de connaissances.
  • Je termine par une description de mes perspectives à court et à moyen terme.