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
Last Modified: Feb. 29, 2016