Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic
Sponsor
This work was supported by the Chinese National 973 Plan under grant No. 2010CB328003, the NSF of China under grants No. 11326070, 61272001, 60903030, 91218302, the Chinese National Key Technology R&D Program under grant No. SQ2012BAJY4052, the Tsinghua University Initiative Scientific Research Program, and the Importation and Development of High-Caliber Talents Project of Beijing Municipal Institutions under grant No. YETP0167
Published In
Theory of Computing Systems
Document Type
Citation
Publication Date
2-2015
Subjects
Monte Carlo method, Volume estimation, Algorithms, Software engineering
Abstract
Satisfiability Modulo Theories techniques can check if a formula is satisfiable. In many cases, not only the qualitative judgment (satisfiable or not) but also the quantitative judgment (the dimension and size of the solution space) are of practical interest. For instance, the volume of path condition formula reflects the probability of the corresponding program path being taken. However, existing algorithms are not practical because they only work for small instances. Given a formula with Boolean structures, its volume is typically obtained by first decomposing it to a series of conjunctions (of linear constraints) with disjoint solution spaces and then accumulating the volume of each one. For the former step, we propose a BDD-based search algorithm which sharply reduces the number of conjunctions. For the latter one, we propose a Monte-Carlo integration with a ray-based sampling strategy, which approximates the volume efficiently and accurately. Furthermore, degenerate solution spaces, which are not considered by other algorithms, could be handled properly by ours. Experimental results show that our method can handle formulas with up to 20 variables, which will cover many practical cases in software engineering
Rights
© 2015 Springer International Publishing AG
Locate the Document
DOI
10.1007/s00224-014-9553-9
Persistent Identifier
http://archives.pdx.edu/ds/psu/20911
Citation Details
Zhou, Min, Fei He, Xiaoyu Song, Shi He, Gangyi Chen, and Ming Gu. "Estimating the volume of solution space for satisfiability modulo linear real arithmetic." Theory of Computing Systems 56, no. 2 (2015): 347-371.