Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method
文献类型：期刊论文
| 作者 | Gao, Wei; Lv, Hengyi; Zhang, Qiang ; Cai, Dunbo
|
| 刊名 | Algorithms
 |
| 出版日期 | 2018 |
| 卷号 | 11期号:9 |
| 关键词 | Monte Carlo methods Chains Formal logic Graphic methods Markov processes |
| ISSN号 | 19994893 |
| DOI | 10.3390/a11090142 |
| 英文摘要 | The satisfiability modulo theories (SMT) problem is to decide the satisfiability of a logical formula with respect to a given background theory. This work studies the counting version of SMT with respect to linear integer arithmetic (LIA), termed SMT(LIA). Specifically, the purpose of this paper is to count the number of solutions (volume) of a SMT(LIA) formula, which has many important applications and is computationally hard. To solve the counting problem, an approximate method that employs a recent Markov Chain Monte Carlo (MCMC) sampling strategy called "flat histogram" is proposed. Furthermore, two refinement strategies are proposed for the sampling process and result in two algorithms, MCMC-Flat1/2 and MCMC-Flat1/t, respectively. In MCMC-Flat1/t, a pseudo sampling strategy is introduced to evaluate the flatness of histograms. Experimental results show that our MCMC-Flat1/t method can achieve good accuracy on both structured and random instances, and our MCMC-Flat1/2 is scalable for instances of convex bodies with up to 7 variables. 2018 by the authors. |
| 源URL | [http://ir.ciomp.ac.cn/handle/181722/60653]  |
| 专题 | 中国科学院长春光学精密机械与物理研究所 |
| 推荐引用方式 GB/T 7714 | Gao, Wei,Lv, Hengyi,Zhang, Qiang,et al. Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method[J]. Algorithms,2018,11(9). |
| APA | Gao, Wei,Lv, Hengyi,Zhang, Qiang,&Cai, Dunbo.(2018).Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method.Algorithms,11(9). |
| MLA | Gao, Wei,et al."Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method".Algorithms 11.9(2018). |
入库方式： OAI收割
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。