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

摘要：

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

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

所属期刊栏目：27

分类号：TP18(自动化基础理论)

资助基金：国家自然科学基金61370156,61403076,61403077;高等学校博士学科点专项科研基金20120043120017;新世纪优秀人才支持计划NCET-13-0724;吉林省大型科学仪器装备共享共用专项项目20150623024TC-03National Natural Science Foundation of China61370156,61403076,61403077;Research Fund for the Doctoral Program of Higher Education20120043120017;Program for New Century Excellent Talents in UniversityNCET-13-0724;The Large-scale Scientific Instrment and Equipment Sharing Project of Jilin Province20150623024TC-03

在线出版日期：2016-12-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共14页

页码：2185-2198