Daniel J. Fremont and Markus N. Rabe and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2016-169

November 30, 2016

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-169.pdf

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, 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 citation:

@techreport{Fremont:EECS-2016-169,
    Author= {Fremont, Daniel J. and Rabe, Markus N. and Seshia, Sanjit A.},
    Title= {Maximum Model Counting},
    Year= {2016},
    Month= {Nov},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-169.html},
    Number= {UCB/EECS-2016-169},
    Note= {This is the extended version of a paper to appear at AAAI 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, 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.},
}

EndNote citation:

%0 Report
%A Fremont, Daniel J. 
%A Rabe, Markus N. 
%A Seshia, Sanjit A. 
%T Maximum Model Counting
%I EECS Department, University of California, Berkeley
%D 2016
%8 November 30
%@ UCB/EECS-2016-169
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-169.html
%F Fremont:EECS-2016-169