Acceso al sitio web del Consejo de Políticas de Infraestructura
REVISTA
Algorithms

   
Inicio  /  Algorithms  /  Vol: 11 Par: 9 (2018)  /  Artículo
ARTÍCULO
TITULO

Estimating the Volume of the Solution Space of SMT(LIA) Constraints by a Flat Histogram Method

Wei Gao    
Hengyi Lv    
Qiang Zhang and Dunbo Cai    

Resumen

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.

PÁGINAS
pp. 0 - 0

 Artículos similares

       
 
Xuebo Liu, Yingying Wu and Hongyu Wu    
The 3D body scan technology has recently innovated the way of measuring human bodies and generated a large volume of body measurements. However, one inherent issue that plagues the use of the resultant database is the missing data usually caused by using... ver más
Revista: Applied Sciences

 
Ruoyu Wang, Xianjun Yu, Ke Zhao, Baojie Liu and Guangfeng An    
The variable area bypass injector (VABI) plays a crucial role in variable cycle engines by regulating the flow mixing process in complex bypass ducts, and low-dimensional theoretical models are the key to revealing its working mechanism while estimating ... ver más
Revista: Aerospace

 
Gianluigi Bovesecchi, Sandra Corasaniti, Girolamo Costanza, Fabio Piccotti, Michele Potenza and Maria Elisa Tata    
A nanofluid is a suspension consisting of a uniform distribution of nanoparticles in a base fluid, generally a liquid. Nanofluid can be used as a working fluid in heat exchangers to dissipate heat in the automotive, solar, aviation, aerospace industries.... ver más
Revista: Aerospace

 
Ana Cristina Pinto Silva, Keyla Thayrinne Zoppi Coimbra, Levi Wellington Rezende Filho, Gustavo Pessin and Rosa Elvira Correa-Pabón    
Currently, most mining companies conduct chemical analyses by X-ray fluorescence performed in the laboratory to evaluate the quality of Fe ore, where the focus is mainly on the Fe content and the presence of impurities. However, this type of analysis req... ver más
Revista: AI

 
Zaven G. Ter-Martirosyan, Armen Z. Ter-Martirosyan and Huu H. Dam    
This article presents a solution for the quantitative evaluation of the stress?strain state (SSS) and the bearing capacity of rectangular foundations, factoring in the unit weight of the soil mass and different values of pre-overburden pressure (POP). In... ver más
Revista: Applied Sciences