arXiv++ Combinatorics

The purpose of this paper is the formal verification of a counterexample of Santos et al. to the so-called Hirsch Conjecture on the diameter of polytopes (bounded convex polyhedra). In contrast with the pen-and-paper proof, our approach is entirely computational: we implement in Coq and prove correct an algorithm that explicitly computes, within the proof assistant, vertex-edge graphs of polytopes as well as their diameter. The originality of this certificate-based algorithm is to achieve a tradeoff between simplicity and efficiency. Simplicity is crucial in obtaining the proof of correctness of the algorithm. This proof splits into the correctness of an abstract algorithm stated over proof-oriented data types and the correspondence with a low-level implementation over computation-oriented data types. A special effort has been made to reduce the algorithm to a small sequence of elementary operations (e.g., matrix multiplications, basic routines on sets and graphs), in order to make the derivation of the correctness of the low-level implementation more transparent. Efficiency allows us to scale up to polytopes with a challenging combinatorics. For instance, we formally check the two counterexamples of Matschke, Santos and Weibel to the Hirsch conjecture, respectively 20- and 23-dimensional polytopes with 36 425 and 73 224 vertices involving rational coefficients with up to 40 digits in their numerator and denominator. We also illustrate the performance of the method by computing the list of vertices or the diameter of well-known classes of polytopes, such as (polars of) cyclic polytopes involved in McMullen's Upper Bound Theorem.

It is an open question to determine if the theory of self-concordant barriers can provide an interior point method with strongly polynomial complexity in linear programming. In the special case of the logarithmic barrier, it was shown in [Allamigeon, Benchimol, Gaubert and Joswig, SIAM J. on Applied Algebra and Geometry, 2018] that the answer is negative. In this paper, we show that none of the self-concordant barrier interior point methods is strongly polynomial. This result is obtained by establishing that, on parametric families of convex optimization problems, the log-limit of the central path degenerates to a piecewise linear curve, independently of the choice of the barrier function. We provide an explicit linear program that falls in the same class as the Klee-Minty counterexample, i.e., in dimension $n$ with $2n$ constraints, in which the number of iterations is $Ω(2^n)$.

Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under interval sublattices. We also prove a theorem due to Balinski on the $d$-connectedness of the adjacency graph of polytopes of dimension $d$.

The entropic barrier, studied by Bubeck and Eldan (Proc. Mach. Learn. Research, 2015), is a self-concordant barrier with asymptotically optimal self-concordance parameter. In this paper, we study the tropicalization of the central path associated with the entropic barrier, i.e., the logarithmic limit of this central path for a parametric family of linear programs defined over the field of Puiseux series. Our main result is that the tropicalization of the entropic central path is a piecewise linear curve which coincides with the tropicalization of the logarithmic central path studied by Allamigeon et al. (SIAM J. Applied Alg. Geom., 2018). One consequence is that the number of linear pieces in the tropical entropic central path can be exponential in the dimension and the number of inequalities defining the linear program.

We exhibit a class of classical or tropical posynomial systems which can be solved by reduction to linear or convex programming problems. This relies on a notion of colorful vectors with respect to a collection of Newton polytopes. This extends the convex programming approach of one player stochastic games.

Semidefinite programming can be considered over any real closed field, including fields of Puiseux series equipped with their nonarchimedean valuation. Nonarchimedean semidefinite programs encode parametric families of classical semidefinite programs, for sufficiently large values of the parameter. Recently, a correspondence has been established between nonarchimedean semidefinite programs and stochastic mean payoff games with perfect information. This correspondence relies on tropical geometry. It allows one to solve generic nonarchimedean semidefinite feasibility problems, of large scale, by means of stochastic game algorithms. In this paper, we show that the mean payoff of these games can be interpreted as a condition number for the corresponding nonarchimedean feasibility problems. This number measures how close a feasible instance is from being infeasible, and vice versa. We show that it coincides with the maximal radius of a ball in Hilbert's projective metric, that is included in the feasible set. The geometric interpretation of the condition number relies in particular on a duality theorem for tropical semidefinite feasibility programs. Then, we bound the complexity of the feasibility problem in terms of the condition number. We finally give explicit bounds for this condition number, in terms of the characteristics of the stochastic game. As a consequence, we show that the simplest algorithm to decide whether a stochastic mean payoff game is winning, namely value iteration, has a pseudopolynomial complexity when the number of random positions is fixed.

