Preprocessing in Model Counting through Clause and Variable Elimination

Abstract:

Preprocessing model counting instances can reduce their size considerably and decrease the solving time. In this paper we present a preprocessing algorithm Preprocess, which combines many advanced techniques, such as the unit propagation, and the hyper-binary resolution. In particular, it also combines (1) clause elimination by subsumption, and (2) variable elimination by equivalence reasoning. It has proved that these excellent technologies not only reduce the size of the model counting formulae, but also improve the ability of the model counters to solve model counting problems.

• Periodical: Advanced Materials Research (Volumes 255-260)
• Pages: 2033-2036
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.255-260.2033
• Online since: May 2011
• Authors: Qin Guo, Ai Lian Wang, Ying Liu
• Keywords: #SAT, Equivalence Reasoning, Model Counting, Preprocess, Subsumption

References

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

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

DOI: 10.1109/sfcs.2003.1238208

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

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

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

[6] 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

[7] J. Zhou, C. Zhou, M. Yin, and H. Yang: Advanced Materials Research Vol. 108-111 (2010), p.268

[8] Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano, in: Proc. of International Conference on Theory and Applications of Satisfiability Testingthe, edited by Hans KB, Zhao XS, Springer-Verlag, Berlin, Heidelberg (2010), p.85

[9] Lintao Zhang, 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.482