Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method

doi:10.3390/a11090142

CIOMP OpenIR

	Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method
	Gao, Wei; Lv, Hengyi; Zhang, Qiang; Cai, Dunbo
	2018
发表期刊	Algorithms
ISSN	19994893
卷号	11 期号:9
摘要	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.
关键词	Monte Carlo methods Chains Formal logic Graphic methods Markov processes
DOI	10.3390/a11090142
收录类别	EI
引用统计
文献类型	期刊论文
条目标识符	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).

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
Estimating the volum（1198KB）	期刊论文	出版稿	开放获取	CC BY-NC-SA	浏览请求全文