We prove that primal-dual log-barrier interior point methods are not strongly polynomial, by constructing a family of linear programs with $3r+1$ inequalities in dimension $2r$ for which the number of iterations performed is in $Ω(2^r)$. The total curvature of the central path of these linear programs is also exponential in $r$, disproving a continuous analogue of the Hirsch conjecture proposed by Deza, Terlaky and Zinchenko. Our method is to tropicalize the central path in linear programming. The tropical central path is the piecewise-linear limit of the central paths of parameterized families of classical linear programs viewed through logarithmic glasses. This allows us to provide combinatorial lower bounds for the number of iterations and the total curvature, in a general setting.

We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define the basic predicates over polyhedra in an effective way (i.e., as programs), and relate them with the corresponding usual logical counterparts. To this end, we make an extensive use of the Boolean reflection methodology. The benefit of this approach is that we can easily derive the proof of several fundamental results on polyhedra, such as Farkas' Lemma, the duality theorem of linear programming, and Minkowski's Theorem.

We introduce tropical spectrahedra, defined as the images by the nonarchimedean valuation of spectrahedra over the field of real Puiseux series. We provide an explicit polyhedral characterization of generic tropical spectrahedra, involving principal tropical minors of size at most 2. One of the key ingredients is Denef-Pas quantifier elimination result over valued fields. We obtain from this that the nonarchimedean valuation maps semialgebraic sets to semilinear sets that are closed. We also prove that, under a regularity assumption, the image by the valuation of a basic semialgebraic set is obtained by tropicalizing the inequalities which define it.

A general issue in computational optimization is to develop combinatorial algorithms for semidefinite programming. We address this issue when the base field is nonarchimedean. We provide a solution for a class of semidefinite feasibility problems given by generic matrices. Our approach is based on tropical geometry. It relies on tropical spectrahedra, which are defined as the images by the valuation of nonarchimedean spectrahedra. We establish a correspondence between generic tropical spectrahedra and zero-sum stochastic games with perfect information. The latter have been well studied in algorithmic game theory. This allows us to solve nonarchimedean semidefinite feasibility problems using algorithms for stochastic games. These algorithms are of a combinatorial nature and work for large instances.

It is known that any tropical polytope is the image under the valuation map of ordinary polytopes over the Puiseux series field. The latter polytopes are called lifts of the tropical polytope. We prove that any pure tropical polytope is the intersection of the tropical half-spaces given by the images under the valuation map of the facet-defining half-spaces of a certain lift. We construct this lift explicitly, taking into account geometric properties of the given polytope. Moreover, when the generators of the tropical polytope are in general position, we prove that the above property is satisfied for any lift. This solves a conjecture of Develin and Yu.

We disprove a continuous analogue of the Hirsch conjecture proposed by Deza, Terlaky and Zinchenko, by constructing a family of linear programs with $3r+4$ inequalities in dimension $2r+2$ where the central path has a total curvature in $Ω(2^r)$. Our method is to tropicalize the central path in linear programming. The tropical central path is the piecewise-linear limit of the central paths of parameterized families of classical linear programs viewed through logarithmic glasses. The lower bound for the classical curvature is obtained by developing a combinatorial concept of a tropical angle.

A combinatorial simplex algorithm is an instance of the simplex method in which the pivoting depends on combinatorial data only. We show that any algorithm of this kind admits a tropical analogue which can be used to solve mean payoff games. Moreover, any combinatorial simplex algorithm with a strongly polynomial complexity (the existence of such an algorithm is open) would provide in this way a strongly polynomial algorithm solving mean payoff games. Mean payoff games are known to be in NP and co-NP; whether they can be solved in polynomial time is an open problem. Our algorithm relies on a tropical implementation of the simplex method over a real closed field of Hahn series. One of the key ingredients is a new scheme for symbolic perturbation which allows us to lift an arbitrary mean payoff game instance into a non-degenerate linear program over Hahn series.

