Responsable : Philippe JEGOU




Mots clés : Intelligence Artificielle, Logique, Représentation des Connaissances,
Algorithmique et Complexité, Programmation par contraintes, SAT, CSP, Max-SAT


Les travaux développés par INCA portent sur des sujets qui relèvent principalement de l’Intelligence Artificielle : la représentation logique des connaissances et la formalisation du raisonnement ainsi que la démonstration automatique et l’algorithmique associée à la résolution des problèmes de satisfaction de contraintes (SAT et CSP principalement).

Synthétiquement, on peut estimer que notre activité porte sur deux axes complémentaires :

  • la représentation logique des connaissances et le raisonnement
  • l’algorithmique pour la satisfaction de contraintes

Toutefois, scinder nos activités relève d’une dichotomie artificielle car une des forces du projet est justement de s’appuyer sur ces deux thèmes. En effet, les formalismes de représentation des connaissances que nous étudions nécessitent la mise en œuvre de méthodes de raisonnement efficaces. Cependant, le recours à des cadres de représentation très expressifs conduit en général à formuler des problèmes dont la complexité se situe au mieux dans la classe des problèmes NP-Complets. L’une des nos ambitions consiste à définir et à étudier des formalismes de représentation suffisamment puissants mais pour lesquels nous disposerons soit de fragments traitables en théorie i.e. de complexité polynomiale, soit de méthodes et algorithmes opérationnels en pratique.

Ainsi, les deux axes principaux de la recherche des membres du projet se positionnent d’une part autour de la représentation des connaissances et de la logique et d’autre part, autour de la résolution des problèmes de satisfaction de contraintes.


La représentation des connaissances du monde réel pose un ensemble de problèmes : la connaissance est typiquement incomplète, floue, sujette au changement et provient de différentes sources souvent incohérentes entre elles. La représentation de telles connaissances et leur gestion efficace a toujours été une thématique centrale dans l’Intelligence Artificielle. Elle pose des défis à la fois en termes de calculabilité et de complexité. Dans ce premier axe rentrent les recherches sur la fusion et la révision de connaissances, sur le traitement de connaissances incomplètes et prototypiques (logiques non-monotones et des conditionnels), sur les méthodes de déduction pour les logiques floues. Une direction stratégique de recherche est le développement de systèmes de preuve pour les logiques non-classiques, notamment pour les logiques qui formalisent le raisonnement plausible et révisable d’un agent rationnel. Dans cette famille rentrent les logiques des conditionnels et les logiques non-monotones pour l’inférence plausible. Une telle étude a plusieurs objectif : (i) une meilleure ompréhension des systèmes logiques en soi par le biais d’une présentation constructive en termes e calculsou systèmes de preuve, à l’opposé de la présentation émantique/algébrique, basée sur une théorie des modèles, (ii) le développement des systèmes de raisonnement utomatique (démonstrateurs), (iii) l’applications à la représentation des connaissances raisonnement non-monotone, application aux logiques des description et ontologies). Un domaine d’application de nos travaux sur ce thème porte notamment sur les problèmes de diagnostic.


Dans le deuxième axe rentrent les recherches sur la résolution du problème général de la satisfiabilité (SAT), sur la résolution des problèmes de satisfaction de contraintes (au sens CSP à domaines finis qui est une extension de SAT) et leurs extensions à l’optimisation (cf. MAX-SAT, MAX-SAT pondéré et les CSP Pondérés), voire au dénombrement (cf. #SAT et #CSP). Cette activité s’avère nécessaire pour doter les systèmes de raisonnement de l’Intelligence Artificielle d’outils de résolution efficaces à la fois en théorie (cf. notion de classe polynomiale) et en pratique (solveurs "compétitifs"), sachant qu’à la base, SAT et CSP sont NP-complets, et leurs extensions NP-difficile pour l’optimisation et #P-complet pour le dénombrement.

Il y a donc des thèmes ou des préoccupations communes entre les deux axes, notamment le problème de la satisfiabilité des formules de la logique booléenne (SAT) est ses généralisations. Ce problème revêt un intérêt central pour l’inférence automatique et constitue un champ d’application privilégié des méthodes de résolution de contraintes. D’autres recherches plus spécifiques comme l’étude des symétries dans les modèles par exemple, ou la planification automatique, se situent à la frontière entre représentation logique des connaissances et résolution de contraintes. En termes d’applications, nous avons étudié, entre autres, les problèmes de packing, et plus récemment, les problèmes de plus court chemins contraints (généralisation multicritère des problèmes classiques de plus courts chemins). Il s’agit là d’exemples significatifs de l’application de techniques algorithmiques basées sur la résolution de contraintes à des problèmes parfois situés au-delà des champs ’investigation classiques de l’Intelligence Artificielle.