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

In recent years, there have been a lot of work on solving the Satisfiability Modulo Theories (SMT) problem, which try to decide the satisfiability of logical formulas with respect to combinations of background theories. Restricted to linear arithmetic (LA) theory, they are SMT(LA) formulas. The counting version of the SMT(LA) problems, i.e., the #SMT(LA) problems, have many applications, such as probabilistic inference, counting-based search, simple temporal planning, probabilistic program analysis, etc. To solve the problems, Dr. Ge Cunjing published his new research on 15 August 2025 in Frontiers of Computer Science co-published by Higher Education Press and Springer Nature.

This paper present a toolkit called SharpSMT for #SMT(LA) problems. SharpSMT integrates SMT satisfiability solving algorithm with various polytope subroutines: volume computation/estimation, lattice counting/approximation, for real variables and integer variables respectively.

Intuitively, the solution space of an SMT(LA) formula can be viewed as the union of many polytopes, since a set of linear constraints corresponds to a polytope. Naturally, one can first enumerate polytopes by SMT solving (DPLL(T) framework), and then handling polytopes with subroutines, and finally sum up the volume, or integer point count of each polytope.

Based on this idea, a regular run of SharpSMT has four stages: parsing and rewriting, feasible assignments enumeration, polytope preprocessing and polytope subroutines. In this paper, Dr Ge further introduces some new polytope preprocessing techniques and integrates them deeply to improve the efficiency of polytope subroutines in the fourth stage, such as, factorization, variable elimination, cache technique, etc. Extensive experiments on random and application benchmarks clearly show that the new polytope preprocessing techniques are very effective, especially on application instances generated from program analysis.