Approximating Integer Solution Counting via Space Quantification for Linear Constraints

Approximating Integer Solution Counting via Space Quantification for Linear Constraints

Cunjing Ge, Feifei Ma, Xutong Ma, Fan Zhang, Pei Huang, Jian Zhang

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Main track. Pages 1697-1703. https://doi.org/10.24963/ijcai.2019/235

Solution counting or solution space quantification (means volume computation and volume estimation) for linear constraints (LCs) has found interesting applications in various fields. Experimental data shows that integer solution counting is usually more expensive than quantifying volume of solution space while their output values are close. So it is helpful to approximate the number of integer solutions by the volume if the error is acceptable. In this paper, we present and prove a bound of such error for LCs. It is the first bound that can be used to approximate the integer solution counts. Based on this result, an approximate integer solution counting method for LCs is proposed. Experiments show that our approach is over 20x faster than the state-of-the-art integer solution counters. Moreover, such advantage increases with the problem scale.
Keywords:
Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving
Constraints and SAT: Other approaches