×
Wang, Jinyan; Yin, Minghao; Wu, Jingli

Two approximate algorithms for model counting. (English) Zbl 1356.68110

Theor. Comput. Sci. 657, Part A, 28-37 (2017).
Summary: Model counting is the problem of computing the number of models or satisfying assignments for a given propositional formula, and is #P-complete. Owing to its inherent complexity, approximate model counting is an alternative in practice. Model counting using the extension rule is an exact method, and is considered as an alternative to resolution-based methods for model counting. Based on the exact method, we propose two approximate model counting algorithms, and prove the time complexity of the algorithms. Experimental results show that they have good performance in the accuracy and efficiency.

MSC:

68Q25 Analysis of algorithms and problem complexity
03B05 Classical propositional logic
03B35 Mechanization of proofs and logical operations
68W25 Approximation algorithms

Keywords:

propositional satisfiability; model counting; resolution principle; extension rule

Software:

Walksat; sharpSAT
PDFBibTeX XMLCite
\textit{J. Wang} et al., Theor. Comput. Sci. 657, Part A, 28--37 (2017; Zbl 1356.68110)
Full Text: DOI

References:

[1] Gomes, C. P.; Kautz, H.; Sabharwal, A.; Selman, B., Satisfiability solvers. Handbook of knowledge representation, (Harmelen, F.; etal., Found. Artif. Intell., vol. 3 (2008), Elsevier), 89-134
[2] Rintanen, J., Planning as satisfiability: heuristics, Artificial Intelligence, 193, 45-86 (2012) · Zbl 1270.68276
[3] Cai, D.; Yin, M., On the utility of landmarks in SAT based planning, Knowl.-Based Syst., 36, 146-154 (2012)
[4] Nakhost, H.; Müller, M., Towards a theory of random walk planning: regress factors, fair homogeneous graphs and extensions, AI Commun., 27, 4, 329-344 (2014) · Zbl 1338.68245
[5] Gomes, C. P.; Sabharwal, A.; Selman, B., Model counting, handbook of satisfiability, (Biere, A.; etal., Frontiers Artificial Intelligence Appl., vol. 185 (2009), IOS Press), 633-654 · Zbl 1183.68568
[6] Kroc, L.; Sabharwal, A.; Selman, B., Leveraging belief propagation, backtrack search, and statistics for model counting, Ann. Oper. Res., 184, 1, 209-231 (2011) · Zbl 1225.90108
[7] Bacchus, F.; Dalmao, S.; Pitassi, T., Algorithms and complexity results for #SAT and Bayesian inference, (44th Symposium on Foundations of Computer Science. 44th Symposium on Foundations of Computer Science, FOCS (2003)), 340-351
[8] Li, W.; Poupart, P.; Beek, P. V., Exploiting structure in weighted model counting approaches to probabilistic inference, J. Artificial Intelligence Res., 40, 729-765 (2011) · Zbl 1216.68247
[9] Domshlak, C.; Hoffmann, J., Probabilistic planning via heuristic forward search and weighted model counting, J. Artificial Intelligence Res., 30, 565-620 (2007) · Zbl 1182.68235
[10] Satish Kumar, T. K., A model counting characterization of diagnoses, (13th International Workshop on Principles of Diagnosis (2002)), 70-76
[11] Birnbaum, E.; Lozinskii, E., The good old Davis-Putnam procedure helps counting models, J. Artificial Intelligence Res., 10, 457-477 (1999) · Zbl 0918.68098
[12] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun. ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002
[13] Bayardo, R. J.; Pehoushek, J. D., Counting models using connected components, (Seventeenth National Conference on Artificial Intelligence. Seventeenth National Conference on Artificial Intelligence, AAAI (2000)), 157-162
[14] Sang, T.; Bacchus, F.; Beame, P.; Kautz, H.; Pitassi, T., Combining component caching and clause learning for effective model counting, (Seventh International Conference on Theory and Applications of Satisfiability Testing. Seventh International Conference on Theory and Applications of Satisfiability Testing, SAT (2004)), 20-28
[15] Thurley, M., SharpSAT-counting models with advanced component caching and implicit BCP, (Ninth International Conference on Theory and Applications of Satisfiability Testing. Ninth International Conference on Theory and Applications of Satisfiability Testing, SAT (2006)), 424-429
[16] Bacchus, F.; Dalmao, S.; Pitassi, T., Solving #SAT and Bayesian inference with backtracking search, J. Artificial Intelligence Res., 34, 391-442 (2009) · Zbl 1182.68294
[17] Lagniez, J.-M.; Marquis, P., Preprocessing for propositional model counting, (Twenty-Eighth National Conference on Artificial Intelligence. Twenty-Eighth National Conference on Artificial Intelligence, AAAI (2014)), 2688-2694
[18] Wei, W.; Selman, B., A new approach to model counting, (Eighth International Conference on Theory and Applications of Satisfiability Testing. Eighth International Conference on Theory and Applications of Satisfiability Testing, SAT (2005)), 324-339 · Zbl 1128.68487
[19] Wei, W.; Erenrich, J.; Selman, B., Towards efficient sampling: exploiting random walk strategies, (Nineteenth National Conference on Artificial Intelligence. Nineteenth National Conference on Artificial Intelligence, AAAI (2004)), 670-676
[20] Jweeum, M. R.; Valiant, L. G.; Vazirani, V. V., Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci., 43, 169-188 (1986) · Zbl 0597.68056
[21] Gomes, C. P.; Hoffmann, J.; Sabharwal, A.; Selman, B., From sampling to model counting, (Twentieth International Joint Conference on Artificial Intelligence. Twentieth International Joint Conference on Artificial Intelligence, IJCAI (2007)), 2293-2299
[22] Gogate, V.; Dechter, R., Approximate counting by sampling the backtrackfree search space, (Twenty-Second National Conference on Artificial Intelligence. Twenty-Second National Conference on Artificial Intelligence, AAAI (2007)), 198-203
[23] Kroc, L.; Sabharwal, A.; Selman, B., Leveraging belief propagation, backtrack search, and statistics for model counting, Ann. Oper. Res., 184, 1, 209-231 (2011) · Zbl 1225.90108
[24] Lin, H.; Sun, J.; Zhang, Y., Theorem proving based on extension rule, J. Automat. Reason., 31, 1, 11-21 (2003) · Zbl 1043.03012
[25] Iwama, K., CNF satisfiability test by counting and polynomial average time, SIAM J. Comput., 18, 2, 385-391 (1989) · Zbl 0674.68034
[26] Yin, M.; Sun, J., Counting models using extension rules, (Twenty-Second National Conference on Artificial Intelligence. Twenty-Second National Conference on Artificial Intelligence, AAAI (2007)), 1916-1917
[27] Yin, M.; Lin, H.; Sun, J., Solving #SAT using extension rules, J. Softw., 20, 7, 1714-1725 (2009), (in Chinese) · Zbl 1212.68313
[28] Bennett, H.; Sankaranarayanan, S., Model counting using the inclusion-exclusion principle, (Sakallah, K. A.; Simon, L., 14th International Conference on Theory and Applications of Satisfiability Testing. 14th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Comput. Sci., vol. 6695 (2011), Springer: Springer Heidelberg), 362-363
[29] Linial, N.; Nisan, N., Approximate inclusion-exclusion, Combinatorica, 10, 4, 349-365 (1990) · Zbl 0738.05009
[30] Kahn, J.; Linial, N.; Samorodnitsky, A., Inclusion-exclusion: exact and approximate, Combinatorica, 16, 4, 465-477 (1996) · Zbl 0881.68084
[31] Selman, B.; Kautz, H.; Cohen, B., Local search strategies for satisfiability testing, (Second DIMACS Challenge on Cliques, Coloring and Satisfiability (1993)), 521-532
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.