2019-12-11 • salle des thèses, Faculté des sciences Jean Perrin

Résumé

Devant nous se dresse la montagne PSPACE, la route vers son sommet (les problèmes PSPACE-complets) est jonchée de problèmes dont la difficulté va croissant. Après avoir quitté le départ, la pente est tout de suite raide : tous les problèmes rencontrés sont NP-difficiles. Nul ne sait aujourd’hui prouver qu’il existe (ou pas) des algorithmes de résolution efficaces (c’est-à-dire en temps polynomial) pour de tels problèmes et tous les algorithmes existants à ce jour requièrent un temps d’exécution exponentiel dans le pire des cas.

Parmi les problèmes NP-difficiles, les plus faciles à résoudre en pratique sont les problèmes NP-complets. Le problème SAT (décider la satisfaisabilité d’une formule propositionnelle) est l’un d’entre eux. Il fait depuis longtemps l’objet d’une attention toute particulière, qui a conduit à l’avènement des solveurs SAT dits « modernes » au début de notre millénaire. Ces solveurs sont capables actuellement de résoudre en pratique de nombreux problèmes industriels.

Cette présentation décrit notre ascension vers le sommet de la montagne PSPACE en utilisant de tels solveurs comme piolets. Il retrace d’abord nos contributions quant à la résolution pratique de SAT (on affûte les piolets !). Il explique ensuite comment utiliser les piolets pour résoudre en pratique des problèmes de plus en plus durs, comme celui du calcul d’ensembles maximalement cohérents de formules propositionnelles, de la compilation de telles formules et du comptage du nombre de leurs modèles, pour conclure sur la présentation d’un nouveau schéma algorithmique permettant en particulier de décider la satisfaisabilité de formules en logique modale en haut de la montagne PSPACE.

Jury

  • Pierre Marquis - Professeur, CRIL - Université d’Artois
  • Andreas Herzig - Directeur de Recherche, IRIT - CNRS
  • Thomas Schiex - Directeur de Recherche, INRA Toulouse
  • Hélène Fargier - Directeur de Recherche, IRIT - CNRS
  • Philippe Dague - Professeur, Université Paris-Sud
  • Christine Solnon - Professeur, INSA Lyon