We introduce a generalization of tropical polyhedra able to express both strict and non-strict inequalities. Such inequalities are handled by means of a semiring of germs (encoding infinitesimal perturbations). We develop a tropical analogue of Fourier-Motzkin elimination from which we derive geometrical properties of these polyhedra. In particular, we show that they coincide with the tropically convex union of (non-necessarily closed) cells that are convex both classically and tropically. We also prove that the redundant inequalities produced when performing successive elimination steps can be dynamically deleted by reduction to mean payoff game problems. As a complement, we provide a coarser (polynomial time) deletion procedure which is enough to arrive at a simply exponential bound for the total execution time. These algorithms are illustrated by an application to real-time systems (reachability analysis of timed automata).

We develop a tropical analog of the simplex algorithm for linear programming. In particular, we obtain a combinatorial algorithm to perform one tropical pivoting step, including the computation of reduced costs, in O(n(m+n)) time, where m is the number of constraints and n is the dimension.

Tropical polyhedra are known to be representable externally, as intersections of finitely many tropical half-spaces. However, unlike in the classical case, the extreme rays of their polar cones provide external representations containing in general superfluous half-spaces. In this paper, we prove that any tropical polyhedral cone in R^n (also known as "tropical polytope" in the literature) admits an essentially unique minimal external representation. The result is obtained by establishing a (partial) anti-exchange property of half-spaces. Moreover, we show that the apices of the half-spaces appearing in such non-redundant external representations are vertices of the cell complex associated with the polyhedral cone. We also establish a necessary condition for a vertex of this cell complex to be the apex of a non-redundant half-space. It is shown that this condition is sufficient for a dense class of polyhedral cones having "generic extremities".

We discuss the tropical analogues of several basic questions of convex duality. In particular, the polar of a tropical polyhedral cone represents the set of linear inequalities that its elements satisfy. We characterize the extreme rays of the polar in terms of certain minimal set covers which may be thought of as weighted generalizations of minimal transversals in hypergraphs. We also give a tropical analogue of Farkas lemma, which allows one to check whether a linear inequality is implied by a finite family of linear inequalities. Here, the certificate is a strategy of a mean payoff game. We discuss examples, showing that the number of extreme rays of the polar of the tropical cyclic polyhedral cone is polynomially bounded, and that there is no unique minimal system of inequalities defining a given tropical polyhedral cone.

The celebrated upper bound theorem of McMullen determines the maximal number of extreme points of a polyhedron in terms of its dimension and the number of constraints which define it, showing that the maximum is attained by the polar of the cyclic polytope. We show that the same bound is valid in the tropical setting, up to a trivial modification. Then, we study the natural candidates to be the maximizing polyhedra, which are the polars of a family of cyclic polytopes equipped with a sign pattern. We construct bijections between the extreme points of these polars and lattice paths depending on the sign pattern, from which we deduce explicit bounds for the number of extreme points, showing in particular that the upper bound is asymptotically tight as the dimension tends to infinity, keeping the number of constraints fixed. When transposed to the classical case, the previous constructions yield some lattice path generalizations of Gale's evenness criterion.

We establish a characterization of the vertices of a tropical polyhedron defined as the intersection of finitely many half-spaces. We show that a point is a vertex if, and only if, a directed hypergraph, constructed from the subdifferentials of the active constraints at this point, admits a unique strongly connected component that is maximal with respect to the reachability relation (all the other strongly connected components have access to it). This property can be checked in almost linear-time. This allows us to develop a tropical analogue of the classical double description method, which computes a minimal internal representation (in terms of vertices) of a polyhedron defined externally (by half-spaces or hyperplanes). We provide theoretical worst case complexity bounds and report extensive experimental tests performed using the library TPLib, showing that this method outperforms the other existing approaches.