Approximate Integer Solution Counts over Linear Arithmetic Constraints

Counting integer solutions of linear constraints has found interesting applications in various fields. It is equivalent to the problem of counting lattice points inside a polytope. However, state-of-the-art algorithms for this problem become too slow for even a modest number of variables. In this paper, we propose a new framework to approximate the lattice counts inside a polytope with a new random-walk sampling method. The counts computed by our approach has been proved approximately bounded by a (epsilon, delta)-bound. Experiments on extensive benchmarks show that our algorithm could solve polytopes with dozens of dimensions, which significantly outperforms state-of-the-art counters.

Authors

• Cunjing Ge Nanjing University

Keywords

• CSO: Other Foundations of Constraint Satisfaction
• CSO: Satisfiability
• CSO: Satisfiability Modulo Theories
• CSO: Solvers and Tools