Abstract
Resolution principle is an important rule of inference in theorem proving. Model counting using extension rule is considered as a counterpart to resolution-based methods for model counting. Based on the exact method, this paper proposes two approximate model counting algorithms, and proves the time complexity of the algorithms. Experimental results show that they have good performance in the accuracy and efficiency.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
If \(\sigma \) is very small, then \(S_{accur}\approx S_{appr}\). Consequently, \(\sigma \approx \sigma '=\frac{|S_{accur}-S_{appr}|}{S_{appr}}\). So \(\sigma '\) is also considered as approximate dispersion. In this paper, we use \(\sigma '\) to get the approximate number of unsatisfying assignments of \(\varSigma \), because it is difficult to use \(\sigma \) in the condition that we do not know the exact number of unsatisfying assignments of \(\varSigma \). However, in the experimental results, we obtain the approximate value of models and know the exact number of models, so we use \(\sigma \) to measure the two approximate algorithms.
- 2.
When \(sumterm\) is the value of the first sum term, \(svalue = 0\). In this case, we can not run the division operator, so we restrict \(i\ge 2\); because model counting is generally to count the number of models of a Boolean formula, the number of unsatisfying assignments is less than \(2^{v}\). So we restrict its approximate value is less than \(2^{v}\).
References
Rintanen, J.: Planning as satisfiability: heuristics. Artif. Intell. 193, 45–86 (2012)
Cai, D., Yin, M.: On the utility of landmarks in SAT based planning. Knowl.-Based Syst. 36, 146–154 (2012)
Nakhost, H., Mller, M.: Towards a theory of random walk planning: regress factors. fair homogeneous graphs and extensions. AI Communications 27(4), 329–344 (2014)
Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for # SAT and bayesian inference. In: 44th Symposium on Foundations of Computer Science (FOCS), pp. 340–351 (2003)
Li, W., Poupart, P., Beek, P.V.: Exploiting structure in weighted model counting approaches to probabilistic inference. J. Artif. Intell. Res. 40, 729–765 (2011)
Domshlak, C., Hoffmann, J.: Probabilistic planning via heuristic forward search and weighted model counting. J. Artif. Intell. Res. 30, 565–620 (2007)
Satish Kumar, T.K.: A model counting characterization of diagnoses. In: 13th International Workshop on Principles of Diagnosis, pp. 70–76 (2002)
Zhang, S., Zhang, C., Yan, X.: Post-mining: maintenance of association rules by weighting. Inf. Syst. 28(7), 691–707 (2003)
Wu, X., Zhang, S.: Synthesizing high-frequency rules from different data sources. IEEE Trans. Knowl. Data Eng. 15(2), 353–367 (2003)
Gomes, C.P., Sabharwal, A., Selman, B.: Model counting, handbook of satisfiability. In: Biere, A., et al. (eds.) Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 633–654. IOS Press, Amsterdam (2009)
Birnbaum, E., Lozinskii, E.: The good old davis-putnam procedure helps counting models. J. Artif. Intell. Res. 10, 457–477 (1999)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Bayardo Jr., R.J., Pehoushek, J.D.: Counting models using connected components. In: Seventeenth National Conference on Artificial Intelligence (AAAI), pp. 157–162 (2000)
Sang, T., Bacchus, F., Beame, P., Kautz, H., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 20–28 (2004)
Thurley, M.: SharpSAT – counting models with advanced component caching and implicit bcp. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424–429. Springer, Heidelberg (2006)
Bacchus, F., Dalmao, S., Pitassi, T.: Solving # SAT and bayesian inference with backtracking search. J. Artif. Intell. Res. 34, 391–442 (2009)
Wei, W., Selman, B.: A new approach to model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 324–339. Springer, Heidelberg (2005)
Wei, W., Erenrich, J., Selman, B.: Towards efficient sampling: exploiting random walk strategies. In: Nineteenth National Conference on Artificial Intelligence (AAAI), pp. 670–676 (2004)
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)
Gomes, C.P., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: Twentieth International Joint Conference on Artificial Intelligence (IJCAI), pp. 2293–2299 (2007)
Gogate, V., Dechter, R.: Approximate counting by sampling the backtrackfree search space. In: Twenty-Second National Conference on Artificial Intelligence (AAAI), pp. 198–203 (2007)
Kroc, L., Sabharwal, A., Selman, B.: Leveraging belief propagation, backtrack search, and statistics for model counting. Ann. Oper. Res. 184(1), 209–231 (2011)
Lin, H., Sun, J.: Zhang, Y.: Theorem proving based on extension rule. J. Autom. Reasoning 31(1), 11–21 (2003)
Iwama, K.: CNF satisfiability test by counting and polynomial average time. SIAM J. Comput. 18(2), 385–391 (1989)
Yin, M., Sun, J.: Counting models using extension rules. In: Twenty-Second National Conference on Artificial Intelligence (AAAI), pp. 1916–1917 (2007)
Yin, M., Lin, H., Sun, J.: Solving # SAT using extension rules. J. Softw. 20(7), 1714–1725 (2009)
Bennett, H., Sankaranarayanan, S.: Model counting using the inclusion-exclusion principle. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 362–363. Springer, Heidelberg (2011)
Linial, N., Nisan, N.: Approximate inclusion-exclusion. Combinatorica 10(4), 349–365 (1990)
Kahn, J., Linial, N., Samorodnitsky, A.: Inclusion-exclusion: exact and approximate. Combinatorica 16(4), 465–477 (1996)
Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. In: Trick, M., Johnson, D.S (eds.) Second DIMACS Challenge on Cliques, Coloring and Satisfiability, pp. 521–532 (1993)
Acknowledgments
This paper was supported by the National Key Basic Research Program of China (973 Program, No. 2012CB326403), National Natural Science Foundation of China (Nos. 61272535, 61370156, 61363035, 61165009), Guangxi “Bagui Scholar” Teams for Innovation and Research Project, Guangxi Natural Science Foundation (No. 2013GXNSFBA019263), Science and Technology Research Projects of Guangxi Higher Education (Nos. 2013YB028, 2013YB029), Scientific Research Foundation of Guangxi Normal University for Doctors, and Guangxi Collaborative Innovation Center of Multisource Information Integration and Intelligent Processing.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Wang, J., Yin, M., Wu, J. (2015). Approximate Model Counting via Extension Rule. In: Wang, J., Yap, C. (eds) Frontiers in Algorithmics. FAW 2015. Lecture Notes in Computer Science(), vol 9130. Springer, Cham. https://doi.org/10.1007/978-3-319-19647-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-19647-3_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19646-6
Online ISBN: 978-3-319-19647-3
eBook Packages: Computer ScienceComputer Science (R0)