微信服务号

微信订阅号

2025-4-24- 11
Home > Archive>Volume 27, Issue 9, 2016 >2185-2198. DOI:10.13328/j.cnki.jos.004856
PDF HTML XML Export Cite reminder
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)

  • Article
    • | |
  • Metrics
    • |
  • Reference [32]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • 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
    [1] Cook SA.The complexity of theorem-proving procedures.In:Proc.of the 3rd Annual ACM Symp.on Theory of Computing.ACM Press,1971.151-158.[doi:10.1145/800157.805047]
    [2] Li J,Liu WF.A survey on theoretical combination techniques of SMT solvers.Computer Engineering&Science,2011,33(10):111-119(in Chinese with English abstract).
    [3] Bozzano M,Bruttomesso R,Cimatti A,Junttila T,Ranise S,van Rossum P,Sebastiani R.Efficient satisfiability modulo theories via delayed theory combination.In:Proc.of the Computer Aided Verification.Berlin Heidelberg:Springer-Valag,2005.335-349.[doi:10.1007/11513988_34]
    [4] Nieuwenhuis R,Oliveras A,Tinelli C.Solving SAT and SAT modulo theories:From an abstract davis-putnam-logemann-loveland procedure to DPLL (T).Journal of the ACM,2006,53(6):937-977.[doi:10.1145/1217856.1217859]
    [5] Jha S,Limaye R,Seshia SA.Beaver:Engineering an efficient smt solver for bit-vector arithmetic.In:Proc.of the Computer Aided Verification.Berlin,Heidelberg:Springer-Verlag,2009.668-674.[doi:10.1007/978-3-642-02658-4_53]
    [6] Zhou J,Su WH,Wang JY.New worst-case upper bound for counting exact satisfiability.Int'l Journal of Foundations of Computer Science,2014,25(6):667-678.
    [7] Huang P,Yin MH,Xu K.Exact phase transitions and approximate algorithm of#CSP.In:Proc.of the AAAI.2011.
    [8] Ma FF,Liu S,Zhang J.Volume computation for boolean combination of linear arithmetic constraints.In:Proc.of the Automated Deduction.Springer-Verlag,2009.453-468.[doi:10.1007/978-3-642-02959-2_33]
    [9] Gomes CP,Hoffmann J,Sabharwal A,Selman B.From sampling to model counting.In:Proc.of the 20th Int'l Joint Conf.on ArtificialIntelligence (IJCAI 2007).2007.2293-2299.
    [10] Dyer ME,Frieze AM.On the complexity of computing the volume of a polyhedron.SIAM Journal on Computing,1988,17(5):967-974.[doi:10.1137/0217060]
    [11] Davis M,Putnam H.A computing procedure for quantification theory.Journal of the ACM,1960,7(3):201-215.[doi:10.1145/321033.321034]
    [12] Davis M,Logemann G,Loveland D.A machine program for theorem-proving.Communications of the ACM,1962,5(7):394-397.[doi:10.1145/368273.368557]
    [13] Storn R,Price K.Differential evolution-A simple and efficient heuristic for global optimization over continuous spaces.Journal of Global Optimization,1997,11(4):341-359.[doi:10.1023/A:1008202821328]
    [14] Storn R.On the usage of differential evolution for function optimization.In:Proc.of the'96 Biennial Conf.of the North American Fuzzy Information Processing Society (NAFIPS).IEEE,1996.519-523.[doi:10.1109/NAFIPS.1996.534789]
    [15] Storn R,Price K.Minimizing the real functions of the ICEC'96 contest by differential evolution.In:Proc.of the Int'l Conf.on Evolutionary Computation.1996.842-844.[doi:10.1109/ICEC.1996.542711]
    [16] Li XT,Yin MH.Application of differential evolution algorithm on self-potential data.PloS one,2012,7(12):e51199.[doi:10.1371/journal.pone.0051199]
    [17] Li XT,Yin MH.An opposition-based differential evolution algorithm for permutation flow shop scheduling based on diversity measure.Advances in Engineering Software,2013,55:10-31.[doi:10.1016/j.advengsoft.2012.09.003]
    [18] Zhou JP,Yin MH,Zhou CG.New worst-case upper bound for#2-SAT and#3-SAT with the number of clauses as the parameter.In:Proc.of the 24th AAAI Conf.on Artificial Intelligence (AAAI 2010).2010.217-222.
    [19] Gao J,Wang JN,Yin MH.Experimental analyses on phase transitions in compiling satisfiability problems.Science China Information Sciences,2015,58(3):1-11.[doi:10.1007/s11432-014-5154-0]
    [20] Huang P,Yin MH.An upper (lower) bound for max (min) CSP.Science China Information Sciences,2014,57(7):1-9.[doi:10.1007/s11432-013-5052-x]
    [21] Zhou JP,Yin MH,Gu WX,Sun JG.Research on decreasing observation variables for strong planning under partial observation.Ruan Jian Xue Bao/Journal of Software,2009,20(2):290-304(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3152.htm[doi:10.3724/SP.J.1001.2009.03152]
    [22] Yin MH,Sun JG,Lin H,Wu X.Possibilistic extension rules for reasoning and knowledge compilation.Ruan Jian Xue Bao/Journal of Software,2010,21(11):2826-2837(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
    [23] Yin MH,Zhou JP,Sun JG,Gu WX.Heuristic survey propagation algorithm for solving QBF problem.Ruan Jian Xue Bao/Journal of Software,2011,22(7):1538-1550(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3859.htm[doi:10.3724/SP.J.1001.2011.03859]
    [24] Yin MH,Lin H,Sun JG.Solving#SAT using extension rules.Ruan Jian Xue Bao/Journal of Software,2009,20(7):1714-1725(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/3320.htm[doi:10.3724/SP.J.1001.2009.03320]
    [25] Xu L.Improved SMT-Based Bounded Model Checking for Real-Time Systems.Ruan Jian Xue Bao/Journal of Software,2010,21(7):1491-1502.http://www.jos.org.cn/1000-9825/585.htm[doi:10.3724/SP.J.1001.2010.00585]
    [26] Liu S,Zhang J,Zhu B.Volume computation using a direct Monte Carlo method.In:Proc.of the Computing and Combinatorics.Springer-Verlag,2007.198-209.[doi:10.1007/978-3-540-73545-8_21]
    附中文参考文献:
    [2] 李婧,刘万伟.SMT求解器理论组合技术研究.计算机工程与科学,2011,33(10):111-119.
    [21] 周俊萍,殷明浩,谷文祥,孙吉贵.部分可观察强规划中约减观察变量的研究.软件学报,2009,20(2):290-304.http://www.jos.org.cn/1000-9825/3152.htm[doi:10.3724/SP.J.1001.2009.03152]
    [22] 殷明浩,孙吉贵,林海,吴瑕.可能性扩展规则的推理和知识编译.软件学报,2010,21(11):2826-2837.http://www.jos.org.cn/1000-9825/3690.htm[doi:10.3724/SP.J.1001.2010.03690]
    [23] 殷明浩,周俊萍,孙吉贵,谷文祥.求解QBF问题的启发式调查传播算法.软件学报,2011,22(7):1538-1550.http://www.jos.org.cn/1000-9825/3859.htm[doi:10.3724/SP.J.1001.2011.03859]
    [24] 殷明浩,林海,孙吉贵.一种基于扩展规则的#SAT求解系统.软件学报,2009,20(7):1714-1725.http://www.jos.org.cn/1000-9825/3320.htm[doi:10.3724/SP.J.1001.2009.03320]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
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
  • Online: September 02,2016
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2038013Visitors
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