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