Reconstructive Algorithm Based on Extension Rule for Solving #SAT Incrementally
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61272208, 61133011, 61402196, 61003101, 61170092); Doctoral Fund of Ministry of Education of China (20100061110031); China Postdoctoral Science Foundation (2013M541302); Jilin Province Science and Technology Development Plan (20101501, 20140520067JH)

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

    #SAT problem is an important problem and used widely in the field of artificial intelligence. By the in-depth study of model counting algorithm CER based on extension rule, the calculation formula used in CER is reconstructed and its correctness is proved in this paper. Then, the concepts of maximum term intersection and extended maximum term intersection are put forward. An incremental method for #SAT is also proposed, and the extended maximum term intersections are computed preferentially based on the solution of the maximum term intersection. Pruning is performed on the extended maximum term intersections corresponding to the generalized complementary base clause sets to avoid the redundant calculation. A method is provided to decide if a clause set is generalized complementary or not by creating a complementary table for recording the complementarity of all pairs of clauses. Using this complementary table, the base clause set of extended maximum term intersection can be decided incrementally. Based on this method, the redundant calculation for deciding the complementarity of clauses and clause sets is avoided better. Experimental results show that the presented RCER algorithm runs faster than CER algorithm, especially in the instances where complementary factor is small.

    Reference
    Related
    Cited by
Get Citation

贾凤雨,欧阳丹彤,张立明,刘思光.结合扩展规则重构的#SAT问题增量求解方法.软件学报,2015,26(12):3117-3129

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:December 04,2014
  • Revised:February 15,2015
  • Adopted:
  • Online: December 04,2015
  • 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