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

doi:10.3390/a11090142

CORC > 长春光学精密机械与物理研究所 > 中国科学院长春光学精密机械与物理研究所

	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).