OpenAlex ·
Formally Certifying the Vertex Set of a Polyhedron Faster than Informal Enumeration
- Published
- Source
- OpenAlex
- Published in
- arXiv (Cornell University)
- DOI
- 10.48550/arxiv.2610.11913
- Original
- Read it at the publisher
- Topics
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.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Artificial Intelligence
A QPTAS for Stochastic Scheduling of Bernoulli Jobs
Dynamic Matching with Abandonment: Optimal Guarantees via Static Priority Policies
A Catalytic Algorithm for Transposing Unknown Qutrit Unitaries with Tight Query Bounds
Quantum Query Complexity of Maximum Degree and its Generalizations
Uniqueness for tv-regularized inverse problems with source in divergence form
Get the few papers worth your time in Artificial Intelligence every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.