SharpSMT: a scalable toolkit for measuring solution spaces of SMT(LA) formulas

Abstract

In this paper, we present SHARPSMT, a toolkit for measuring solution spaces of SMT(LA) formulas which are Boolean combinations of linear arithmetic constraints, i.e., #SMT(LA) problems. It integrates SMT satisfiability solving algorithm with various polytope subroutines: volume computation, volume estimation, lattice counting, and approximate lattice counting. We propose a series of new polytope preprocessing techniques which have been implemented in SHARPSMT. Experimental results show that the new polytope preprocessing techniques are very effective, especially on application instances. We believe that SHARPSMT will be useful in a number of areas.

Graphical abstract

Keywords

#SMT(LA) problems / DPLL(T) algorithm / polytope preprocessing techniques / volume computation / lattice counting

References

[1] Barrett C, Conway C L, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C. CVC4. In: Proceedings of the 23rd International Conference on Computer aided verification. 2011, 171−177

[2] Barbosa H, Barrett C, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, Nötzli A, Ozdemir A, Preiner M, Reynolds A, Sheng Y, Tinelli C, Zohar Y. cvc5: a versatile and industrial-strength SMT solver. In: Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2022, 415−442

[3] Cimatti A, Griggio A, Schaafsma B J, Sebastiani R. The MathSAT5 SMT solver. In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013, 93−107

[4] Dutertre B. Yices 2.2. In: Proceedings of the 26th International Conference on Computer Aided Verification. 2014, 737−744

[5] de Moura L M, Bjørner N. Z3: an efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008, 337−340

[6] Chavira M, Darwiche A. On probabilistic inference by weighted model counting. Artificial Intelligence, 2008, 172(6−7): 772−799

[7] Belle V, Passerini A, Van Den Broeck G. Probabilistic inference in hybrid domains by weighted model integration. In: Proceedings of the 24th International Conference on Artificial Intelligence. 2015, 2770−2776

[8] Zanarini A, Pesant G. Solution counting algorithms for constraint-centered search heuristics. In: Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming. 2007, 743−757

[9] Pesant G. Counting-based search for constraint optimization problems. In: Proceedings of the 30th AAAI Conference on Artificial Intelligence. 2016, 3441−3448

[10] Huang A, Lloyd L, Omar M, Boerkoel J C. New perspectives on flexibility in simple temporal planning. In: Proceedings of the 28th International Conference on Automated Planning and Scheduling (ICAPS). 2018, 123−131

[11] Geldenhuys J, Dwyer M B, Visser W. Probabilistic symbolic execution. In: Proceedings of International Symposium on Software Testing and Analysis (ISSTA). 2012, 166−176

[12] Luckow K, Păsăreanu C S, Dwyer M B, Filieri A, Visser W. Exact and approximate probabilistic symbolic execution for nondeterministic programs. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering (ASE). 2014, 575−586

[13] Ma F, Liu S, Zhang J. Volume computation for Boolean combination of linear arithmetic constraints. In: Proceedings of the 22nd International Conference on Automated Deduction (CADE). 2009, 453−468

[14] Ge C, Ma F, Zhang P, Zhang J . Computing and estimating the volume of the solution space of SMT(LA) constraints. Theoretical Computer Science, 2018, 743: 110–129

[15] Ge C, Ma F, Ma X, Zhang F, Huang P, Zhang J. Approximating integer solution counting via space quantification for linear constraints. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI). 2019, 1697−1703

[16] Ge C, Biere A. Decomposition strategies to count integer solutions over linear constraints. In: Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI). 2021, 1389−1395

[17] Ge C. Approximate integer solution counts over linear arithmetic constraints. In: Proceedings of the 38th AAAI Conference on Artificial Intelligence. 2024, 8022−8029

[18] Chakraborty S, Meel K S, Mistry R, Vardi M Y. Approximate probabilistic inference via word-level counting. In: Proceedings of the 30th AAAI Conference on Artificial Intelligence. 2016, 3218−3224

[19] Bueler B, Enge A, Fukuda K. Exact volume computation for polytopes: a practical study. In: Kalai G, Ziegler G M, eds. Polytopes - Combinations and Computation. Basel: Birkhauser, 2000, 131−154

[20] Ge C, Ma F. A fast and practical method to estimate volumes of convex polytopes. In: Proceedings of the 9th International Workshop on Frontiers in Algorithmics. 2015, 52−65

[21] de Loera J A, Hemmecke R, Tauzer J, Yoshida R . Effective lattice point counting in rational convex polytopes. Journal of Symbolic Computation, 2004, 38( 4): 1273–1302

[22] Verdoolaege S, Seghir R, Beyls K, Loechner V, Bruynooghe M . Counting integer points in parametric polytopes using BARVINOK’s rational functions. Algorithmica, 2007, 48( 1): 37–66

[23] Soos M, Meel K S. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: Proceedings of the 33rd AAAI Conference on Artificial Intelligence. 2019, 1592−1599

[24] Sang T, Bacchus F, Beame P, Kautz H A, Pitassi T. Combining component caching and clause learning for effective model counting. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT). 2004

[25] Sharma S, Roy S, Soos M, Meel K S. GANAK: a scalable probabilistic exact model counter. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI). 2019, 1169−1176

RIGHTS & PERMISSIONS

Higher Education Press