首页 | 本学科首页   官方微博 | 高级检索  
     

求解#SMT问题的局部搜索算法
引用本文:周俊萍,李睿智,曾志勇,殷明浩.求解#SMT问题的局部搜索算法[J].软件学报,2016,27(9):2185-2198.
作者姓名:周俊萍  李睿智  曾志勇  殷明浩
作者单位:东北师范大学 计算机科学与信息技术学院, 吉林 长春 130117,东北师范大学 计算机科学与信息技术学院, 吉林 长春 130117,东北师范大学 计算机科学与信息技术学院, 吉林 长春 130117,东北师范大学 计算机科学与信息技术学院, 吉林 长春 130117
基金项目:国家自然科学基金(61370156,61403076,61403077);高等学校博士学科点专项科研基金(20120043120017);新世纪优秀人才支持计划(NCET-13-0724);吉林省大型科学仪器装备共享共用专项项目(20150623024TC-03)
摘    要:#SMT问题是SMT问题的扩展,它需要计算一阶逻辑公式F所有可满足解的个数.目前,该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用,设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因,设计了一种求解较大规模#SMT实例的近似求解器——VolComputeWithLocalSearch.它在现有的#SMT精确求解算法的基础上加入差分进化算法,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数,差分进化方法快速地枚举各个有解的区域.另外,从理论上证明了VolComputeWithLocalSearch求解器可以得到精确解的下界,使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明:VolComputeWithLocalSearch求解器是稳定的、具有快速的求解能力,并在高维问题上具有很好的表现.

关 键 词:#SMT  满足性  差分进化  线性公式
收稿时间:4/1/2015 12:00:00 AM
修稿时间:5/8/2015 12:00:00 AM

Local Search Algorithm for Solving #SMT Problem
ZHOU Jun-Ping,LI Rui-Zhi,ZENG Zhi-Yong and YIN Ming-Hao.Local Search Algorithm for Solving #SMT Problem[J].Journal of Software,2016,27(9):2185-2198.
Authors:ZHOU Jun-Ping  LI Rui-Zhi  ZENG Zhi-Yong and YIN Ming-Hao
Affiliation:School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China,School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China,School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China and School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China
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.
Keywords:#SMT  satisfiability  differential evolution  linear formulation
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号