#SMT Problem Based On Local Search

The Satisfiability Modulo Theories (SMT) problem is a decision problem for logicalformulas with respect to combinations of background theories, such as bit vectors and pointer,expressed in classical first-order logic with equality. Its computational complexity is NP. SMTis widely used in compiler optimization, hardware design, software validation and automatedreasoning and so on. With the development of SMT application, the counting version of SMTproblem is gradually drawing people’s attention.In some applications of#SMT problem, such as software testing, the upper or lowerbound is very practical, but exact value is futile. So, we focus on the lower bound, andpropose a new algorithm based on VolComputeBunches, we call it as VolComputeWithLocal-Search algorithm. In theory, we also prove that the solution of our algorithm is the lowerbound. We implement our algorithm, and we experiment in stability, accuracy and the abilityof algorithm computing, by instance from Sheng Liu’s and Feifei Ma’s paper and other80instances which are randomly generated. Experimental data shows that, our algorithm isstable in results and time, and improves the efficiency on the basis of ensuring calculationprecision. Comparing with VolComputeBunches, our algorithm improves greatly in solvinghigh-dimensional problems.