Tags:Floating-point arithmetic, Parametric linear programming and Polyhedral projection
Abstract:
Polyhedral projection is a main operation of the polyhedron abstract domain. It can be computed via parametric linear programming(PLP), which is more efficient than the classic Fourier-Motzkin elimination method. In prior work, PLP was done in arbitrary precision rational arithmetic. In this paper, we present an approach where most of the computation is performed in floating-point arithmetic, then exact rational results are reconstructed. We also propose a workaround for a difficulty that plagued previous attempts at using PLP for computations on polyhedra: in general the linear programming problems are degenerate, resulting in redundant computations and geometric descriptions.
An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection