Approximating Integer Solution Counting via Space Quantification for Linear Constraints

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.

Authors

• Cunjing Ge Nanjing University
• Feifei Ma Institute of Software, Chinese Academy of Sciences University of the Chinese Academy of Sciences
• Xutong Ma
• Fan Zhang
• Pei Huang
• Jian Zhang

Keywords

• Constraints and SAT: Other approaches
• Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving