A Tool for Computing and Estimating the Volume of the Solution Space of SMT(LA)
This provides a practical tool for researchers and engineers working with SMT solving who need quantitative analysis of solution spaces, though it is an incremental extension of existing SMT solvers.
The authors tackled the problem of counting solutions to SMT constraints with linear arithmetic by developing VolCE, a tool that computes or estimates the volume of solution spaces for bounded integer or real variables, achieving efficient and accurate performance on high-dimensional instances.
There are already quite a few tools for solving the Satisfiability Modulo Theories (SMT) problems. In this paper, we present \texttt{VolCE}, a tool for counting the solutions of SMT constraints, or in other words, for computing the volume of the solution space. Its input is essentially a set of Boolean combinations of linear constraints, where the numeric variables are either all integers or all reals, and each variable is bounded. The tool extends SMT solving with integer solution counting and volume computation/estimation for convex polytopes. Effective heuristics are adopted, which enable the tool to deal with high-dimensional problem instances efficiently and accurately.