Maximum Model Counting

Daniel Fremont, Markus N. Rabe, and Sanjit A. Seshia. Maximum Model Counting. In Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI), pp. 3885–3892, February 2017.

Download

[pdf] 

Abstract

We introduce the problem Max#SAT, an extension of model counting (#SAT). Given a formula over sets of variables X and Y, the Max#SAT problem is to maximize over the variables X the number of solutions in Y. We demonstrate that Max#SAT has applications in many areas, showing how it can be used to solve problems in probabilistic inference (marginal MAP), planning, program synthesis, and quantitative information flow analysis. We also give an algorithm which by making only polynomially many calls to an NP oracle can approximate the maximum count to within any desired multiplicative error. The NP queries needed are relatively simple, arising from recent practical approximate model counting and sampling algorithms, which allows our technique to be effectively implemented with a SAT solver. Through several experiments we show that our approach can be successfully applied to interesting problems.

BibTeX

@inproceedings{fremont-aaai17,
  author    = {Daniel Fremont and Markus N. Rabe and Sanjit A. Seshia},
  title     = {Maximum Model Counting},
  booktitle = {Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI)},
  month = "February",
  year = {2017},
  pages     = {3885--3892},
  abstract = {We introduce the problem Max#SAT, an extension of model 
counting (#SAT). Given a formula over sets of variables X 
and Y, the Max#SAT problem is to maximize over the variables 
X the number of solutions in Y. We demonstrate that 
Max#SAT has applications in many areas, showing how it can 
be used to solve problems in probabilistic inference (marginal 
MAP), planning, program synthesis, and quantitative information 
flow analysis. We also give an algorithm which by 
making only polynomially many calls to an NP oracle can 
approximate the maximum count to within any desired multiplicative 
error. The NP queries needed are relatively simple, 
arising from recent practical approximate model counting and 
sampling algorithms, which allows our technique to be effectively 
implemented with a SAT solver. Through several experiments 
we show that our approach can be successfully applied 
to interesting problems.},
}