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