一种用于计算与估计 SMT(LA) 解空间体积的工具
人工智能
2015-07-02 v1
摘要
已有不少用于求解可满足性模理论 (SMT) 问题的工具。本文我们提出 \texttt{VolCE}，一个用于对 SMT 约束的解进行计数，换言之，用于计算解空间体积的工具。其输入本质上是一组线性约束的布尔组合，其中数值变量全为整数或全为实数，且每个变量均有界。该工具通过整数解计数和凸多面体的体积计算/估计扩展了 SMT 求解。采用了有效的启发式方法，使该工具能够高效且精确地处理高维问题实例。
引用
@article{arxiv.1507.00142,
title = {A Tool for Computing and Estimating the Volume of the Solution Space of SMT(LA)},
author = {Cunjing Ge and Feifei Ma and Jian Zhang},
journal= {arXiv preprint arXiv:1507.00142},
year = {2015}
}