Séminaire APRRSS

Nouvelle Algorithmique pour le Calcul Polyédral via Programmation Linéaire Paramétrique

17/05/2018
Intervenant(s) : Alexandre Maréchal (APR)
Ce séminaire présente la nouvelle implémentation de la Verified Polyhedra Library (VPL), une bibliothèque efficace de calcul polyédral. Elle fournit des opérateurs certifiés en Coq, s’appliquant sur des représentations en contraintes. La version précédente souffrait d’inefficacité lors d’opérateurs cruciaux, à savoir l’élimination de variables et l’enveloppe convexe. Je présenterai ici des améliorations importantes qui bénéficient à la modularité, la simplicité et au passage à l’échelle de la bibliothèque : le processus de certification est généralisé et simplifié ; les conditions polynomiales sont maintenant traitées ; les calculs qui n’impliquent pas de certification sont effectués en flottants ; de nouveaux algorithmes sont fournis pour la minimisation de représentation et la détection d’égalités implicites. D’un côté, l’implémentation d’un solveur de problèmes de programmation linéaire paramétrique (PLP) a mené à une meilleure efficacité tant en nombre de contraintes que de générateurs. L’élimination de variables et l’enveloppe convexe sont tous deux encodés en problème PLP. Le PLP est un outil générique possédant de nombreuses applications, et qui permet d’éviter la génération de redondances grâce à l’utilisation d’une contrainte de normalisation. De plus, nous proposons de nouveaux opérateurs pour la gestion des contraintes polynomiales, l’un d’entre eux étant également encodé en tant que problème PLP. De l’autre, la certification de la bibliothèque a été grandement optimisée et simplifiée. La VPL suit un paradigme de vérification a posteriori, où les calculs non triviaux sont effectués par des oracles externes générant des témoins de correction. Ces témoins sont ensuite validés par un vérifieur écrit en Coq. Grâce à un cadre de certification puissant et innovant, le polymorphic factory style (PFS), la plupart des aspects délicats de la génération de témoins sont maintenant évitée. La souplesse du PFS est démontrée par la création d’une tactique en COQ qui découvre les égalités implicites en arithmétique linéaire.

romain.demangeon (at) nulllip6.fr
Mentions légales
Carte du site