#SAT Solving Algorithms Based on Extension Rule Using Heuristic Strategies
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61300049, 61402195, 61502197, 61503044); Specialized Research Fund for the Doctoral Program of Higher Education of China (20120061120059); Natural Science Research Foundation of Jilin Province (20180101053JC); Natural Science Research Foundation of Jilin Province for Young Scholars (20140520069JH, 20150520058JH)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    #SAT is used widely in the field of artificial intelligence, and many real-world problems can be reduced to #SAT to get the number of models of a propositional theory. By an in-depth study of #SAT solvers using extension rule, this paper finds that the order of reduction clause has great impact on the size of maxterm space. Thus, in this paper two heuristic strategies, MW and LC&MW are proposed to enhance the efficiency of solving #SAT. MW chooses the clause with maximum weight as reduction clause in every calling procedure; LC&MW chooses the longest clause as reduction clause in every calling procedure and takes the clause with maximum weight as tie breaker. The algorithm CER_MW is designed by using MW, and the algorithm CER_LC&MW is designed by using LC&MW. According to the experimental results, CER_MW and CER_LC&MW show a significant improvement over previous #SAT algorithms. Comparing the new #SAT solvers with other state-of-the-art #SAT solvers using extension rule also shows that CER_MW and CER_LC&MW are significantly improved over the previous #SAT algorithms in solving efficiency and solving capacity. In terms of efficiency, the speed of CER_MW and CER_LC&MW is 1.4~100 times that of other algorithms. In terms of capacity, CER_MW and CER_LC&MW can solve more instances in a time limit.

    Reference
    Related
    Cited by
Get Citation

王强,刘磊,吕帅.基于扩展规则的启发式#SAT求解算法.软件学报,2018,29(11):3517-3527

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:November 29,2016
  • Revised:January 11,2017
  • Adopted:
  • Online: April 16,2018
  • 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