Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6875391 | Theoretical Computer Science | 2018 | 20 Pages |
Abstract
The satisfiability modulo theories (SMT) problem is a decision problem, i.e., deciding the satisfiability of logical formulas with respect to combinations of background theories (like reals, integers, arrays, bit-vectors). In this paper, we study the counting version of SMT with respect to linear arithmetic - SMT(LA), which generalizes both model counting and volume computation of convex polytopes. We describe a method for estimating the volume of convex polytopes based on the Multiphase Monte-Carlo method. It employs a new technique to reutilize random points, so that the number of random points can be significantly reduced. We prove that the reutilization technique has no side-effect on the error. We also investigate a simplified version of hit-and-run method: the coordinate directions method. Based on volume estimation method for polytopes, we present an approach to estimating the volume of the solution space of SMT(LA) formulas. It employs a heuristic strategy to accelerate the volume estimation procedure. In addition, we devise some specific techniques for instances that arise from program analysis.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Cunjing Ge, Feifei Ma, Peng Zhang, Jian Zhang,