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

Clc Number:

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)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:April 01,2015
  • Revised:May 08,2015
  • Adopted:
  • Online: September 02,2016
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063