Problème SAT et CSPs: des modèles aux formules

En Intelligence Artificielle, la notion d’assignement à des variables peut modéliser la notion d’observation, à partir de capteurs par exemple.

Ainsi, l’observation que quelqu’un est brun et grand peut être vue comme l’affectation (couleur-cheveux=brun, grand=oui), etc.

Il est intéressant d’être capable de transformer des ensembles d’observations de cette forme en des formules, des ensembles de règles, afin de les intégrer à des bases de connaissances par exemple.

Je parlerai des problématiques algorithmiques que ces transformations soulèvent : description, identification, approximation, apprentissage par l’exemple, etc… dans le cadre de la logique propositionnelle et des problèmes de satisfaction de contraintes (CSPs), et notamment lorsque l’on cherche à obtenir des formules ayant des propriétés particulières (être de Horn par exemple).