微信服务号

微信订阅号

2025-4-9- 16
Home > Archive>Volume 20, Issue 7, 2009 >1714-1725
PDF HTML XML Export Cite reminder
Solving #SAT Using Extension Rules
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [21]
    • |
  • Related [20]
    • |
  • Cited by [2]
    • | |
  • Comments
    Abstract:

    #SAT problem is the extension of SAT problem. It involves counting models of a given set of proposition formulae. By using the inverse of resolution and the inclusion-exclusion principle to circumvent the problem of space complexity, this paper proposes a framework for both model counting and weighted model counting. It suggests a complementary method for current model counting methods. These methods are proved to be sound and complete. A model counting system, namely JLU-ERWMC, is built based on these methods.JLU-ERWMC outperforms the most efficient model counting methods in some cases.

    Reference
    [1] Zhang LT, Madign CF, Moskewicz MH, Malik S. Efficient conflict driven learning in a Boolean satisfiability solver. In: Pileggi LT,Kuehlmann A, eds. Proc. of the ACM/IEEE ICCAD 2001. New York: ACM Press, 2001. 279?285.
    [2] Zecchina R, Mezard M, Parisi G. Analytic and algorithmic solution of random satisfiability problems. Science, 2002,297:812?815.
    [3] Zecchina R, Monasson R, Kirkpatrick S, Selman B, Troyansky L. Determining computational complexity from characteristic ‘phase transitions’. Nature, 1999,400:133?137.
    [4] Kautz H, Selman B. Unifying SAT-based and graph-based planning. In: Gottlob G, Walsh T, eds. Proc. of the Int’l Joint Conf. on Artificial Intelligence (IJCAI). Seattle: Morgan Kaufmann Publishers, 1999. 318?325.
    [5] Kautz HA. Deconstructing planning as satisfiability. In: Zilberstein S, Koehler J, Koenig S, eds. Proc. of the 21st National Conf. on Artificial Intelligence (AAAI 2006). Menlo Park: AAAI Press, 2006. 178?183.
    [6] Majercik SM, Littman ML. Contingent planning under uncertainty via stochastic satisfiability. Artificial Intelligence, 2003,147(1-2):119?162.
    [7] Palacios H, Bonet B, Darwiche A, Geffner H. Pruning conformant plans by counting models on compiled d-DNNF representations.In: Biundo S, Myers KL, Rajan K, eds. Proc. of the ICAPS 2005. Menlo Park: AAAI Press, 2005. 141?150.
    [8] Bacchus F, Dalmao S, Pitassi T. Algorithms and complexity results for #SAT and Bayesian inference. In: Blum A, Randall D,Upfal E, eds. Proc. of the FOCS 2003. Washington: IEEE Computer Society, 2003. 340?351.
    [9] Birnbaum E, Lozinskii E. The good old Davis-Putnam procedure helps counting models. Journal of Artificial Intelligence Research,1999,10(1):457?477.
    [10] Sang T, Bacchus F, Beame P, Kautz H, Pitassi T. Combining component caching and clause learning for effective model counting.In: Hans KB, Zhao XS, eds. Proc. of the SAT 2004. Berlin, Heidelberg: Springer-Verlag, 2004. 20?28.
    [11] Sang T, Beame P, Kautz H. Heuristic for fast exact model counting. In: Hans KB, Zhao XS, eds. Proc. of the SAT 2005. Berlin,Heidelberg: Springer-Verlag, 2005. 226?240.
    [12] Sang T, Beame P, Kautz H. Solving Bayesian networks by weighted model counting. In: Zilberstein S, Koehler J, Koenig S, eds.Proc. of the 20th National Conf. on Artificial Intelligence (AAAI 2005). Menlo Park: AAAI Press, 2005. 475?482.
    [13] Wei W, Selman B. A new approach to model counting. In: Hans KB, Zhao XS, eds. Proc. of the SAT 2005. Berlin, Heidelberg:Springer-Verlag, 2005. 324?339.
    [14] Chavira M, Darwiche A. Compiling Bayesian networks with local structure. In: Gottlob G, Walsh T, eds. Proc. of the Int’l Joint Conf. on Artificial Intelligence (IJCAI). Seattle: Morgan Kaufmann Publishers, 2005. 211?219.
    [15] Chavira M, Darwiche A. On probabilistic inference by weighted model counting. Artificial Intelligence, 2008,172(6-7):772?799.
    [16] Darwiche A. On the tractability of counting theory models and its application to belief revision and truth maintenance. Journal of Non-Classical Logics, 2001,11(1-2):11?34.
    [17] Lin H, Sun JG, Zhang YM. Theorem proving based on extension rule. Journal of Automated Reasoning, 2003,31(1):11?21.
    [18] Lin H, Sun JG. Knowledge compilation using extension rule. Journal of Automated Reasoning, 2004,32(2):93?102.
    [19] Wu X, Sun JG, Lin H, Feng SS. Modal extension rule. Progress in Natural Science, 2005,15(6):550?558.
    [20] Sun JG, Li Y, Zhu XJ, Lu S. A novel theorem proving algorithm based on extension rule. Journal of Computer Research and Development, 2009,46(1):9?14 (in Chinese with English abstract). 附中文参考文献:
    [20] 孙吉贵,李莹,朱兴军,吕帅.一种新的基于扩展规则的定理证明算法.计算机研究与发展,2009,46(1):9?14.
    Comments
    Comments
    分享到微博
    Submit
Get Citation

殷明浩,林 海,孙吉贵.一种基于扩展规则的#SAT 求解系统.软件学报,2009,20(7):1714-1725

Copy
Share
Article Metrics
  • Abstract:5275
  • PDF: 7188
  • HTML: 0
  • Cited by: 0
History
  • Received:May 31,2007
  • Revised:February 20,2008
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034142Visitors
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