#SMT問題是SMT問題的擴展，它需要計算一階邏輯公式F所有可滿足解的個數．目前，該問題已被廣泛應用于編譯器優化、硬件設計、軟件驗證和自動化推理等領域，隨著#SMT問題的廣泛應用，設計可以求解較大規模#SMT實例的求解器亟待解決．基于以上原因，設計了一種求解較大規模#SMT實例的近似求解器一一VolComputeWithLocalSearch．它在現有的#SMT精確求解算法的基礎上加入差分進化算法，通過調用體積計算工具qhull，進而給出#SMT問題的近似解．算法采用群體規則減少體積計算的次數，差分進化方法快速地枚舉各個有解的區域．另外，從理論上證明了VolComputeWithLocalSearch求解器可以得到精確解的下界，使其可以應用在軟件測試等只需要知道問題下界的領域，實驗結果表明：VolComputeWithLocalSearch求解器是穩定的、具有快速的求解能力，并在高維問題上具有很好的表現．
?