Name
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. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1016/j.tcs.2016.10.019 | Theoretical Computer Science |
Keywords | Field | DocType |
SMT,Volume,Counting,Convex polytope | Integer,Discrete mathematics,Combinatorics,Heuristic,Decision problem,Satisfiability,Algorithm,Convex polytope,Polytope,Program analysis,Mathematics,Satisfiability modulo theories | Journal |
Volume | ISSN | Citations |
743 | 0304-3975 | 2 |
PageRank | References | Authors |
0.40 | 21 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cunjing Ge | 1 | 3 | 2.12 |
| Feifei Ma | 2 | 58 | 13.64 |
| Peng Zhang | 3 | 172 | 19.52 |
| Jian Zhang | 4 | 288 | 24.45 |