求解#SMT问题的局部搜索算法

#SMT问题是SMT问题的扩展，它需要计算一阶逻辑公式F所有可满足解的个数.目前，该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用，设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因，设计了一种求解较大规模#SMT实例的近似求解器——VolComputeWithLocalSearch.它在现有的#SMT精确求解算法的基础上加入差分进化算法，通过调用体积计算工具qhull，进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数，差分进化方法快速地枚举各个有解的区域.另外，从理论上证明了VolComputeWithLocalSearch求解器可以得到精确解的下界，使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明：VolComputeWithLocalSearch求解器是稳定的、具有快速的求解能力，并在高维问题上具有很好的表现.

Local Search Algorithm for Solving #SMT Problem

#SMT problem is an extension of SMT problem. It needs to compute the number of satisfiable solutions for a given first-order logic formula. Now the problem has been widely applied in the compiler optimization, hardware design, software verification, and automated reasoning. With widespread application of #SMT problem, the design of #SMT solver for large-scale instances is needed. This work presents a design of an approximate solver (VolComputeWithLocalSearch) for solving large-scale #SMT instances. It adds the differential evolution algorithm into the existing exact solution algorithm for #SMT, and gives the approximate solution by calling the volume calculation tool qhull. The algorithm reduces the number of volume calculations by bunch rule and enumerates all regions with solutions by differential evolution algorithm. This paper also proves in theory that the solution of new algorithm is the lower bound of the exact solution, thus it can be used in software testing and other fields which only need to know the lower bound. The experimental results show that VolComputeWithLocalSearch solver is stable, fast, and has a good performance in high dimension problems.