Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic
详细信息 查看全文
- 作者：Min Zhou (1) (2) (3)
Fei He (1) (2) (3)
Xiaoyu Song (4)
Shi He (1) (2) (3)
Gangyi Chen (5)
Ming Gu (1) (2) (3)
1. School of Software ; Tsinghua University ; Beijing ; 100084 ; China
2. Key Laboratory for Information System Security ; MOE ; Shanghai ; China
3. Tsinghua National Laboratory for Information Science and Technology (TNList) ; Beijing ; China
4. Electrical and Computer Engineering ; Portland State University ; Portland ; OR ; 97207 ; USA
5. School of Mathematics and Information Science ; Guangzhou University ; Guangzhou ; 510006 ; China - 关键词：Satisfiability modulo theories ; Linear arithmetic ; Volume estimation ; Monte ; Carlo integration
- 刊名：Theory of Computing Systems
- 出版年：2015
- 出版时间：February 2015
- 年：2015
- 卷：56
- 期：2
- 页码：347-371
- 全文大小：2,342 KB
- 参考文献：1. Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. 100(6), 509鈥?16 (1978) CrossRef
2. Athreya, K.: Unit ball in high dimensions. Resonance 13(4), 334鈥?42 (2008) CrossRef
3. Avis, D.: Computational experience with the reverse search vertex enumeration algorithm. Optim. Methods Softw. 10(2), 107鈥?24 (1998) CrossRef
4. Avis, D.: A revised implementation of the reverse search vertex enumeration algorithm. In: Polytopescombinatorics and Computation, pp. 177鈥?98. Springer (2000)
5. Ball, T., Larus, J.R.: Branch prediction for free. In: Proceedings of PLDI鈥?3, pp. 300鈥?13. ACM, New York (1993)
6. Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. Handb. Satisfiability 185, 825鈥?85 (2009)
7. Barrett, C., Tinelli, C.: CVC3. In: Computer Aided Verification, pp. 298鈥?02. Springer (2007)
8. B眉eler, B., Enge, A., Fukuda, K.: Exact volume computation for polytopes: a practical study. In: Polytopes-Combinatorics and Computation, pp. 131鈥?54. Springer (2000)
9. Buse, R. P., Weimer, W.: The road not taken: estimating path execution frequency statically. In: Proceedings of ICSE鈥?9, pp. 144鈥?54. IEEE Computer Society (2009)
10. Dantzig, G. B.: Linear Programming and Extensions. Princeton university press (1998)
11. De Moura, L., Bj酶rner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 337鈥?40. Springer (2008)
12. Dutertre, B., De Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of CAV鈥?6, pp. 81鈥?4. Springer (2006)
13. Dutertre, B., De Moura, L.: The yices SMT solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf, 2, 2, (2006)
14. Dyer, M., Frieze, A., Kannan, R.: A random polynomial-time algorithm for approximating the volume of convex bodies. JACM 38(1), 1鈥?7 (1991) CrossRef
15. Dyer, M.E., Frieze, A.M.: On the complexity of computing the volume of a polyhedron. SIAM J. Comput. 17(5), 967鈥?74 (1988) CrossRef
16. Gr枚tschel, M., Lov谩sz, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization. Springer (1988). http://eudml.org/doc/204187
17. Huang, J., Darwiche, A.: Using DPLL for efficient OBDD construction. In: Theory and Applications of Satisfiability Testing, pp. 157鈥?72. Springer (2005)
18. Kannan, R., Lov谩sz, L., Simonovits, M.: Random walks and an / O 鈭?/sup>( / n 5) volume algorithm for convex bodies. Random Struct. Algoritm. 11(1), 1鈥?0 (1997) CrossRef
19. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385鈥?94 (1976) CrossRef
20. Liu, S., Zhang, J.: Program analysis: from qualitative analysis to quantitative analysis (nier track). In: Proceedings of ICSE鈥?1, pp. 956鈥?59. IEEE (2011)
21. Liu, S., Zhang, J., Zhu, B.: Volume computation using a direct monte carlo method. In: Computing and Combinatorics, pp. 198鈥?09. Springer (2007)
22. Lov谩sz, L., Simonovits, M.: Random walks in a convex body and an improved volume algorithm. Random Struct. Algoritm. 4(4), 359鈥?12 (1993) CrossRef
23. Lov谩sz, L., Vempala, S.: Simulated annealing in convex bodies and an / O 鈭?/sup>( / n 4) volume algorithm. J. Comput. Syst. Sci. 72(2), 392鈥?17 (2006) CrossRef
24. Ma, F., Liu, S., Zhang, J.: Volume computation for boolean combination of linear arithmetic constraints. In: Proceedings of CADE鈥?9, pp. 453鈥?68. Springer (2009)
25. Marsaglia, G.: Choosing a point from the surface of a sphere. Ann. Math. Stat. 43(2), 645鈥?46 (1972) CrossRef
26. Necula, G. C.: Proof-Carrying Code. Design and Implementation. Springer (2002)
27. Nelson, C. G.: Techniques for program verification. XEROX Research Center (1981)
28. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis鈥揚utnam鈥揕ogemann鈥揕oveland procedure to DPLL(T). JACM 53(6), 937鈥?77 (2006) CrossRef
29. P膬s膬reanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Softw. Tools Technol. Transfer 11(4), 339鈥?53 (2009) CrossRef
30. Poulding, S., Clark, J.A.: Efficient software verification: Statistical testing using automated search. IEEE Trans. Softw. Eng. 36(6), 763鈥?77 (2010) CrossRef
31. Smale, S.: On the average number of steps of the simplex method of linear programming. Math. Program. 27(3), 241鈥?62 (1983) CrossRef
32. Wei, W., Selman, B.: A new approach to model counting. In: Theory and Applications of Satisfiability Testing, pp. 324鈥?39. Springer (2005) - 刊物类别：Computer Science
- 刊物主题：Theory of Computation
Computational Mathematics and Numerical Analysis - 出版者：Springer New York
- ISSN：1433-0490
文摘
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