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

作     者：周俊萍 李睿智 曾志勇 殷明浩 ZHOU Jun-Ping;LI Rui-Zhi;ZENG Zhi-Yong;YIN Ming-Hao

作者机构：东北师范大学计算机科学与信息技术学院吉林长春130117 

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

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2016年第27卷第9期

页      码：2185-2198页

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

主 题 词：#SMT 满足性 差分进化 线性公式 

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 081104[081104] 08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 

核心收录：

D　O　I：10.13328/j.cnki.jos.004856

馆 藏 号：203190584...