Membres du thème
| NOM Prénom | Statut |
|---|---|
| BARICHARD Vincent | Maître de conférences |
| BEHUET Corentin | Doctorant |
| DEGUIEZ LODEIRO Martin | Maître de conférences |
| DEVRED Caroline | Maître de conférences |
| GARCIA Laurent | Maître de conférences |
| GARREAU Bryan | Doctorant |
| LARDEUX Frédéric | Professeur |
| LEFEVRE Claire | Maître de conférences |
| LEGEAY Marc | Maître de conférences |
| LESAINT David | Professeur |
| MONFROY Éric | Professeur |
| SEKAR Suruthy | Doctorant |
| STEPHAN Igor | Maître de conférences/HDR |
| VASCONCELLOS Claudia | Enseignant-chercheur contractuel |
Le thème RIC fédère les travaux du laboratoire autour du raisonnement non-monotone et des approches déclaratives pour la résolution de problèmes combinatoires (livret détaillé). L’accent est mis sur la représentation des connaissances et les efforts se portent sur la conception de langages de modélisation et le développement de techniques de transformation ou d’encodage de modèles visant à concilier flexibilité et efficacité. Les travaux, qui abordent les fondements théoriques de ces outils mais aussi leur implantation et leurs applications, s’appuient sur des paradigmes de modélisation haut-niveau tels la programmation par ensembles-réponses (ASP) et la programmation par contraintes (PPC, CHR) ainsi que sur des formalismes plus élémentaires tels CSP et SAT :
- Extension des cadres ASP et CHR : intégration de variables existentielles en ASP pour le raisonnement ontologique, gestion de préférences en ASP possibilistes pour la révision de croyances, quantification de contraintes en CHR pour les problèmes à horizon non borné.
- Modélisation, transformation et encodage : CSP ensemblistes et encodages CSP/SAT, décomposition de problème fondée sur l’interprétation abstraite et la PPC, PPC pour la transformation de modèles en ingénierie des modèles, PPC pour la recherche de motifs en fouille de données.
Programmation par ensembles-réponses
L’ASP (Answer Set Programming) est un langage déclaratif développé afin de traiter des connaissances en intelligence artificielle, lorsque les informations sont incomplètes, ou pour résoudre des problèmes combinatoires. Nos travaux portent sur diverses extensions du cadre de l’ASP et allient théorie et pratique.
Nous développons depuis plusieurs années un solveur ASP, ASPeRiX, basé sur une approche originale guidée par les règles et ne nécessitant pas d’instanciation préalable du programme. Nos travaux récents montrent que l’algorithme sous-jacent à ASPeRiX peut s’exprimer de manière efficace et extensible en CHR. Nous travaillons à une mise à jour majeure d’ASPeRiX basée sur le langage CHR (et sa version CHR++ développée au sein du laboratoire) qui permettra de remplacer le backtrack chronologique d’ASPeRiX par un backtrack intelligent et, d’un autre côté, pourra intégrer aisément des contraintes définies par l’utilisateur ainsi que les extensions modernes d’ASP.
Par ailleurs, dans le cadre de l’étude de la fusion multi-sources et de l’interrogation d’informations issues du web, généralement exprimées en logique de description (projet ANR ASPIQ), nous nous sommes par exemple intéressés à l’intégration dans l’ASP des variables existentielles, inhérentes aux ontologies exprimées en logique de description, ainsi qu’à l’interrogation de ces ontologies en ASP.
D’autre part, nous nous intéressons à la révision de croyances lorsque les connaissances sont exprimées par un programme ASP. Cette problématique étant peu étudiée, nous proposons une sémantique, des postulats de révision et une étude de complexité de la révision en ASP. Enfin, l’intégration de préférences entre connaissances a amené à l’étude de la révision en ASP possibiliste. Nous étudions de nouveaux modes de révision tirant profit de la structure des règles ASP (révision par ajout, par exemple) et nous essayons de déterminer s’il est possible d’élaborer une caractérisation logique de l’ASP possibiliste en termes de logique d’équilibre ce qui pourrait donner un cadre pour l’étude de théories arbitraires dans l’ASP possibiliste.
Concernant l’ASP, nous nous intéressons plus généralement à l’explicabilité des résultats. Cette étude est nécessaire pour nos travaux sur le backjumping et pourra aussi être utilisée dans le cadre de l’ASP possibiliste.
Toujours préoccupés par la mise en pratique de l’ASP sur des applications réelles, nous sommes partie prenante du projet Potassco Solutions, initié par nos collègues de Potsdam, dont nous sommes les correspondants français.
Modélisation par contraintes, conversion et reformulation de modèles
À l’origine, la programmation par contraintes comportait deux volets primordiaux : le langage pour modéliser les problèmes, et les solveurs pour résoudre ces derniers. Pendant de nombreuses années, les efforts se sont portés sur les solveurs afin d’améliorer la résolution. Cependant, il y a quelques années, la partie langage est revenue sur l’avant de la scène, car la modélisation permet d’ouvrir les contraintes à des utilisateurs non experts, mais également d’obtenir des modèles possiblement plus robustes et résolus beaucoup plus efficacement. Différents aspects peuvent être pris en compte tels que la reformulation de modèle, la conversion de modèle ou le langage de modélisation. Nous travaillons principalement sur les voies suivantes.
Contraintes ensemblistes
Par rapport aux modélisations basées sur des matrices ou des entiers, les ensembles sont pratiques car ils réduisent naturellement le nombre de symétries. De plus, il est bien connu que de nombreux problèmes peuvent être facilement modélisés avec des contraintes ensemblistes. Plusieurs solveurs de contraintes spécialisés pour les contraintes ensemblistes existent déjà. Nous nous intéressons à divers aspects des contraintes ensemblistes : les modèles CSP avec contraintes ensemblistes, la réduction des variables à domaine fini et des variables ensemblistes ainsi qu’à l’encodage des contraintes ensemblistes en SAT.
Encodage CSP/SAT
Nous travaillons sur les encodages CSP vers SAT afin de mieux comprendre les facteurs clés qui déterminent leurs caractéristiques ainsi que leurs effets sur la résolution. Dans un premier temps, nous analysons l’impact de la provenance des variables du modèle SAT sur l’heuristique de branchement les solveurs SAT. En effet, certaines variables du modèle SAT correspondent directement à des variables du modèle CSP alors que d’autres, dites auxiliaires, sont ajoutées lors de l’encodage des contraintes du modèle CSP. Nous travaillons également sur l’encodage de mécanismes de propagation propres aux solveurs CSP dans le modèle SAT. Afin d’encoder au mieux le maximum d’informations provenant du mécanisme de propagation CSP sans pour autant augmenter de manière démesurée la taille de l’instance SAT, nous proposons de nouveaux encodages SAT comme par exemple l’Abacus encoding.
Problèmes quantifiés sous contraintes
Il existe plusieurs formalismes et langages de modélisation issus de la programmation par contraintes comme CSP et CHR (Constraint Handling Rules). Les CSP ont donné lieu à plusieurs extensions dont les QCSP (Quanfitied Constraint Satisfaction Problem) qui adressent les problèmes quantifiés sous contraintes. Néanmoins les formalismes quantifiés de la littérature sont à horizon borné ce qui rend difficile voire impossible la modélisation de certains problèmes quantifiés qui nécessite une représentation en intention et non en extension de la combinatoire. C’est pourquoi nous proposons une approche étendant CHR pour intégrer la quantification. Ceci nous permet de modéliser des problèmes à horizon non borné.
Constraint Handling Rules
La programmation par contraintes tire ses racines de la programmation logique et peut être vue comme une forme de programmation logique qui incorpore des contraintes. Cette variante de la programmation logique, appelée communément programmation logique par contraintes, a été implémentée dans différents systèmes (Prolog III, CLP (R) et CHIP). Ces systèmes sont aujourd’hui supplantés par les solveurs PPC plus efficaces. Toutefois, lorsque l’on souhaite innover, il est nécessaire de sortir du carcan d’un solveur PPC, tâche difficile avec les solveurs actuels. C’est pourquoi depuis quelques années nous cherchons un langage de modélisation de contraintes d’un autre niveau d’abstraction. Notre choix s’est porté sur CHR (Constraint Handling Rules). CHR est un langage de modélisation et de programmation de haut niveau basé sur des règles de propagation descriptives et applicables. Les axiomes du langage sont de plus bas niveau que les contraintes habituelles d’un solveur PPC, mais elles permettent de redéfinir facilement et rapidement chacune d’elles. CHR est implémentée comme extension d’un langage hôte et est disponible pour Prolog, Haskell, Java …C’est pourquoi nous développons CHR++1, notre propre implémentation de CHR au dessus de C++. CHR++ implémente un mécanisme d’exploration arborescent avec retour arrière permettant la recherche d’une solution comme un solveur PPC. Il allie à la fois la puissance de modélisation et la simplicité d’utilisation d’un solveur PPC, la souplesse d’un langage de programmation logique et la performance d’un langage impératif. Nous avons utilisé la logique linéaire pour formaliser le système, et travaillons à étendre le langage par l’ajout de concepts tels que : la disjonction hiérarchique, les contraintes bang ou les contraintes permanentes. Nos travaux sont ensuite appliqués à divers domaines et applications comme les QCSP, l’ASP, la transformation de modèles et la conception d’emplois du temps.
Modélisation et résolution hybrides
Actuellement, les travaux liés à la frontière entre la programmation logique non-monotone (et de son langage phare, ASP) et la résolution de problèmes combinatoires contraints sur les domaines finis ne considère qu’un unique point de vue consistant à faire coopérer à haut niveau un solveur ASP et un solveur de contraintes. Un axe que nous explorons est d’appliquer des mécanismes de la propagation de contraintes à l’ASP.
Applications en cours
- L’ingénierie dirigée par les modèles consiste à abstraire les différentes parties d’un système sous la forme d’un ensemble de modèles, chaque modèle adoptant un niveau d’abstraction différent et adapté aux besoins de la personne les utilisant. Nous avons défini une approche permettant d’intégrer des contraintes dans des transformations de modèles, pour spécifier certaines contraintes spécifiques au domaine d’application (par exemple, la planification d’emploi du temps).
- Les emplois du temps universitaires (EDT) se construisent généralement par optimisation combinatoire et des travaux récents se sont intéressés à la révision d’EDT pour mieux répondre au caractère dynamique du problème et aux exigences des différents acteurs en termes de contrôle et d’explicabilité du calcul. Notre approche vise à établir un cadre formel pour la révision d’EDT ciblant particulièrement le système universitaire français et qui se fonde sur la programmation par contraintes et possibles hybridations afin d’intégrer opérations et stratégies de réparation.
- L’Inférence grammaticale consiste à apprendre automatiquement une grammaire formelle (généralement sous forme de règles de productions ou d’un automate) à partir d’un ensemble d’observations. Nous nous intéressons actuellement à la modélisation SAT et INLP d’automates finis non déterministes devant accepter un ensemble de mots donnés et rejeter un ensemble de mots n’appartenant pas au langage.