Algorithms for Weighted Counting over Parametric Polytopes: A Survey and a Practical Comparison

摘要

The polytope model is widely used in compiler analysis for representing a certain class of programs. Many counting problems that occur in the analysis of such programs can be solved by counting the number of integer points in a parametric polytope. In other counting problems, polynomial weights are assigned to the integer points of a parametric polytope and the objective is to find the sum of these weights over all integer points. This paper briefly surveys a number of algorithms for solving such problems, extending them where needed and evaluating them on a set of realistic and constructed examples from compiler analysis and beyond. The paper also serves to document some of the algorithms implemented in the freely available barvinok library.