Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming

International audienceConvex polyhedra capture linear relations between variables. They are used in static analysis and optimizing compilation. Their high expressiveness is however barely used in verification because of their cost, often prohibitive as the number of variables involved increases. Our goal in this article is to lower this cost. Whatever the chosen representation of polyhedra – as constraints, as generators or as both – expensive operations are unavoidable. That cost is mostly due to four operations: conversion between representations, based on Chernikova’s algorithm, for libraries in double description; convex hull, projection and minimization, in the constraints-only representation of polyhedra. Libraries operating over generators incur exponential costs on cases common in program analysis. In the Verimag Polyhedra Library this cost was avoided by a constraints-only representation and reducingall operations to variable projection, classically done by Fourier-Motzkin elimination. Since Fourier-Motzkin generates many redundant constraints, minimization was however very expensive. In this article, we avoid this pitfall by expressing projection as a parametric linear programming problem. This dramatically improves efficiency, mainly because it avoids the post-processing minimization. We show how our new approach can be up to orders of magnitude faster than the previous approach implemented in the Verimag Polyhedra Library that uses only constraints and Fourier-Motzkin elimination, and on par with the conventional double description approach, as implemented in well-known libraries