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

来源：软件学报杂志2016年第9期北京时间：

作者：周俊萍,李睿智,曾志勇,殷明浩

单位：周俊萍，东北师范大学 计算机科学与信息技术学院, 吉林 长春 13011711,李睿智，东北师范大学 计算机科学与信息技术学院, 吉林 长春 13011702,曾志勇，东北师范大学 计算机科学与信息技术学院, 吉林 长春 13011703,殷明浩，东北师范大学 计算机科学与信息技术学院, 吉林 长春 13011704

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

关键词：#SMT;满足性;差分进化;线性公式

基金资助：国家自然科学基金（61370156，61403076，61403077）；高等学校博士学科点专项科研基金（20120043120017）；新世纪优秀人才支持计划（NCET-13-0724）；吉林省大型科学仪器装备共享共用专项项目（20150623024TC-03）