求解#SMT问题的局部搜索算法
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

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


Local Search Algorithm for Solving #SMT Problem
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61370156, 61403076, 61403077); Research Fund for the Doctoral Program of Higher Education (20120043120017); Program for New Century Excellent Talents in University (NCET-13-0724); The Large-scale Scientific Instrment and Equipment Sharing Project of Jilin Province(20150623024TC-03)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    #SMT problem is an extension of SMT problem. It needs to compute the number of satisfiable solutions for a given first-order logic formula. Now the problem has been widely applied in the compiler optimization, hardware design, software verification, and automated reasoning. With widespread application of #SMT problem, the design of #SMT solver for large-scale instances is needed. This work presents a design of an approximate solver (VolComputeWithLocalSearch) for solving large-scale #SMT instances. It adds the differential evolution algorithm into the existing exact solution algorithm for #SMT, and gives the approximate solution by calling the volume calculation tool qhull. The algorithm reduces the number of volume calculations by bunch rule and enumerates all regions with solutions by differential evolution algorithm. This paper also proves in theory that the solution of new algorithm is the lower bound of the exact solution, thus it can be used in software testing and other fields which only need to know the lower bound. The experimental results show that VolComputeWithLocalSearch solver is stable, fast, and has a good performance in high dimension problems.

    参考文献
    相似文献
    引证文献
引用本文

周俊萍,李睿智,曾志勇,殷明浩.求解#SMT问题的局部搜索算法.软件学报,2016,27(9):2185-2198

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2015-04-01
  • 最后修改日期:2015-05-08
  • 录用日期:
  • 在线发布日期: 2016-09-02
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号