The Power of Literal Equivalence in Model Counting

Authors

  • Yong Lai Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University, China School of Computing, National University of Singapore
  • Kuldeep S. Meel School of Computing, National University of Singapore
  • Roland H. C. Yap School of Computing, National University of Singapore

Keywords:

Solvers and Tools, Satisfiability, Automated Reasoning and Theorem Proving, Stochastic Models & Probabilistic Inference

Abstract

The past two decades have seen the significant improvements of the scalability of practical model counters, which have been quite influential in many applications from artificial intelligence to formal verification. While most of exact counters fall into two categories, search-based and compilation-based, Huang and Darwiche's remarkable observation ties these two categories: the trace of a search-based exact model counter corresponds to a Decision-DNNF formula. Taking advantage of literal equivalences, this paper designs an efficient model counting technique such that its trace is a generalization of Decision-DNNF formula. We first propose a generalization of Decision-DNNF, called CCDD, to capture literal equivalences, then show that CCDD supports model counting in linear time, and finally design a model counter, called ExactMC, whose trace corresponds to CCDD. We perform an extensive experimental evaluation over a comprehensive set of benchmarks and conduct performance comparison of ExactMC vis-a-vis the state of the art counters, c2d, Dsharp, miniC2D, D4, ADDMC, and Ganak. Our empirical evaluation demonstrates ExactMC can solve 885 instances while the prior state of the art could solve only 843 instances, representing a significant improvement of 42 instances.

Downloads

Published

2021-05-18

How to Cite

Lai, Y., Meel, K. S., & Yap, R. H. C. (2021). The Power of Literal Equivalence in Model Counting. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3851-3859. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16503

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization