logo spi

Dans la résolution de problèmes combinatoires, on peut soit chercher une solution au problème, soit chercher une solution qui optimise un ou plusieurs critères. Dans le cadre d’une recherche d’itinéraire par exemple, on ne cherche généralement pas un trajet allant d’un point à un autre, mais un trajet minimisant la distance, le coût, ou le nombre de changements de direction par exemple. On parle dans le premier cas de résolution de problème de satisfaction, et dans le second cas de problème d’optimisation. Dans le cadre de problèmes combinatoires en variables booléennes, le problème de satisfaction est appelé simplement SAT tandis qu’il existe deux variantes répandues de problèmes d’optimisation : l’optimisation pseudo-Booléenne (PBO) et le problème de satisfiabilité maximale (MAXSAT).

L’une des conséquences de l’omniprésence de traitements automatiques pour aboutir à des décisions qui nous touchent au jour le jour est la nécessité de pouvoir expliquer la solution qui nous est proposée (RGPD). La communauté scientifique a beaucoup travaillé sur l’explication d’absence de solution. Par contre, les travaux sur l’explication de solutions sont beaucoup moins fréquents : on se satisfait généralement de vérifier que la solution apporte bien une solution au problème posé (aller d’un point à un autre). On se pose moins la question de la solution proposée (pourquoi passer par une étape particulière dans un trajet par exemple). On peut dans certains cas transformer ce problème en justification d’absence de solutions : quand la solution est optimale par exemple, on peut justifier qu’il n’est pas possible de faire mieux, quand une valeur est obligatoire, on peut justifier pourquoi on ne peut pas la changer. Cependant, dans un monde dans lequel des algorithmes retournent des solutions sous-optimales pour des raisons d’efficacité, ou une solution parmi de nombreuses solutions équivalentes, il est nécessaire de construire des mécanismes d’explication nouveaux.

L’objectif de cette thèse est de considérer les mécanismes d’explication d’une manière complètement différente de ce qui a été fait jusqu’ici. Depuis longtemps, les justifications sont pensées comme partie intégrante du mécanisme de résolution du problème : les systèmes de maintien de la cohérence de Reiter et De Kleer dans les années 80 [1], les solveurs CSP explicables dans les années 90 [2], etc. L’idée est dans ce cadre de maintenir des explications durant le processus de résolution afin de pouvoir justifier la solution produite. Le problème de cette approche est de lier étroitement le mécanisme d’explication à l’algorithme utilisé [3].

Pendant plusieurs années, la communauté SAT a essayé de vérifier l’absence de solution : une épreuve particulière de la compétition SAT était organisée dès 2005 sur le sujet, sans arriver à motiver les concepteurs des nouveaux solveurs SAT : là aussi, le mécanisme de trace était très simple, indépendant des solveurs, mais demandait beaucoup d’efforts de la part des concepteurs des solveurs pour l’intégrer. C’est un changement de principe qui a permis de changer les choses en 2013 [4] : en utilisant une trace implicite, nécessitant des vérifications plus coûteuses, mais rendant l’intégration de traces beaucoup plus simple pour le concepteur de solveur, tous les solveurs SAT actuels peuvent désormais produire des traces permettant de justifier l’absence de solutions en un temps raisonnable. L’effort de maintenance et d’amélioration du vérificateur de trace est donc centralisé, et bénéficie à tous.

Nous souhaitons répéter cette approche pour l’explication de solutions : permettre aux concepteurs de solveurs PBO et MAXSAT de produire des traces ou d’intégrer des mécanismes simples qui pourraient être utilisés pour expliquer les solutions a posteriori. La bibliothèque Sat4j sera étendue pour permettre la justification de solutions, et vérifier ainsi la difficulté d’intégration de la solution proposée dans un solveur. Nous espérons convaincre d’autres collègues d’adopter cette solution avant la fin de la thèse si celle-ci est conforme à nos attentes.

Une autre approche serait de concevoir un outil totalement découplé des solveurs, permettant d’analyser une solution sans autre information que le problème de départ. Cette approche aurait pour avantage d’être indépendante des solveurs existants et futurs, au prix de ne pas capitaliser sur l’effort de calcul ayant produit la solution.

Quelques références

[1] Raymond Reiter, Johan de Kleer: Foundations of Assumption-based Truth Maintenance Systems: Preliminary Report. AAAI 1987: 183-189

[2] Narendra Jussien. e-constraints: explanation-based constraint programming. In CP01 Workshop on User-Interaction in Constraint Satisfaction, Paphos, Cyprus, 1 December 2001.

[3] Didier Dubois, Daniel Le Berre, Henri Prade, Régis Sabbadin: Using Possibilistic Logic for Modeling Qualitative Decision: ATMS-based Algorithms. Fundam. Inform. 37(1-2): 1-30 (1999)

[4] Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test., Verif. Reliab. 24(8): 593-607 (2014)