Maximum Model Counting
Daniel J. Fremont, Markus N. Rabe, Sanjit Seshia

Citation
Daniel J. Fremont, Markus N. Rabe, Sanjit Seshia. "Maximum Model Counting". Association for the Advancement of Artificial Intelligence (AAAI), February, 2017.

Abstract
We introduce the problem Max#SAT, an extension of model counting (#SAT). Given a formula over sets of variables X, Y, and Z, the Max#SAT problem is to maximize over the variables X the number of assignments to Y that can be extended to a solution with some assignment to Z. We demonstrate that Max#SAT has applications in many areas, show- ing 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.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Daniel J. Fremont, Markus N. Rabe, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/896.html"
  >Maximum Model Counting</a>, Association for the
  Advancement of Artificial Intelligence (AAAI), February,
  2017.

• Plain text

  Daniel J. Fremont, Markus N. Rabe, Sanjit Seshia.
  "Maximum Model Counting". Association for the
  Advancement of Artificial Intelligence (AAAI), February,
  2017.

• BibTeX

  @inproceedings{FremontRabeSeshia17_MaximumModelCounting,
      author = {Daniel J. Fremont and Markus N. Rabe and Sanjit
                Seshia},
      title = {Maximum Model Counting},
      booktitle = {Association for the Advancement of Artificial
                Intelligence (AAAI)},
      month = {February},
      year = {2017},
      abstract = {We introduce the problem Max\#SAT, an extension of
                model counting (\#SAT). Given a formula over sets
                of variables X, Y, and Z, the Max\#SAT problem is
                to maximize over the variables X the number of
                assignments to Y that can be extended to a
                solution with some assignment to Z. We demonstrate
                that Max\#SAT has applications in many areas, show-
                ing 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.},
      URL = {http://terraswarm.org/pubs/896.html}
  }
  

Posted by Daniel J. Fremont on 8 Nov 2016.
Groups: tools