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 :
Dans la seconde partie, je décris mes travaux « autour de SAT» :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. Je termine par une description de mes perspectives à court et à moyen terme.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.