Formally Certifying the Vertex Set of a Polyhedron Faster than Informal Enumeration
Abstract
The computation of the vertices of a polyhedron described by a system of linear inequalities is a central problem in polyhedral computation. It is a fundamental step in the conversion between H-representations, by linear inequalities, and V-representations, by vertices and extreme rays. This operation plays an important role both in the study of polyhedra and their combinatorics in mathematics and in applications to software and system verification. We present a certificate-based approach for formally verifying the computation of the vertices of a polyhedron. Given an informally computed list of vertices, our method allows to certify in the proof assistant Rocq that the list is complete, or even exact. The cornerstone of the method is a new completeness criterion based on an abstract simplicial complex that generalizes a triangulation of the normal fan of the polyhedron. A significant advantage over previous approaches is that the usually expensive numerical computations are essentially reduced to membership tests to the polyhedron, while the other steps are cheap combinatorial tests. We implement the certification method and prove its correctness in the proof assistant Rocq. We experiment with it on a variety of polyhedra, including Birkhoff polytopes, cross-polytopes, cubes, permutahedra, hypersimplices, and high-dimensional polytopes involved in the disproof of the Hirsch conjecture. Our experiments show that certification with the Rocq-to-OCaml extracted checker is typically 1.5x to over 5x faster than vertex enumeration by the state-of-the-art informal C implementation lrslib of the reverse search method.
Related
- Enumeration of small vertex-transitive directed strongly regular graphs
- The Last Isolated Vertex in Random-Order Uncovering of Cycles and Their Powers: Exact Enumeration and Weibull Limits
- Embracing exchange sequences and oriented matroid polyhedron diameter
- The distributions of convex body functionals of the Poisson polyhedron
- A second eight-faced polyhedron in which every two faces share an edge
BibTeX
@misc{allamigeon2026formally,
title = {{Formally Certifying the Vertex Set of a Polyhedron Faster than Informal Enumeration}},
author = {Xavier Allamigeon and Yazid Id-Sahra and Pierre-Yves Strub},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.11913},
eprint = {2610.11913},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.11913},
}
RIS
TY - UNPB
TI - Formally Certifying the Vertex Set of a Polyhedron Faster than Informal Enumeration
AU - Xavier Allamigeon
AU - Yazid Id-Sahra
AU - Pierre-Yves Strub
PY - 2026
DA - 2026/10/08
PB - arXiv
DO - 10.48550/arxiv.2610.11913
UR - https://arxiv.org/abs/2610.11913
AB - The computation of the vertices of a polyhedron described by a system of linear inequalities is a central problem in polyhedral computation. It is a fundamental step in the conversion between H-representations, by linear inequalities, and V-representations, by vertices and extreme rays. This operation plays an important role both in the study of polyhedra and their combinatorics in mathematics and in applications to software and system verification. We present a certificate-based approach for formally verifying the computation of the vertices of a polyhedron. Given an informally computed list of vertices, our method allows to certify in the proof assistant Rocq that the list is complete, or even exact. The cornerstone of the method is a new completeness criterion based on an abstract simplicial complex that generalizes a triangulation of the normal fan of the polyhedron. A significant advantage over previous approaches is that the usually expensive numerical computations are essentially reduced to membership tests to the polyhedron, while the other steps are cheap combinatorial tests. We implement the certification method and prove its correctness in the proof assistant Rocq. We experiment with it on a variety of polyhedra, including Birkhoff polytopes, cross-polytopes, cubes, permutahedra, hypersimplices, and high-dimensional polytopes involved in the disproof of the Hirsch conjecture. Our experiments show that certification with the Rocq-to-OCaml extracted checker is typically 1.5x to over 5x faster than vertex enumeration by the state-of-the-art informal C implementation lrslib of the reverse search method.
ER -