Financement : Université d’Artois

Descriptif :

Ces quinze dernières années, des progrès spectaculaires dans le cadre du test de cohérence de formules propositionnelles (SAT) ont permis à une grande variété de problèmes de satisfaction et d’optimisation d’être traités à l’aide d’un moteur de résolution générique, le solveur SAT [1].

Au delà des seuls solveurs SAT, de nombreux cadres utilisant des techniques issues du monde SAT ont pu bénéficier de ces améliorations : on citera par exemple SAT modulo Theories (SMT) [2] ou Answer Set Programming (ASP) [3]. Cependant, il existe encore de nombreux formalismes pour lesquels le test de cohérence ne passe pas à l’échelle. C’est le cas par exemple dès que l’on rajoute des opérateurs modaux dans une formule logique.

Le but de cette thèse est de concevoir un outil de résolution efficace pour tester la cohérence de formules logiques dans le cadre de la logique modale [4], problème que nous appellerons Modal SAT. Une première approche sera d’étudier les diverses façons de réduire le problème Modal SAT à un problème pour lequel il existe des solveurs efficaces en pratique : par exemple SAT[5], SMT[6] ou ASP[7]. Une autre approche sera de concevoir un solveur “ad hoc” pour Modal SAT en adaptant les principes et techniques des meilleurs solveurs cités plus haut.

L’évaluation de solveurs requiert un ensemble varié de benchmarks, idéalement représentant des problèmes Modal SAT réels (par opposition aux problèmes générés aléatoirement ou aux exemples académiques). Un aspect important de la thèse sera de collecter et classer les problèmes Modal SAT disponibles dans la communauté et d’en créer de nouveaux.

On s’intéressera tout particulièrement à la modélisation de jeux avec des aspects épistémiques, c’est à dire des jeux (coopératifs ou non) dont les participants doivent raisonner sur la connaissance que les autres participants ont du jeu. Le résultat de la thèse devrait idéalement permettre la réalisation d’un joueur logiciel capable de participer à ce type de jeu, en utilisant le solveur Modal SAT comme unique moteur de raisonnement.

[1] A. Biere, M. Heule, H. Van Maaren and T. Walsh, Editors : Handbook of Satisfiability. volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, February 2009.

[2] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli : Satisfiability modulo theories. In [1], chapter 26, thesiss 825–885

[3] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Torsten Schaub : Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan & Claypool Publishers 2012

[4] edited by Patrick Blackburn, Johan van Benthem and Frank Wolter, editors : Handbook of Modal Logic. Elsevier. 2007.

[5] Roberto Sebastiani and Michele Vescovi: Automated reasoning in modal and description logics via SAT encoding: the case study of KmALC-satisfiability J. Artif. Int. Res. 35, 1, thesiss 343-389, June 2009

[6] Carlos Areces, Pascal Fontaine, and Stephan Merz : Modal Satisfiability via SMT Solving, Software, Services, and Systems: Festschrift Martin Wirsing. Springer, LNCS 8950, pp. 30-45 (2015).

[7] M. Osorio, and J. A. Navarro Pérez: Answer Set Programming and S4. In IBERAMIA’04: Proceedings of the IX Ibero-American Conference on Artificial Intelligence, number 3315 in Lecture Notes in Computer Science, Puebla, México, November 2004. Springer