Enumerating Integer Projections of Parametric Polytopes: A Direct Approach

Many compiler techniques depend on the ability to count the number of integer points that satisfy a given set of linear inequalities. Typically, a subset of the variables are identified as the parameters ~ p and the number of possible values for the other, “counted” variables ~y needs to be counted as a function of those parameters. If each variable is either a parameter or counted, then the problem is equivalent to the enumeration of parametric polytopes, which can be computed efficiently using a technique based on Barvinok’s decomposition of unimodular cones [1, 3, 5]. In general, the linear inequalities may also involve additional, existentially quantified variables ~ǫ and then the object is to count the number of possible integer values for ~y in function of the parameters ~ p This problem is equivalent to enumerating an integer projection of a parametric polytope. Pugh [4] addresses the closely related problem of counting the number of solutions to Presburger formulas, but his technique seems underspecified and has apparently never been implemented. One of the substeps is also clearly exponential in the input size. More recently, a technique was outlined for integer projections of non-parametric polytopes [2], but it appears not to have been implemented yet and it is not immediately clear how easily it can be extended to the parametric case. Consider the polyhedron P defined by the given set of linear inequalities in (d + d + n)-dimensional space, where d, d and n are the number of counted variables, existential variables and parameters. Our technique manipulates this polyhedron directly through a set of simplification rules, which either reduce the number of existential variables, shrink the polyhedron or split the problem into several smaller subproblems. Pick an existential variable ǫi and take a pair of inequalities such that the coefficients of ǫi have opposite signs. The two inequalities determine a range for ǫi as a function of the other variables. If no such pair exists or if this range admits at least one integer solution over the whole of P , then ǫi can be eliminated. If a pair exists such that at least one of the inequalities is independent of the other existential variables and such that the range admits at most one solution, then ǫi can be treated as a counted variable. The polyhedron can be shrunk by adding cutting planes such that the bounding box of P has integer vertices. In principle, planes can be added until the integer hull is obtained, basically solving the problem, but this would be prohibitively expensive. Rays and lines can be removed from P by taking a slice