Contexte

Les problèmes de satisfaction de contraintes (CSP) [Lec13] fournissent un cadre puissant permettant de représenter et résoudre de nombreux problèmes de nature combinatoire (planification, ordonnancement, configuration…). Lorsque un problème CSP est cohérent, on obtient alors une solution facilement exploitable. Au contraire, lorsqu’un problème CSP est incohérent, il est plus difficile d’expliquer la raison de cette incohérence [HLSB06, GMP07, GLM14]. Malgré tout, ces explications sont importantes car elles peuvent aider l’utilisateur à comprendre les raisons de l’incohérence de la formule. Le but de ce stage est de commencer à étudier un nouveau type d’explication d’incohérence au travers du concept de « weak core ». A noter que ce sujet fera l’objet d’un financement pour des travaux de thèse.

Sujet

Ce travail se situe dans le cadre de l’intelligence artificielle explicable. L’objectif est de pouvoir expliquer à un utilisateur pourquoi un réseau de contraintes est insatisfiable, où qu’il ne possède pas toutes les solutions attendues. Quand le réseau est insatisfiable, une technique bien connue pour fournir cette explication est d’identifier un MUC (sous-ensemble incohérent minimal). Malheureusement, les MUC sont inexploitables pour un utilisateur s’ils sont soit trop gros, soit trop longs à obtenir, soit lorsque le réseau est satisfiable. La notion de weak core permet de généraliser la notion de MUC pour permettre d’obtenir selon les cas une explication partielle, ou une explication de l’absence de certaines solutions. Un weak core est un (petit) ensemble de contraintes qui est cohérent, tout en admettant un faible nombre de solutions. L’idée est d’identifier des sous-parties de problèmes (réseaux) très contraintes, dont la taille est suffisamment petite pour rester exploitable. Un weak core peut être défini comme un sous-ensemble de contraintes ayant au plus soit un nombre fixe de solutions soit une proportion fixe de solutions. Identifier des weak cores est clairement un problème d’optimisation bi-critère, où un équilibre doit être trouvé entre la taille des weak cores et leurs nombres de solutions.

Nous pensons que l’identification de petits weak cores peut permettre à l’utilisateur de mieux comprendre la raison d’une incohérence globale par rapport à un sous-ensemble incohérent minimal (MUC) de grande taille. A titre d’exemple, si un problème incohérent admet un petit weak core comportant seulement 10 solutions, il peut être facile pour l’utilisateur de comprendre les raisons pour lesquelles ce noyau est presque incohérent, et de vérifier à la main que les 10 solutions restantes ne peuvent pas être étendues globalement. Ce processus est similaire à un schéma de preuve dans lequel un cas général est tout d’abord identifié puis des cas spécifiques explorés.

De manière à être pertinents pour l’utilisateur, les weak cores devraient correspondre à un cluster de contraintes qui sont liées sémantiquement (par contraste avec des sous-ensembles de contraintes prises plus ou moins aléatoirement). Cela peut être assuré en demandant soit de minimiser le nombre de variables dans les noyaux, soit d’étiqueter avec le même label les contraintes liées sémantiquement et de minimiser le nombre de labels différents dans les weak cores. Identifier des weak cores est clairement difficile du point de vue calculatoire (plus difficile que de trouver des MUCs), mais le problème pourrait parfois se révéler plus facile en pratique que de prouver l’incohérence. Quand un problème est difficile, prouver l’incohérence peut nécessiter des années de temps de calcul. Identifier des weak cores intéressants est vraisemblablement encore plus difficile (et coûteux), mais approximer des weak cores peut sans doute être effectué efficacement car cela ne nécessite pas d’explorer totalement l’espace de recherche. Par conséquent, les weak cores peuvent être perçus comme un palliatif quand l’incohérence ne peut être prouvée. Si ces noyaux sont suffisamment petits, ils peuvent être utiles à l’utilisateur. S’ils sont gros, ils peuvent être traités et convertis en lemmes qui peuvent aider à prouver l’incohérence.

Un autre usage des weak cores est d’aider à identifier pourquoi le réseau ne possède pas autant de solutions qu’on pourrait l’espérer. Par exemple, pour le problème de construction d’un emploi du temps, si l’utilisateur obtient des solutions mais qu’elles ne sont pas satisfaisantes, la recherche de weak cores permettra d’identifier le sous ensemble le plus contraint et qui élimine les solutions que l’on souhaiterait avoir. Illustration sur un exemple : quand il faut construire un emploi du temps, la disponibilité des intervenants figure parmi les contraintes majeures. Si un intervenant donne des disponibilités trop limitées, cela peut amener à placer les autres intervenants de manière moins satisfaisante, voire à ne plus avoir de solution. On peut par exemple se retrouver dans une situation où il n’y a pas de solution, mais le MUC l’expliquant contient toutes les contraintes de disponibilité, ce qui n’aide guère à résoudre le problème. Dans ce cas, un weak core devra contenir les quelques disponibilités qui contraignent le plus le problème et qu’on cherchera à modifier. Dans d’autres circonstances, on peut effectivement obtenir des solutions mais qui ne sont pas satisfaisantes (par exemple parce qu’il y a de nombreux trous). On ne peut chercher un MUC dans ce cas, mais là encore un weak core permettra d’identifier le cœur du problème.

References

[BHvM09] Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009. Hans Kleine Büning and Oliver Kullmann. Handbook of satisfiability, chapter 11: Minimal Unsatisfia- bility and Autarkies. Volume 185 of [BHvM09], 2009.

[BK09] Bart Selman Carla P. Gomes, Ashish Sabharwal. Handbook of satisfiability, chapter 20: Model Counting. Volume 185 of [BHvM09], 2009.

[GLM14] Eric Grégoire, Jean-Marie Lagniez, and Bertrand Mazure. Boosting MUC extraction in unsatisfiable constraint networks. Appl. Intell., 41(4):1012–1023, 2014.

[CPG09][GMP07] Eric Grégoire, Bertrand Mazure, and Ce ́dric Piette. MUST: provide a finer-grained explanation of un- satisfiability. In Principles and Practice of Constraint Programming - CP, Proceedings, pages 317–331, 2007.

[HLSB06] Fred Hemery, Christophe Lecoutre, Lakhdar Sais, and Frédéric Boussemart. Extracting mucs from con- straint networks. In ECAI 2006, 17th European Conference on Artificial Intelligence, Proceedings, pages 113–117, 2006.

[Lec13] Christophe Lecoutre. Constraint Networks: Targeting Simplicity for Techniques and Algorithms. John Wiley & Sons, 2013.