Journal of Software:2016.27(9):2185-2198

(东北师范大学 计算机科学与信息技术学院, 吉林 长春 130117)
Local Search Algorithm for Solving #SMT Problem
ZHOU Jun-Ping,LI Rui-Zhi,ZENG Zhi-Yong,YIN Ming-Hao
(School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China)
Chart / table
Similar Articles
Article :Browse 1169   Download 1365
Received:April 01, 2015    Revised:May 08, 2015
> 中文摘要: #SMT问题是SMT问题的扩展,它需要计算一阶逻辑公式F所有可满足解的个数.目前,该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用,设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因,设计了一种求解较大规模#SMT实例的近似求解器——VolComputeWithLocalSearch.它在现有的#SMT精确求解算法的基础上加入差分进化算法,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数,差分进化方法快速地枚举各个有解的区域.另外,从理论上证明了VolComputeWithLocalSearch求解器可以得到精确解的下界,使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明:VolComputeWithLocalSearch求解器是稳定的、具有快速的求解能力,并在高维问题上具有很好的表现.
中文关键词: #SMT  满足性  差分进化  线性公式
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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61370156,61403076,61403077);高等学校博士学科点专项科研基金(20120043120017);新世纪优秀人才支持计划(NCET-13-0724);吉林省大型科学仪器装备共享共用专项项目(20150623024TC-03) 国家自然科学基金(61370156,61403076,61403077);高等学校博士学科点专项科研基金(20120043120017);新世纪优秀人才支持计划(NCET-13-0724);吉林省大型科学仪器装备共享共用专项项目(20150623024TC-03)
Foundation items: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)
Reference text:


ZHOU Jun-Ping,LI Rui-Zhi,ZENG Zhi-Yong,YIN Ming-Hao.Local Search Algorithm for Solving #SMT Problem.Journal of Software,2016,27(9):2185-2198