计算和估计SMT（LA）解空间体积的工具
A Tool for Computing and Estimating the Volume of the Solution Space of SMT(LA)
摘要：
已经有相当多的工具来解决可满足性模理论（SMT）问题。在本文中，我们提出了\texttt{VolCE}，一个工具，用于计数的解决方案的SMT约束，或者换句话说，用于计算体积的解决方案空间。它的输入本质上是一组线性约束的布尔组合，其中数值变量要么全是整数，要么全是实数，并且每个变量都是有界的。该工具扩展了SMT求解与整数解决方案计数和体积计算/估计凸多面体。该工具采用了有效的算法，能够高效、准确地处理高维问题实例。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
