Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic

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

DOI

10.1007/s00224-014-9553-9

Persistent Identifier

http://archives.pdx.edu/ds/psu/20911

Share

COinS