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

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.