Polynomialité pour la Compréhension et l’Extension des Limites des Solveurs Performants – TUPLES

Ce projet a pour ambition de repousser significativement les limites actuellement observées au niveau de l’efficacité pratique des systèmes de résolution (appelés « solveurs ») tout en fournissant les outils théoriques nécessaires à cet objectif. Nous envisageons d’aborder cette question par le biais de l’élaboration et de l’exploitation des classes polynomiales. Cette étude se situera dans le contexte de l’Intelligence Artificielle, plus précisément dans le cadre des formalismes SAT (problème de la Satisfiabilité en logique) et CSP (Problèmes de Satisfaction de Contraintes). D’autres domaines proches de l’IA, comme la Planification seront aussi abordés.

En Théorie de la Complexité, l'étude des classes polynomiales a pour objet de contourner la difficulté de nombreux problèmes rencontrés en informatique (SAT et CSP sont NP-complets) en essayant de dégager des sous-ensembles de jeux de données traitables en temps polynomial. Cette question a fait l'objet de nombreux développements depuis longtemps et dans différents domaines. Deux formalismes ont émergés au cours des dernières décennies, SAT et CSP. Ils ont pour vertus d'être à la fois décidables et suffisamment puissants pour exprimer de nombreux problèmes. Etant NP-Complets, deux démarches ont été adoptées pour les résoudre. D’une part, la réalisation de solveurs dont l'efficacité pratique a permis des passages à l'échelle les rendant souvent opérationnels dans le contexte des applications. D’autre part, une démarche plus théorique visant à restreindre l'expressivité des langages de description des données pour garantir l'existence d'algorithmes efficaces en théorie (de complexité polynomiale) ; ces restrictions permettent de définir ce que l'on appelle des classes polynomiales. Ces deux approches, même si elles ont offert des avancées significatives, sur le plan pratique ou sur le plan théorique, posent encore des problèmes.

En effet, les classes polynomiales exhibées se révèlent souvent artificielles, au sens où le sous-langage d'expression garantissant la polynomialité est très restrictif (formules SAT à deux littéraux ou CSP binaires arborescents par exemple). Les jeux de données concernés sont alors d’un intérêt très limité. De plus, il existe un réel déficit dans l'unification de ces classes à tel point que dans la plupart des cas, l'exploitation de celles-ci nécessite l'élaboration d'algorithmes de reconnaissance et de traitement ad-hoc et donc restreints à une seule classe. Ce déficit de généralité est l’une des raisons qui fait que les solveurs efficaces ne les exploitent pas. En pratique, de très grosses instances SAT ou CSP (portant sur plusieurs millions de variables) peuvent cependant être résolues sans qu'il soit donc fait recours à l’exploitation de ces classes polynomiales. La puissance de ces systèmes repose généralement sur des techniques algorithmiques de type propagation et/ou apprentissage de contraintes, renforcées par l’exploitation d’heuristiques extrêmement efficaces. Toutefois, malgré l'observation de vrais succès, l'état actuel des connaissances ne permet pas de justifier théoriquement de cette efficacité, et n'offre donc aucun outil qui permettrait de l'évaluer a priori. De plus sur le plan de l’efficacité pratique, nous sommes arrivés à un palier dont le dépassement nécessite l’ouverture vers d’autres orientations.

Les objectifs et ambitions du projet peuvent se résumer à trois points :

- mieux comprendre les raisons de la polynomialité (en caractérisant mieux son origine) et celles de l'efficacité pratique des solveurs (par des critères théoriques de polynomialité)

- élaborer de nouvelles classes polynomiales qui auraient pour vertus essentielles de capter de nombreux jeux de données réels et d’être à la fois efficaces et faciles à implémenter

- étendre significativement les capacités des solveurs actuels afin de franchir un nouveau palier en intégrant l’exploitation des classes polynomiales