A Tool for Computing and Estimating the Volume of the Solution Space of SMT(LA)

TL;DR

This paper introduces exttt{VolCE}, a tool that extends SMT solving to count solutions and estimate the volume of solution spaces for linear constraints, handling high-dimensional problems efficiently.

Contribution

The paper presents exttt{VolCE}, a novel tool that combines SMT solving with solution counting and volume estimation for convex polytopes, with effective heuristics for high-dimensional cases.

Findings

Successfully counts solutions for complex SMT constraints.

Accurately estimates volume in high-dimensional spaces.

Handles both integer and real variables efficiently.

Abstract

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.