Extension Rule Based Model Counting Using More Reasoning

Abstract:

Extension rule is a new method for computing the number of models for a given propositional formula. In some sense, it is actually an inverse propositonal resolution. In order to improve counting performance, we introduce some reasoning rules into extension rule based model counting and present a new algorithm RCER which combines the extension rule and the reasoning rule together. The experiment results show that the algorithm not only occupies less space but also increases the efficiency for solving model counting.

• Periodical: Advanced Materials Research (Volumes 108-111)
• Pages: 268-273
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.108-111.268
• Online since: May 2010
• Authors: Jun Ping Zhou, Chun Guang Zhou, Ming Hao Yin, Hui Yang
• Keywords: Equality Reduction, Extension Rule, Hyper-Binary Resolution, Model Counting

References

[1] F. Bacchus, S. Dalmao and T. Pitassi, in: Proc. of the 44 th Symposium on Foundations of Computer Science, edited by A. Blum, D. Randall, E. Upfal, IEEE Computer Society, MA, USA (2003), p.340.

[2] M. L. Littman, S. M. Majercik and T. Pitassi: J. Auto. Reasoning Vol. 27 (2001), p.251.

[3] T. Sang, P. Beame and H.A. Kautz, in: Proc. of the 20th +ational Conf. on Artificial Intelligence, edited by S. Zilberstein, J. Koehler, S. Koenig, AAAI Press, Menlo Park (2005), p.475.

[4] R. J. Bayardo, J. D. Pehoushek, in: Proc. of the 17th +ational Conference on Artificial Intelligence, edited by S. Zilberstein, J. Koehler, S. Koenig, AAAI Press, Texas, USA (2000), p.157.

[5] T. Sang, F. Bacchus, P. Beame, H. Kautz, and T. Pitassi, in: Proc. of the Seventh International Conference on Theory and Applications of Satisfiability Testingthe, edited by Hans KB, Zhao XS, Springer-Verlag, Berlin, Heidelberg (2004), p.20.

[6] T. Sang, P. Beame, and H. Kautz, in: Proc. of the Eighth International Conference on Theory and Applications of Satisfiability Testingthe, edited by Hans KB, Zhao XS, Springer-Verlag, Berlin, Heidelberg (2005), p.226.

[7] M. Yin, H. Lin, J. Sun, in: Proc. of the Twenty-Second AAAI Conference on Artificial Intelligence, edited by S. Zilberstein, J. Koehler, S. Koenig, AAAI Press, British Columbia, Canada (2007), p. (1916).

[8] M. Yin, H. Lin, J. Sun: Journal of Software Vol. 20(2009), p.1714.

[9] F. Bacchus, in: Proc. of the 18 th +ational Conference on Artificial Intelligence, edited by S. Zilberstein, J. Koehler, S. Koenig, AAAI Press, British Columbia, Canada (2002), p.613.

[10] R. Bayardo, J. D. Pehoushek, in: Proc. of Seventeenth +ational Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, edited by S. Zilberstein, J. Koehler, and S. Koenig, AAAI Press, Menlo Park (2000).

[11] H. Lin, J. Sun, Y. Zhang: J. Auto. Reasoning Vol. 31(2003), p.11.

[12] J. Sun, Y. Li, X. Zhu, S. Lu: Journal of Computer Research and Development Vol. 46(2009), p.9.