Volume Computation and Estimation, Solution Counting

Given a set of constraints, where each constraint is a Boolean combination of linear inequalities, there are quite some techniques and tools for checking the consistency (or finding a solution). But can we compute the number of solutions to the constraints? In other words, can we compute the size/volume of the solution space? This is the counting version of the SMT(LAC) problem, i.e., #SMT(LAC).

For the past several years, we have been investigating the above problem. Recently, we developed a tool called VolCE for doing that. Here is the executable (on Linux, 64-bit system) together with a manual. It uses a tool called PolyVest that we developed.



---

Related Papers

• Feifei Ma, Sheng Liu and Jian Zhang. Volume computation for Boolean combination of linear arithmetic constraints. Proc. CADE-22, LNCS 5663, pp.453-468, 2009.
• Sheng Liu and Jian Zhang. Program analysis: from qualitative analysis to quantitative analysis. Proc. ICSE 2011 (NIER track), pp.956-959.
• Cunjing Ge, Feifei Ma and Jian Zhang. A tool for computing and estimating the volume of the solution space of SMT(LA). CoRR abs/1507.00142, 2015.



---


Last Modified: Feb. 29, 2016