Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Mon 16 Jan 2017 11:00 - 11:30 at Amphitheater 44 - Numerical domains Chair(s): Laure Gonnord

Polyhedra are used in verification and automatic parallelization to capture linear relations between variables. A polyhedron can be represented as constraints, generators or both in the double description framework. Whatever the representation, most polyhedral operators spend a significant amount of time to maintain minimal representations.

To minimize a polyhedron in constraints-only representation, the redundancy of each constraint must be checked with respect to others. Each of these redundancy tests generally implies solving a linear programming (LP) problem using the simplex algorithm. We present an algorithm that replaces most LP problem resolutions by distance computations.

The geometric intuition is simple: consider ray traces starting from a point within the polyhedron and orthogonal to its faces. A face first encountered by one of these rays is an actual face of the polyhedron. It is therefore a non-redundant constraint. Since this procedure is incomplete, LP problem resolutions are required for the remaining undetermined constraints.

Experiments show that our algorithm drastically reduces the number of calls to the simplex, resulting in a considerable speed improvement. In addition, our algorithm generates by construction a certificate for each constraint: redundancy is established by exhibiting a non-negative linear combination of contraints that yields the removed constraint, whereas irredundancy is shown by exhibiting a point outside of the polyhedron which is excluded only by the kept constraint.

To follow the geometric interpretation, the algorithm is explained in terms of constraints but it can also be used to minimize generators.

slides (Marechal_VMCAI2017.pdf)885KiB

Mon 16 Jan