Les activités d’INCA se déclinent en deux axes principaux qui s’organisent chacun en sous-thèmes :

Axe 1 - Représentation des connaissances et raisonnement en Intelligence Artificielle
Axe 2 - Satisfaction de contraintes et satisfiabilité

L’équipe réalise également des logiciels (essentiellement des solveurs) qui sont mis à disposition de la communauté (voir la rubrique « Logiciel » après la description des activités de recherche).Les thèmes de recherche sont présentés dans le détail ci-dessous :


Un des thèmes principaux de l’équipe porte sur la représentation des connaissances et le raisonnement automatique notamment, le changement de croyances, l’argumentation, les méthodes de déduction pour les logiques des conditionnels et similaires, et le raisonnement non-monotone appliqué aux logiques de descriptions.

Changement de croyances

Le changement de croyances est un thème de recherche important de l’Intelligence Artificielle depuis le début des années 1980. Dans de nombreuses applications un agent est confronté à des informations imparfaites, incomplètes, imprécises ou incertaines qui peuvent conduire à des incohérences. Deux approches sont alors possibles : soit définir des opérations de changement de croyances (révision ou fusion selon le contexte), soit définir de nouvelles relations d’inférence tolérant l’incohérence. Les travaux de l’équipe ont porté sur le changement de croyances représentées dans différents formalismes logiques.

Une partie importante des travaux a été développée dans le cadre du projet ANR blanc ASPIQ (http://aspiq.lsis.org) (octobre 2012 - août 2017) dont nous assurons la coordination (Odile PAPINI coordinatrice national du projet). Il implique également Farid NOUIOUA, Vincent RISCH, E. Würbel, Safa YAHI et Zied BOURAOUI pendant son stage post-doctoral. L’objectif général du projet était de proposer des solutions originales pour l’interrogation d’informations hétérogènes multi-sources à grande échelle. Les informations disponibles fournies par les sources sont exprimées dans des formalismes qui reposent sur des logiques de descriptions légères (DL-Lite), en particulier dans le cas du Web. L’une des idées du projet était de proposer et d’implanter des opérations de fusion et d’interrogation d’informations en s’appuyant sur la programmation logique avec sémantique de modèles stables (Answer Set Programming ou ASP). Dans le cadre du projet, nous nous sommes donc concentré sur deux formalismes logiques : les logiques de description légères, en particulier DL-Lite, la programmation logique avec sémantique de modèles stables (ASP). J. Hué, Odile PAPINI et E. Würbel ont d’abord défini des opérations de révision et de fusion syntaxiques de programmes logiques ASP basées sur l’approche des r-ensembles (removed sets). Deux familles d’opérateurs ont été définies en utilisant deux sémantiques, l’une reposant sur les modèles stables, l’autre basée sur les SE modèles (revue RIA 2012). E. Würbel a mis en oeuvre ces opérations et développé un prototype PLRSF. En collaboration avec S. Benferhat et Zied BOURAOUI (membres du projet ASPIQ), Odile PAPINI et E. Würbel ont ensuite défini des opérations de révision de bases de croyances exprimées en DL-Lite. Cette approche s’inspirant de l’approche r-ensembles considère que la terminologie (Tbox) est stable mais que les assertions (Abox) peuvent être révisées (conférences ISAIM 2014 et ECAI 2014). Dans le cas de bases de croyances DL-Lite stratifiées, ils ont proposé de nouveaux opérateurs de révision utilisant un ordre lexicographique sur les ensembles d’assertions à retirer (conférence JELIA 2014), ils ont également étudié les propriétés logiques ainsi que la complexité de ces opérations (revue AMAI 2016).

Concernant les relations d’inférence tolérant l’incohérence à partir de bases de croyances DL-Lite incohérentes, contrairement à l’approche des r-ensembles qui repose sur la minimisation de l’incohérence, cette approche se situe dans le cadre des réparations qui repose sur la maximisation de la cohérence. En collaboration avec S. Benferhat, K. Tabia, M.-L Mugnier, J. F. Baget, M. Croitoru, S. Rocher (membres du projet ASPIQ), Zied BOURAOUI et Odile PAPINI ont proposé un cadre général où une relation d’inférence est paramétrée par une sélection de sous-ensembles d’assertions à conserver et par une stratégie d’inférence. Ce cadre permet de capturer les relations d’inférence tolérant l’incohérence connues et d’en définir de nouvelles (conférence KR 2016). En collaboration avec S. Benferhat, K. Tabia, M. Croitoru (membres du projet ASPIQ), Zied BOURAOUI et Odile PAPINI ont également proposé une nouvelle relation d’inférence : « non objection inférence » où une requête est impliquée par au moins une réparation et est cohérente avec toutes les autres. Ils ont étudié les propriétés logiques de cette relation d’inférence et ils ont montré qu’elle a une complexité polynomiale (conférence IJCAI 2016).

Les travaux ont également porté sur le traitement de l’incertitude dans le cadre des ontologies légères exprimées en DL-Lite. Dans cette perspective, Farid NOUIOUA, en collaboration avec S. Benferhat, F. Khellaf et K. Boutouhami, ont proposée une extension possibiliste quantitative de DL-Lite dans laquelle l’incertitude est représentée en utilisant la théorie des possibilités quantitative (à base du produit). Ils ont montré en particulier que contrairement au cas de DL-Lite possibiliste qualitative, le problème d’inférence dans ce nouveau cadre est un problème difficile (conférence SMPS 2016). Afin de surmonter cette difficulté, ils ont proposé un codage du problème de calcul du degré d’inconsistance en termes du problème de couverture d’ensembles pondérés pour lequel il existe un algorithme glouton polynomial assurant une approximation de la solution. Ce codage leur a permis de proposer une méthode pour le calcul d’une valeur approchée du degré d’inconsistance qui a ensuite été utilisée dans un autre algorithme polynomial destiné à répondre à des requêtes simples sur des bases de connaissances en DL-Lite possibiliste quantitatif (conférence IEA/AIE 2016).

Une autre partie des travaux réalisés s’inscrit également dans le cadre du projet AMADEUS « Vers la fusion de croyances efficace » No 24144UC projet bilatéral franco-autrichien LSIS-LIF-TUW (2013-2014) et dont nous avons assuré la coordination (Odile PAPINI coordinatrice). Il impliquait également Raida KTARI. En collaboration avec N. Creignou, R. Pichler, S. Rümmele, S. Woltran (membres du projet AMADEUS), Raida KTARI (dans le cadre de sa thèse) et Odile PAPINI ont étudié le changement de croyances dans le cadre de fragments propositionnels qui permettent des procédures efficaces de raisonnement. En effet, lorsque les croyances d’un agent sont représentées dans un fragment de la logique propositionnelle il n’est pas garanti que le résultat d’une opération de changement de croyances reste dans le fragment considéré. La plupart des travaux se sont concentrés sur le fragment de Horn et ont porté principalement sur la contraction de croyances. Elles ont proposé une approche qui repose sur le raffinement d’opérateurs sémantiques de changement de croyances connus afin qu’ils opèrent sur les fragments propositionnels. Elles ont donné une caractérisation des raffinements et ont étudié leurs propriétés logiques en termes de satisfaction des postulats pour différents opérateurs de révision (conférence KR 2012 puis revue JCSS 2014), de fusion (conférence ECAI 2014 puis revue ACM TCL 2016), de mise à jour (conférence ECSQARU 2015) et de contraction. L’ approche proposée ne se limite pas au fragment de Horn mais s’applique à tout fragment de la logique propositionnelle caractérisable par une propriété de clôture des ensembles de modèles du fragment considéré.

Belaïd BENHAMOU et Pierre SIEGEL (LIF) se sont intéressés à la sémantique des modèles stables et des ensembles réponses en programmation logique (ASP). Ils ont introduit une nouvelle sémantique pour les programmes logiques généraux (incluant la négation par échec) qui capture la sémantique des modèles stables introduite par Gelfond et Lifshitz en 1988. Ils ont défini une notion d’extension pour les programmes logiques généraux, et ils ont montré que chaque modèle stable au sens de cette sémantique est impliqué par une des extensions de la nouvelles forme logique de ce programme. Ils ont montré que l’ensemble des modèles stables d’un programme logique est en bijection avec un sous ensemble de l’ensemble des extensions dans la nouvelle sémantique. De ce fait, cette nouvelle sémantique peut être vue comme une extension pour la sémantique des modèles stables. Elle a aussi l’avantage de simplifier les méthodes de recherche de modèles stables en programmation logique. Une méthode basée sur cette nouvelle sémantique pour le calcul des extensions a été introduite. L’ensemble des modèles stables du programme logique peut être déduit à partir de ces extensions avec de bonnes propriétés de complexité. Les premiers résultats sont publiés à la conférence ICTAI 2012. Dans un autre travail, Belaïd BENHAMOU a étudié la notion de symétrie dans le cadre des modèles stables et des ensembles réponses au niveau de l’ASP. Il a montré comment détecter et éliminer les symétries globales et locales dans les méthodes de calcul de modèles stables (conférence LPAR 2013).

Argumentation

Dans les systèmes d’argumentation abstraits de Dung, seule l’interaction négative entre arguments est prise en compte à travers une relation d’attaque. Dans le cadre des travaux qui ont été réalisés pour étendre ce modèle, et afin de tenir compte également d’interactions positives à travers une relation de support, Farid NOUIOUA et Vincent RISCH ont proposé les Cadres d’Argumentation avec Nécessité (CANs) (conférence SUM 2011), une extension bipolaire des cadres d’argumentation de Dung (CA) où la relation de support a le sens particulier de nécessité (l’acceptation d’un argument est nécessaire pour l’acceptation d’un autre argument). L’utilisation de ce sens particulier de la relation de support permet de bien maîtriser l’interaction entre les relations de support et d’attaque, de généraliser d’une façon élégante les résultats obtenus pour les CAs de Dung au nouveau cadre bipolaire, d’établir des liens forts avec d’autres formalismes logiques de raisonnement non-monotones. Ce premier travail a été ensuite poursuivi par une étude approfondie des CANs. Farid NOUIOUA a proposé un approfondissement de ce travail qui consistait à couvrir les principales sémantiques d’acceptabilité, à caractériser ces sémantiques en termes d’étiquetages et de proposer des de nouveaux algorithmes d’étiquetage adaptés au nouveau cadre bipolaire (conférence SUM 2013). Le traitement des préférences dans les CAN a donné naissance à une première approche proposée par Imane Boudhar (stage de master), Farid NOUIOUA et Vincent RISCH (conférence ICAART 2012) et une seconde approche proposée par Farid NOUIOUA (conférence SUM 2012) basée sur une représentation axiomatique des sémantiques d’acceptabilité en présence de préférences. Farid NOUIOUA et Vincent RISCH ont étudié les liens entre les CANs et deux autres formalismes de raisonnement non monotone, à savoir les théories de défauts et les programmes logiques (conf érence ICAART 2012). Enfin, Farid NOUIOUA et Sara Boutouhami ont étudié les preuves dialectiques dans les CANs permettant de décider de l’acceptabilité sous la sémantique de base (grounded semantics) et de l’acceptabilité crédule sous la sémantique préférée (conférence ECSQARU 2015).

La dynamique des systèmes argumentatifs est un sujet actif des dix dernières années. Les principaux travaux ont jusqu’ici porté essentiellement sur deux axes : l’analyse du contenu des extensions des systèmes argumentatifs lors de l’arrivée de nouveaux arguments d’une part, et la définition d’opérateurs de révision s’appuyant sur le support logique des arguments. F. Nouiua et É. Würbel ont pour leur part choisi d’étudier le développement d’opérateurs de changement s’appuyant sur des cadres argumentatifs abstraits. Dans un premier temps, ils se sont intéressés à un opérateur de révision s’appliquant aux cadres argumentatifs abstraits de Dung. L’idée de ce premier travail est de considérer la proximité entre cadres argumentatifs abstraits munis de la sémantique d’acceptabilité des extensions stables et programmation logique avec sémantique des modèles stables. Cela les a conduit à proposer un opérateur de révision d’essence syntaxique, permettant de réviser un cadre argumentatif abstrait par un ensemble de relations d’attaque, en considérant comme sémantique d’acceptabilité la sémantique stable. Dans ce contexte, réviser un cadre argumentatif revient à restaurer la cohérence (comprise au sens de l’absence d’extensions stables) qui peut être perdue à l’arrivée des nouvelles relations d’attaque. Par ailleurs, ce travail les a amenés à adapter les postulats de la révision dans un cadre logique syntaxique (Fallappa & al), et à proposer ainsi un ensemble de postulats adaptés à la révision de cadres argumentatifs (conférence ICTAI 2014). Ce premier travail est en cours de développement selon plusieurs axes : cadres argumentatifs bipolaires, application à la révision de programmes logiques avec sémantique des modèles stables, extension à d’autres sémantiques des cadres argumentatifs.

Contrairement aux autres travaux en argumentation décrits précisément et qui se situent au niveau de l’argumentation abstraite, le travail décrit ici s’intéresse à l’argumentation structurée. Plus précisément, Farid NOUIOUA et Leila Amgoud se sont intéressé aux systèmes d’argumentation à base de règles. Ces systèmes d’argumentation sont construits à partir de bases de connaissances formées de faits, de règles strictes et de règles défaisables. D’une part, ils ont montré que parmi les divers types de relations d’attaques proposées dans la littérature, la relation "undercut" est suffisante pour capter les différents conflits présents dans une base de connaissance. D’autre part, ils ont proposé une caractérisation complète des résultats d’un système à base de règles sous différentes sémantiques d’acceptabilité (conférence SUM 2015).

Vincent RISCH a défini un calcul destiné à représenter la dynamique d’un agent formel raisonnant sur ses propres attitudes ou celles d’un interlocuteur, comme préliminaire à la construction de nouveaux arguments dans un cadre logique issu des X–logiques (une extension non–monotone de la logique propositionnelle). A partir du caractère paraconsistant de ces logiques, quatre attitudes sont distinguées qui peuvent à leur tour être interprétées comme les valeurs de vérité d’une logique multivaluée. Elles permettent donc la définition d’une matrice non–déterministe à partir de laquelle est produit un calcul de type n–séquents. La réduction à un calcul de séquents classiques LA (pour "Logique des Attitudes") est réalisée suivant la méthode proposée par (Avron, Ben-Naim, Konikowska). Surtout, il est établi que la logique MSPL ("Most geneneral Source-Processor Logic) de ces auteurs se présente comme un cas particulier de la logique LA, à son tour issu d’une caractérisation cumulative des X-logiques.

Enfin, dans la conférence SUM 2011), Safa YAHI a comparé l’inférence argumentative justifiée avec les inférences basées sur la restauration de la cohérence les plus fréquemment utilisées et ce en terme de productivité. Safa YAHI et Karima Sedki ont proposé une extension des systèmes d’argumentation basés sur les valeurs en considérant des contraintes (conférence IPMU 2016).

Méthodes de déduction pour les logiques des conditionnels et similaires

Il faut rappeler ici que les logiques des conditionnels ont été étudiées depuis les années 1970 pour la formalisation du raisonnement contre-factuel, du changement des croyances (révision), du raisonnement plausible (tolérant exceptions, non-monotone) et du raisonnement causal. Cependant le développement des méthodes de preuve pour ces logiques n’a pas atteint celui d’autres formalismes logiques utilisés en IA et dans la représentation des connaissances. Une partie de l’activité de recherche s’est concentrée sur l’étude des méthodes de déduction pour ces logiques. Récemment en collaboration avec G.L. Pozzato (U. Turin), Nicola OLIVETTI a étudié des calculs des séquents imbriqués pour les logiques des conditionnels. Ces calculs fournissent des méthodes de déduction standard, optimaux et internes pour les logiques des conditionnels de base (conférence JELIA 2012 puis revue JLC 2016-). Ces calculs ont été implémentés dans le démonstrateur NESCOND (conférence IJCAR 2014), dont les performances sont à ce jour les meilleures parmi celles des démonstrateurs connus pour ces logiques. On a proposé ultérieurement (en collaboration avec G.L. Pozzato) un nouveau type de calcul des séquents interne et standard pour la logique des contre-factuels fondamentale de Lewis V (conférence TABLEAUX 2015). Enfin, nous avons proposé en collaboration avec S. Negri, (U. Helsinki) un calcul externe (avec labels) pour la logique préférentielle des conditionnels basée sur une nouvelle sémantique topologique affaiblie (« Neighbourhoods Models ») (conférence TABLEAUX 2015). Le développement de ces calculs rentre aussi dans les objectifs du projet international ANR PRCI TICAMORE et constitue une des thématiques de la thèse de Marianna GIRLANDO débutée en octobre 2015. Lié à cette thématique, l’étude de la logique de la Similarité Comparative des Concepts introduite par Wolter, et als. dont la sémantique basée sur des modèles avec une fonction de distance est un cas particulier de la sémantique des logiques des conditionnels (thèse de Régis ALENDA) : nous avons étudié l’équivalence avec la sémantique préférentielle, son axiomatisation et des méthodes de décision à tableaux (conférences TABLEAUX 2011 et JELIA 2012).

Raisonnement non-monotone appliqué aux logiques de descriptions

Les logiques de descriptions sont à la base des langages des ontologies utilisés dans le Web Sémantique,notamment du langage/standard OWL. Un problème significatif dans les ontologies est celui de représenter des propriétés prototypiques admettant des exceptions et leur héritage dans une taxonomie de concepts. Ce problème rentre dans la thématique du raisonnement non-monotone, mais l’application des formalismes non-monotones les plus connus aux logiques de descriptions soulève à la fois des difficultés sémantiques et computationnelles. Nicola OLIVETTI a étudié l’application des logiques non-monotones de Kraus Lehmann Magidor (KLM) aux logiques de descriptions. En collaboration avec L. Giordano, V. Gliozzi et G.L. Pozzato (U. de Turin et U. du Piémont Oriental), il a proposé une extension des logiques de descriptions basée sur l’introduction d’un opérateur non-monotone de « typicalité » qui sélectionne les instances typiques d’une classe (revue Artificial Intelligence 2013). Ils ont obtenu différents résultats computationnels concernant notamment l’intégration de l’opérateur de typicalité dans les logiques de descriptions à faible complexité (DL light), (conférences IJCAI 2011 et TABLEAUX 2011). Plus récemment, Nicola OLIVETTI a proposé une sémantique alternative non-monotone basée sur la notion de Rational Closure qui se révèle être plus naturelle et plus avantageuse d’un point de vue computationnel (conférences JELIA 2012 et DL 2014, puis revue Artificial Intelligence 2015). La poursuite de ces travaux devrait porter sur l’étude de l’impact en termes de complexité de cette nouvelle sémantique avec différentes logiques de description (de DL Light à SHOIQ(D) = OWL).


Les recherches développées ici portent principalement sur la résolution du problème général de la satisfiabilité (SAT) et des problèmes de satisfaction de contraintes (au sens CSP à domaines finis qui est une extension de SAT), et leurs extensions à l’optimisation, avec Max-SAT (qui consiste à maximiser le nombre de clauses satisfiables) d’une part, et les CSP Pondérés d’autre part (pondération sur les contraintes), voire au dénombrement (#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 et en pratique. Ils ont au-delà des retombées dans de nombreux domaines d’applications. Si le thème central des recherches développées ici concerne l’algorithmique des problèmes de satisfaction de contraintes, on peut cependant évoquer deux autres domaines abordés. D’une part la Théorie de Graphes dans la mesure où nos travaux s’appuient très souvent sur les propriétés graphiques associés à l’expression des CSP sous la forme de "réseaux de contraintes" (ce sont des (hyper)graphes étiquetés). D’autre part, la Théorie de la Complexité au niveau de la mise en évidence de nouvelles classes polynomiales, c’est-à-dire d’ensembles infinis d’instances dont la reconnaissance et la résolution admettent des algorithmes de complexité polynomiale.

Une partie conséquente des travaux réalisés depuis 2011 s’inscrit dans le cadre du projet ANR Blanc TUPLES (http://www.lsis.org/tuples/) qui a débuté en octobre 2010, qui a duré 4 ans et demi, que nous avons initié et dont nous avons assuré la coordination nationale (P. Jégou était coordinateur national du projet). Ce projet était centré sur la résolution effective de problèmes NP-Complets, en particulier de problèmes relevant de l’Intelligence Artificielle. Le projet TUPLES abordait cette question par le biais du développement et de l’exploitation de classes polynomiales ainsi qu’en les envisageant comme outils d’analyse pour expliquer l’efficacité relative des solveurs. Cette étude centrée sur l’Intelligence Artificielle, s’est en particulier intéressée aux problèmes génériques que sont SAT et CSP.

Polynomialité et résolution fondées sur des propriétés de graphes

L’un des premiers résultats obtenus porte sur une nouvelle analyse de la complexité des algorithmes usuels de la programmation par contraintes (algorithmes d’exploration arborescente avec filtrages par propagation tels que FC, RFL, etc…). Cette analyse a permis à Achref EL MOUELHI, P. Jégou et Cyril TERRIOUX, en collaboration avec B. Zanuttinni (membre du projet ANR TUPLES), de mettre en évidence de nouvelles classes polynomiales fondées sur des classes de graphes tels que les graphes planaires ou les graphes toroïdaux (conférences ISAIM 2012 puis CPAIOR 2013). Outre la mise en évidence de nouvelles classes polynomiales, l’originalité de ces résultats est d’avoir montré que les algorithmes usuels de l’état de l’art sont en mesure de résoudre très efficacement en pratique, mais aussi en théorie, des instances du fait de leur appartenance à des classes polynomiales. Un autre champ de travaux, portait sur l’étude des méthodes de résolution de réseaux de contraintes basées sur la notion de décomposition arborescente de graphes (notion introduite par Robertson et Seymour dans les années 1980). P. Jégou et Cyril TERRIOUX ont poursuivi leurs travaux autour des méthodes hybridant recherche arborescente et programmation dynamique. Ils ont d’abord montré comment il était possible, en intégrant des techniques de redémarrage, dont on connaît la pertinence au niveau de la résolution pratique de SAT, d’améliorer très significativement les techniques de résolution exploitant la décomposition de graphes (conférence ECAI 2014. Sur un autre plan, ils ont mis en évidence une nouvelle classe de décomposition de graphes appelée « Bag-Connected-Tree-Decompostion » et l’invariant associé (« Bag-Connected-Tree-Width ») (conférence CP 2014). Ils ont montré l’intérêt de l’exploitation algorithmique de ces objets combinatoires, qui d’ailleurs ont été « découverts » et étudiés au même moment dans la communauté mathématique de la Théorie des Graphes, mais cette fois-ci, sur un plan purement combinatoire et non algorithmique. Plus récemment, dans le cadre de la thèse de Hanan KANSO, des travaux portant sur la conception d’algorithmes de décomposition qui prennent en compte des critères plus pertinents pour la résolution de CSP ont été entrepris (conférence ICTAI 2015). Ce travail a été étendu de sorte à rendre possible la manipulation dynamique de décompositions arborescentes pendant la résolution (conférence CP 2016).

Classes polynomiales et microstructure

Un autre champ de travaux a porté sur l’exploitations de la « microstructure » des CSP. Cet objet formel permet, à l’opposé des approches de type décomposition, de capter des propriétés liées non plus à la structure, mais à la sémantiques des instances. Nous avons focalisé notre étude sur l’extension de la propriété BTP (pour « Broken Triangle Property ») introduite par P. Jeavons et A. Salamon de l’Université d’Oxford et Martin C. Cooper l’Université de Toulouse (et membre du projet ANR TUPLES). L’intérêt de cette propriété est qu’elle définit une classe polynomiale directement exploitable par les solveurs de l’état de l’art (avec des algorithmes tels que RFL ou MAC qui sont au coeur des solveurs). Un premier travail avait pour objet de généraliser cette approche aux contraintes d’arité quelconque, plus à même d’avoir un impact sur la résolution pratique de problèmes, à l’opposé des seules contraintes binaires pour lesquelles BTP a été introduite. Ce travail qui était au cœur de la thèse d’Achref EL MOUELHI, a été publié en revue (revue Constraints 2015). Une autre voie visant à généraliser BTP a eu pour objet de relaxer la propriété BTP tout en conservant une garantie de polynomialité. Cette approche qui a pour vertu essentielle d’étendre le champ des instances désormais traitables en temps polynomial, a permis à P. Jégou et Cyril TERRIOUX de mettre en évidence une nouvelle classe polynomiale appelée ETP qui généralise la classe BTP (conférence AAAI 2015). Il a été suivi par une extension paramétrée présentée à la conférence CP 2015, en collaboration avec M. Cooper, qui permettait notamment de répondre à une question posée par Moshe Vardi sur les relations entre classes « structurelles » au sens de la décomposition arborescente, et classes « sémantiques » au sens de BTP. Parmi les résultats les plus marquants, Achref EL MOUELHI et Cyril TERRIOUX (avec M. Cooper et B. Zanuttinni) ont étudié, toujours dans le cadre de la classe BTP, la notion de fusion de valeurs. Cette approche permet, en exploitant des propriétés locales, de réduire les domaines des variables, et ainsi, d’étendre le puissance de résolution offerte par cette classe polynomiale. Ces travaux ont obtenus le « Award du Best Technical Paper » lors de la conférence CP 2014, et se sont poursuivis avec notamment une communication à la conférence IJCAI 2016. Enfin, une première extension de ces travaux a été publiée dans la revue Artificial Intelligence 2016. De nouveaux développements fondés sur le même type d’approche mais relâchant la propriété BTP ont été présentés à la conférence CP 2016.

Problème SAT

Les travaux relatifs au problème SAT ont porté à la fois sur les méthodes complètes et les méthodes incomplètes. Ces dernières années, les méthodes de résolution complètes basées sur la notion de CDCL (Conflict Driven Clause Learning) ont montré une très grande efficacité pour résoudre de nombreuses instances structurées faisant intervenir des milliers, voire des millions de variables et de clauses. Ces solveurs dits « modernes », sont une combinaison à la fois subtile et sensible de plusieurs composants comme l’apprentissage de clauses, la propagation, les retours-arrières non-chronologiques, les redémarrages, etc. Toutefois, la littérature sur ces méthodes ne fournit pas assez d’explications à cette efficacité. Afin de contribuer à la compréhension des CDCL, Djamal HABET et D. Toumi (dans le cadre sa thèse) ont proposé une étude empirique approfondie d’un module essentiel qui est celui de l’analyse des conflits. Cette étude évaluait l’influence des caractéristiques des conflits analysés (exprimés par la falsification de clauses) sur la qualité des clauses apprises qui forment des nogoods. Il a été montré que ces clauses sont très importantes car elles permettent notamment un meilleur élagage de l’espace de recherche et déterminent les retours-arrières non-chronologiques à effectuer (conférence CP 2013).

Par ailleurs, les méthodes incomplètes pour SAT sont basées sur la recherche locale. Elles sont notamment réputées très efficaces dans la résolution des instances aléatoires. A. Abramé, Djamal HABET et D. Toumi ont proposé Ncca+, un solveur basé sur un algorithme de recherche locale qui tente d’équilibrer finement deux phases de résolution  : la diversification et l’intensification (conférence ISAIM 2014). Le solveur Ncca+ a obtenu une médaille de bronze lors la compétition internationale SAT 2013 dans le resgistre « Random Satisfiable Track » et l’extension de ces travaux a été publiée dans en revue AMAI 2016.

Problème Max-SAT et optimisation

Une autre part importante des travaux s’est intéressée au problème Max-SAT (et ses variantes pondérées). Dans ce cadre, les méthodes de type séparation et évaluation pour Max-SAT ont montré une grande efficacité de résolution, principalement sur les instances aléatoires. Le calcul de la borne inférieure est primordial pour ces méthodes. Il consiste à sous-estimer le nombre de sous-ensembles inconsistants disjoints détectés principalement par la propagation unitaire simulée. Ils sont ensuite transformés pour s’assurer qu’ils ne soient comptabilisés qu’une seule fois. Une des méthodes de transformation est la règle d’inférence dite de « max-résolution ». Elle permet de conserver l’équivalence de la formule tout en isolant les inconsistances, réalisant ainsi une forme d’apprentissage (au sens des solveurs SAT). Toutefois, cette règle augmente considérablement la taille de la formule par l’ajout de « clauses de compensation ». Cela rend son usage systématique inefficace. Ainsi, son application est réduite à certains motifs particuliers des sous-ensembles inconsistants. Dans ce cadre, A. Abramé (dans le cadre de sa thèse) et Djamal HABET ont mis en évidence le fait que la max-résolution impacte la puissance de propagation unitaire simulée et donc la qualité de la borne inférieure. Cela les a conduit à définir la notion de l’UP-résilience (conférence IJCAI 2015) qui est une caractérisation formelle de la relation entre cette règle d’inférence et la capacité de la propagation unitaire simulée à détecter des sous-ensembles inconsistants. L’UP-résilience a permis aussi d’apporter une explication théorique à l’efficacité des formes d’apprentissage correspondant à certains motifs. Par ailleurs, la règle de la max-résolution ajoute à la formule des clauses dont le nombre et la taille dépendent des clauses en entrée. Un nouvel ordre d’application de cette règle sur les clauses des sous-ensembles inconsistants a été proposé . Il est basé sur les caractéristiques des résolvantes intermédiaires produites (durant des années, un seul schéma a été utilisé basé sur l’ordre inverse des propagations) afin de limiter l’augmentation de la taille de la formule. A. Abramé et Djamal HABET ont validé empiriquement cet ordre avec une consolidation théorique de son intérêt et ont proposé une meilleure exploitation de la max-résolution localement à chaque nœud de l’arbre de recherche pour améliorer la qualité de l’estimation de la borne inférieure (conférence CP 2014). Durant ces travaux, ils ont également développé le solveur ahmaxsat (revue JSAT 2015) qui s’est distingué lors des « Max-SAT International Evaluation » 2014, 2015 et 2016, où ce solveur a été classé premier dans trois des neufs catégories d’instances dans chacune des trois éditions, remportant ainsi 9 médailles d’or au total.

Dans le cadre d’une collaboration avec l’équipe du Pr. Dalila BOUGHACI du Laboratoire de Recherche en Intelligence Artificielle (LRIA) de l’Université USTHB d’Alger, Belaïd BENHAMOU s’est intéressé via des approches hyper-heuristiques à la résolution de certains problèmes d’optimisation combinatoire comme Max-SAT et le problème d’assignation de fréquences (MI-FAP) dans les réseaux de téléphonie mobile. Ces travaux, rentrent dans le cadre de deux thèses en co-direction avec l’Université d’Alger. Un autre travail dans le cadre d’une thèse en co-encadrement avec l’ESI d’Alger consiste en l’optimisation de tâches dans les systèmes de production. Les premiers résultats on été reconnus par les publications (conférences MIC 2015 et META 2014).

Toujours dans le cadre des problèmes d’optimisation combinatoire, Farid NOUIOUA s’est intéressé au développement de méthodes fondées sur des approches « bio-inspirées » qui utilisent une représentation quantique des solutions potentielles. Il a notamment proposé l’algorithme QIFAPSO qui hybride deux méthodes bio-inspirés : l’algorithme « firefly » et l’optimisation par essaims de particules tout en s’appuyant sur une représentation quantique des solutions. Il a appliqué QIFAPSO sur le problème de sac à dos multi-dimentionnels et obtenu de très bons résultats. Ce travail qui se poursuit en l’orientant vers le contexte du Data Mining a été publié en revue (Soft Computing 2016).

Autres approches et problèmes connexes

La communauté CSP a remarqué que la généralisation des algorithmes de résolution connus pour les CSP binaires aux CSPs n-aires (contraintes d’arité quelconque) n’est pas une chose facile et est de fait un des verrous de ce domaine. Lionel PARIS et Belaïd BENHAMOU, avec Pierre SIEGEL du LIF, ont étudié un cadre théorique logique généralisant la forme CNF et qui exprime naturellement les CSPs n-aires. Ce cadre a permis de retrouver des outils de résolution efficaces pour Les CSP n-aires donnant ainsi une nouvelle solution alternative. Entre autres, ce travail est reconnu par la publication d’un article dans la Journal of Automated Reasoning.

Parmi les domaines connexes, en relation avec SAT (selon l’approche considérée) et l’optimisation, Stéphane GRANDCOLAS a poursuivi ses travaux sur les problèmes de packing en deux dimensions qui sont des problèmes classiques dans le domaine de l’optimisation combinatoire. Il s’est intéressé au problème de packing orthogonal (déterminer si un ensemble d’objets rectangulaires donné peuvent être placés à l’intérieur d’une boîte rectangulaire sans qu’il y ait de chevauchements), et au problème de strip packing (placer un ensemble d’objets rectangulaires dans une bande de largeur donnée sans qu’il y ait de chevauchements et en minimisant la hauteur occupée dans la bande). Stéphane GRANDCOLAS a proposé (1) une approche utilisant des solveurs SAT (le problème de packing est modélisé par une formule clausale), (2) une méthode exacte de type branch and bound qui s’est avérée très performante, qui fait appel à des techniques d’élimination de configurations équivalentes et de mémorisation de configurations sans intérêt (assimilables à des nogoods), et enfin (3) une métaheuristique originale basée sur de la recherche locale pour le calcul des positions des objets sur l’axe horizontal et sur l’axe vertical. Si les travaux sont en cours pour ce dernier point, les résultats obtenus ont été publiés dans le Journal of Math. Modelling and Algorithms in O.R. 2015 et un solveur est mis à disposition de la communauté.

Belaïd BENHAMOU (en 2013-2014, pendant une délégation CNRS au Laboratoire CRIL de l’Université d’Artois à Lens) a travaillé avec le groupe de Lakhdar Saïs sur les problèmes de fouille de données en utilisant l’approche contraintes. Contrairement aux approches connues dans ce domaine, cette approche récente (Deraedt et al . 2008) est déclarative et fournie un cadre générique pour résoudre des problèmes de Data Mining divers et variés. L’objectif est d’utiliser la force des formalismes déclaratifs de la CP, SAT ou des ASP ainsi que les outils de résolutions associés pour exprimer et résoudre les problèmes de data mining, clustering ou de classification. En collaboration avec le CRIL, Belaïd BENHAMOU a proposé l’introduction d’encodages déclaratifs pour le problème d’Itemset mining et l’étude de la notion de symétrie pour sa résolution. Les premiers travaux ont été publiés dans la conférence KDIR 2014 (une version plus étendue a été publiée dans un chapitre de livre (KDIR & IC3K 2014 Selected Papers 2015) et un article plus élaboré du travail a été présenté à la conférence AISC 2014.


Les activités de l’équipe ont conduit à la conception et la production de plusieurs logiciels qui sont mis à disposition de la communauté. Aucun de ceux-ci n’a fait l’objet d’une déclaration de licence.

2013. « Ncca+ » : un démonstrateur de recherche locale pour SAT conçu et développé par André Abramé, Djamal HABET et Donia Toumi. Téléchargeable publiquement depuis :
http://satcompetition.org/edacc/SATCompetition2013/experiment/23/solver-configurations/889

2014. « NESCOND » : (Nested Sequent calculi for normal conditional logics) un démonstrateur qui implémente les calculs à séquents imbriqués et qui est actuellement le plus efficace pour les logiques des conditionnels de base. Conçu et développé par Nicola OLIVETTI et Gian Luca Pozzato (Università di Torino, Italie). Accessible en ligne depuis : http://www.di.unito.it/~pozzato/nescond/

2014 et 2015. « ahmaxat » : un démonstrateur séparation et évaluation pour Max-SAT conçu et développé par André Abramé et Djamal HABET. Téléchargeable publiquement depuis : http://www.lsis.org/habetd/Djamal_Habet/MaxSAT.html

2015. « PackSolver » : (an exact algorithm for Orthogonal Packing Problems). Conçu et réalisé par Stéphane GRANDCOLAS. Solveur traitant certains problèmes de packing. Téléchargeable publiquement à l’adresse :
http://www.dil.univ-mrs.fr/~gcolas/pack-solver.html