[1]GU Wenxiang,ZHU Lei,HUANG Ping,et al.The model counting of a satisfiability problem[J].CAAI Transactions on Intelligent Systems,2012,7(1):33-39.
Copy

The model counting of a satisfiability problem

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 7 Number of periods: 2012 1 Page number: 33-39 Column: 学术论文—人工智能基础 Public date: 2012-02-25
Title:
The model counting of a satisfiability problem
Author(s):
GU Wenxiang;  ZHU Lei;  HUANG Ping;  YIN Minghao
School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China
Keywords:
artificial intelligence;  constraint satisfaction problem;  propositional satisfiability problem;  model counting
CLC:
TP18
DOI:
-
Abstract:
A model counting problem refers to computing the number of solutions for a given problem which is harder than the decisionmaking problem. Model counting problems are also a hot topic in the field of artificial intelligence. Research on model counting problems can not only improve the efficiency of an algorithm, but also enhance the understanding of the nature of hard problems. Taking a satisfiability problem in propositional logic, known as an SAT, and a constraint satisfaction problem (CSP) as an example, a model counting problem was reviewed from two aspects: an exact algorithm and approximate algorithm. For each aspect, the development and related concepts along with the advantages and disadvantages were emphasized. Moreover, this paper proposed some unsolved questions of the model counting and gave a summary and outlook of the research on model counting. 
References:
［1］COOK S A. The complexity of theoremproving procedures［C］//Proceedings of the Third Annual ACM Symposium on Theory of Computing. New York, USA: ACM, 1971: 151158.
［2］VALIANT L G. The complexity of computing the permanent［J］. Theoretical Computer Science, 1979, 8(2): 189201.
［3］DARWICHE A. The quest for efficient probabilistic inference［R］. Edinburgh, UK: IJCAI, 2005.
［4］DUBOIS O. Counting the number of solutions for instances of satisfiability［J］. Theoretical Computer Science, 1991, 81(1): 4964.
［5］ZHANG Wenhui. Number of models and satisfiability of sets of clauses［J］. Theoretical Computer Science, 1996, 155(1): 277288. 
［6］BIRNBAUM E, LOZINSKII E L. The good old DavisPutnam procedure helps counting models［J］. Journal of Artificial Intelligence Research, 1999, 10(1): 457477.
［7］BAYARDO R J Jr, PEHOUSHEK J D. Counting models using connected components［C］//Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence. Austin, USA, 2000: 157162.
［8］SANG T, BACCHUS F, BEAME P, et al. Combining component caching and clause learning for effective model counting［C/OL］. ［20110720］. http://cs.rochester.edu/~kautz/papers/modelcountsat04.pdf.
［9］THURLEY M. SharpSAT: counting models with advanced component caching and implicit BCP［M］//BIERE A, GOMES C P. Theory and Applications of Satisfiability Testing. Seattle, USA: Springer, 2006: 424429.
［10］DAVIES J, BACCHUS F. Using more reasoning to improve #SAT solving［C］//Proceedings of the 22nd National Conference on Artificial Intelligence. Vancouver, Canada, 2007: 185190.
［11］YIN Minghao, LIN Hai, SUN Jigui. Counting models using extension rules［C］//Proceedings of the 22nd National Conference on Artificial Intelligence. Vancouver, Canada, 2007: 19161917.
［12］DARWICHE A. New advances in compiling CNF into decomposable negation normal form［C］//Proceedings of the 16th Eureopean Conference on Artificial Intelligence. Valencia, Spain, 2004: 328332.
［13］WEI W, SELMAN B. A new approach to model counting［M］//FAHIEM B, WALSH T. Theory and Applications of Satisfiability Testing. St.Andrews, UK: Springer, 2005: 324339.
［14］WEI W, ERENRICH J, SELMAN B. Towards efficient sampling: exploiting random walk strategies［C］//Proceedings of the 19th National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence. San Jose, USA, 2004: 670676.
［15］GOMES C P, HOFFMANN J, SABHARWAL A, et al. From sampling to model counting［C］//Proceedings of the 20th International Joint Conference on Artificial Intelligence. San Francisco, USA: Morgan Kaufmann Publishers Inc, 2007: 22932299.
［16］GOMES C P, SABHARWAL A, SELMAN B. Model counting: a new strategy for obtaining good bounds［C］//Proceedings of the TwentyFirst National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference. Boston, USA, 2006: 5461.
［17］ANGELSMARK O, JONSSON P, LINUSSON S, et al. Determining the number of solutions to binary CSP instances［C］//Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming. Ithaca, USA, 2002: 327340.
［18］ANGELSMARK O, JONSSON P. Improved algorithms for counting solutions in constraint satisfaction problems［C］//Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming. Kinsale, Ireland, 2003: 8195.
［19］FAVIER A, GIVRY S D, JEGOU P. Exploiting problem structure for solution counting［C］//Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming. Lisbon, Portugal, 2009: 335343.
［20］GOMES C P, Van HOEVE W J, SABHARWAL A, et al. Counting CSP solutions using generalized XOR constraints［C］//Proceedings of the 22nd National Conference on Artificial Intelligence. Vancouver, Canada, 2007: 204209.
［21］XU Ke, LI Wei. Exact phase transitions in random constraint satisfaction problems［J］. Journal of Artificial Intelligence Research, 2000, 12: 93103.
［22］HUANG Ping, YIN Minghao, XU Ke. Exact phase transitions and approximate algorithm of #CSP［C/OL］. ［20110720］. http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3508/4142.
Similar References:

Memo

-

Last Update: 2012-05-07

Copyright © CAAI Transactions on Intelligent Systems